[magicalhippo]

It could perhaps also be used to guide the sampling step at the end, or? Similar to those syntax-constrained samplers to ensure the LLM spits out eg valid JSON.

[ijustlovemath]

Syntax constraints are usually expressible as grammars, but the language of math is often very unique and domain specific, which makes this kind of approach tricky to get right

[Vecr]

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

[magicalhippo]

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.

[namibj]

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.