2025
Lean-STaR: Learning to Interleave Thinking and Proving
ICLR 2025spotlight
Traditional language model-based theorem proving assumes that by training on a sufficient amount of formal proof data, a model will learn to prove theorems. Our key observation is that a wealth of informal information that is not present in formal proofs can be useful for learning to prove theorems.…