3 ms·
Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.
by Vecr 2y ago
Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.
- magicalhippo 2y agoSo 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.
- namibj 2y agoIt'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.