MathematicsOlympiad-level formal mathematical reasoning with reinforcement learning
Solving olympiad geometry without human demonstrations
Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
Theorem Proving with Retrieval-Augmented Language Models
Large Language Models as Copilots for Theorem Proving in Lean
Lifelong Learning for Formal Theorem Proving
Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Solving Formal Math Problems by Decomposition and Iterative Reflection
A Frontier Model for Open-Source Automated Theorem Proving
Scaffolded data synthesis plus verifier-guided self-correction, shipping open 8B and 32B theorem-proving weights.
Winning AI Mathematical Olympiad pipeline plus the 860k chain-of-thought corpus that became the standard open math dataset.
★ 496
Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
a cross-system benchmark for formal Olympiad-level mathematics
Open Math Large Language Models Toward Verifiable Reasoning
Tao-led crowdsourced Lean formalization settling all 22 million implications between 4694 magma equational laws.
An Open and Evolving Benchmark for Verified Discovery in Mathematics
IMO-level Automated Theorem Proving
Nothing matches those filters.