undefined | Better HN

0 pointsVecr1y ago0 comments

Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.

0 comments

So yea that was my thought. Use it to spit out valid Lean syntax, and potentially also to backtrack if it outputs inconsistent or erroneous proofs.

namibj1y ago

It's fairly good at valid syntax already, and did the backtracking for a long time due to it doing tree search guided by it's predictions for how likely that tactic will end up finishing the tree leaf it's applied to.

j / k navigate · click thread line to collapse

0 pointsVecr1y ago0 comments

Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.

0 comments

magicalhippo1y ago

So yea that was my thought. Use it to spit out valid Lean syntax, and potentially also to backtrack if it outputs inconsistent or erroneous proofs.

namibj1y ago

j / k navigate · click thread line to collapse