the three modes of machine mathematics
Every "AI does mathematics" headline belongs to one of three modes, and most of the confusion in the field comes from not saying which.
Construction. The machine outputs an object: a cap set, a matrix-multiplication scheme, a Hadamard matrix, a polynomial map with constant Jacobian. A trivial checker validates it. Wagner's 2021 counterexamples, AlphaTensor, FunSearch, AlphaEvolve, the rank-31 elliptic curve and the Jacobian counterexample all live here. The property that makes this mode work is that the machine's unreliability costs nothing. A wrong candidate is thrown away in microseconds. This is also why the classical-search baseline is so often stronger than reported: Kauers and Moosbauer beat AlphaTensor with a random walk on a flip graph two months after the Nature paper, and PatternBoost's own local-search phase is a serious competitor to its transformer. The right question for any construction result is "compared to what classical method, at what compute?"
Conjecture. The machine surfaces a pattern and a human states and proves the theorem. The knot-signature inequality of Lackenby and Juhász, Williamson's hypercube decomposition, the elliptic-curve murmurations, and the 2026 Bruhat-hypercube paper are the canonical cases. In every one, the theorem is the human's. Here the machine's comparative advantage is not proving but noticing: an object nobody thought to look for inside a fifty-year-old, heavily studied structure. The murmurations story is the purest instance, where the machine learning contributed nothing directly and yet was genuinely upstream, because a classifier succeeding at rank prediction is what prompted the plot.
Proof. The machine outputs the argument itself. This splits again. In the formal sub-mode the output is Lean, correctness is free, and the residual risk is statement fidelity: a zero-sorry build proves the Lean statement, not necessarily the English one, which is why Palomar checks the informal description against the formal one. In the informal sub-mode the output is prose and a human has to referee it, which is where the 90,000-line Sendov proof and Bloom's warning about 200-page papers "no human has read" come from.
Through the end of 2024 the scoreboard was stark: every result that constituted real new mathematics sat in the construction or conjecture modes. Formal proving had produced only proofs of known competition statements; informal proving had produced only benchmark numbers. The structural reason was that only the first two modes have free verification.
What changed in 2026 is that the proof mode started producing real theorems, and the field's response was to import free verification into it. The unit distance disproof was checked by nine mathematicians who then wrote a paper. The zeta result came with two authors of record, the previous record-holders as reviewers, a Lean formalization, released transcripts, and within three weeks an independent human reproof. Astra's ten results came with Lean certificates anyone can build, and still drew two prior-art complaints that no kernel could have caught. The Leiden Declaration and Palomar exist because the mode with the weakest built-in verification is now the one producing the biggest claims.
So the reading rule is simple. Ask which mode. If construction, ask about the classical baseline. If conjecture, ask who proved the theorem. If proof, ask who checked it and whether the formal statement says what the English does. Epoch's tier breakdown for open problems is the calibration to keep in mind: of the six solved by AI by August 2026, five were rated "moderately interesting", one a "solid result", and none of the nine rated "major advance" or "breakthrough" had fallen.