AxiomProver: When Mathematical Intuition Meets the Formalization Tsunami
*Translated and adapted from a Chinese tech forum post on zhichai.net.*
Opening: A 24-Year-Old's "Impossible" Declaration
In June 2025, Carina Hong watched her team spend three months trying to get AI to *understand* why the angles of a triangle sum to 180 degrees—not compute it, but understand it. Her conclusion: humans teach children that things are "obvious," but teach machines that every step must be proven.
Six months later, AxiomProver scored 120/120 on the 2025 Putnam Competition—a perfect result on all 12 problems in 6 hours.
What Is AxiomProver?
AxiomProver = Axiom + Prover + X: an "AI mathematician" that writes Lean proofs. In plain terms, it is an agent that can "see" mathematical structure and translate it into machine-verifiable code:
1. A translator: turns human intuition (pictures, analogies) into rigorous Lean code 2. A stubborn verifier: accepts no "obviously"—every step needs lemmas, theorems, proofs 3. An outlier: crushes humans on combinatorics, comically clumsy on calculus 4. A collaborator: humans supply inspiration, it converts inspiration into verified facts 5. A thermometer: measuring how far the "singularity" actually is
The Putnam Results, Problem by Problem
| Problem | Human perception | AI perception | Lean lines | Time | Deciding factor | |---------|------------------|---------------|-----------|------|-----------------| | A2 | Easy (see the picture) | Tedious (definitions) | ~200 | - | Human intuition wins | | B2 | Easy (lemma) | Tedious (60+ line positivity proof) | ~150 | - | Human brevity wins | | A5 | Medium (induction) | Extremely tedious (bookkeeping) | 2054 | 518 min | AI patience wins | | A3 | Hard (combinatorial game) | Easy (branch-free) | ~300 | - | AI logic wins | | B1 | Hard (geometry) | Medium (symbolic) | ~400 | - | AI algebra wins | | A6 | Very hard (p-adics) | Hard (brute force) | High token count | 5 hours | AI persistence wins | | A4 | Medium (algebra) | Medium (geometry) | ~500 | - | Different approaches | | B4 | Medium (diagram) | Tedious (enumeration) | 1061 | - | Different approaches |
Every proof is a "digital tombstone": the human version reads "clearly," "trivial," "see figure"; the AI version reads import Mathlib, theorem, have h1 : ....
The Pipeline
The workflow: human inspiration → AI translation → Lean verification → public audit. All proofs are openly available for community review.
- Input: competition problems supplied by humans
- Processing: symbolic reasoning and formalization by AxiomProver
- Output: complete proofs verifiable in Lean
- Storage: proofs published on GitHub
- Does AI "truly understand"? Critics say it's pattern matching; supporters reply that human intuition is also pattern matching. The likely truth: AI understanding is syntactic, human understanding semantic—yet at sufficient syntactic complexity, behavior becomes indistinguishable.
- Is Lean "math enough"? Formalization has a tax: 60 lines to prove a positivity lemma, 2,054 lines for one induction argument. But that tax is Lean's value—it forces you to check every "obvious."
- Will AI replace mathematicians? Hong's answer: "We don't need to storm every problem by force. Human intuition + machine verification = the rising sea." Division of labor, not replacement.
Cognitive Topology: Two Geometries of Thought
Human mathematics: Grothendieck's "rising sea"
Humans discover patterns, abstract them into definitions (groups, manifolds), build theories, and then solve special cases—top-down, from general to particular.
AI mathematics: Turing's brute-force search
AxiomProver generates candidates, verifies each in Lean, finds a path through combinatorial explosion, and outputs a formal proof—bottom-up, from particular to general.
The post's central metaphor: human and AI thought spaces are manifolds that are similar but not isomorphic—incomparable, but complementary. Carina Hong's vision: humans provide inspiration, machines provide verification, and the two spiral upward together.
Three Approaches to the Singularity
1. GPT-5.2 Pro's absurdity: Polish mathematician Bartosz Naskręcki observed that on nontrivial problems it's hard to find anything that genuinely stalls the model, joking that either OpenAI employs "round-the-clock elves and top mathematicians" or the model is genuinely strong—a reverse Turing test where humans suspect a human is behind the machine. 2. AxiomProver's brute-force elegance: On the notoriously hard p-adic problem A6, it won via "a particularly clumsy but genuinely effective method" after 5 hours. When inspiration runs dry, endurance is creativity. 3. Terence Tao's milestone: Tao called AI's solution of an Erdős problem a milestone. If AI can autonomously solve Erdős problems, Millennium Problems (P vs NP, the Riemann Hypothesis) may fall within the foreseeable future—but Tao cautions that a milestone is not the singularity, which requires a self-improvement loop. AI remains a tool, not an agent.
Controversies
Conclusion
If AxiomProver vanished, we would lose a new way of having mathematical conversations. For millennia math was "humans speaking, humans listening." Now a third voice exists: machines speak, humans verify, machines respond—making mathematics a dialogue rather than a monologue.
Project: https://axiommath.ai Proofs: https://github.com/axiommath/proofs Founder: Carina Hong
> "Mathematics is not a clever game of symbols, but the patient excavation of truth."
The philosophy of AxiomProver: building a bridge between formality and intuition.