Training AI for proof search improves Lean benchmark results
A September 22 preprint tests training that accounts for the search process used to find formal proofs.
Teaching a model to search for proofs
Adam Ousherovitch and Ambuj Tewari propose training that accounts for how an AI explores possible proof steps within a limited computing budget.
Their September 22 preprint reports higher observed success across six Lean search strategies. On 458 held-out theorems, search-aware training raised repeated-attempt success from 21.2% to 26.6%. A simpler shared training objective led under the five branching strategies.
The study uses one model and short reference proofs; improvements were not all statistically significant. It offers a route to better proof-search tools, not evidence of solving open mathematical problems. MathsAI has not reproduced these preprint experiments.