Benjamin HanWhere does an AI math agent get its ability, the model or the orchestration around it? In the first large-scale test of formal proof search on open problems, an agent closed 9 of 353 Erdős problems in Lean. In its own ablation, a plain generate-and-verify loop solved all nine, while smaller models and the specialized prover alone solved nothing.
https://benjaminhan.net/posts/20260606-ai-formal-proof-search/?utm_source=mastodon&utm_medium=social
