1/ AxiomProver has solved Fel’s open conjecture on syzygies of numerical semigroups, autonomously generating a formal proof in Lean with zero human guidance.
This is the first time an AI system has settled an unsolved research problem in theory-building math and self verifies. 2/ We chose this problem intentionally. It is theory-building math research that requires profound capabilities including complex hierarchical decomposition, ability to backtrack, and autoformalizing definitions.
After Putnam perfect score, AxiomProver generated research math.
Jan 9 • 12 tweets • 3 min read
1/ AxiomProver got 12/12 of Putnam 2025. Today we release the Lean proofs AxiomProver generated autonomously.
We also provide our take of the problems, proof visualizations, and compare how humans vs AI approach differently. Tons of fun math and Lean!
Our findings in thread.
2/ We sorted the proofs into three categories:
i. problems that are easy for humans, but painstaking for AxiomProver
ii. problems that are surprisingly within AxiomProver's reach
iii. problems that got two completely different math approaches from humans vs AxiomProver
2/ We chose this problem intentionally. It is theory-building math research that requires profound capabilities including complex hierarchical decomposition, ability to backtrack, and autoformalizing definitions.