Mathematicians Dawei Chen and Quentin Gendron were working on a theorem in algebraic geometry involving differentials — calculus objects used for measuring distances across curved surfaces. Their proof required a formula from number theory that they could not derive or validate. The formula was a specific combinatorial identity: it connected counting arguments in two different mathematical domains, and neither domain's experts recognized it as a known result. The theorem was blocked by a gap between fields.
Axiom's AxiProver — an AI system that combines large language models with a formal proof verifier (Lean) — found the proof overnight. The connection it identified was a 19th-century numerical phenomenon that human mathematicians had not linked to the differential geometry problem. The AI did not discover a new mathematical truth. It discovered a connection between known truths that no one had noticed. The bridge was already there. It was overlooked.
The result is one of four previously unsolved problems that AxiProver solved, with proofs posted to arXiv in February 2026 and verified by Chen and collaborators. The proofs are not probabilistic — they are formal, machine-checked, correct by construction.
The structural insight is about mathematical compartmentalization. Mathematics is organized into fields — algebraic geometry, number theory, combinatorics, analysis — each with its own community, literature, and intuitions. A result in one field may be the missing lemma for a theorem in another, but the two communities may never communicate because the result is trivial in its native field and unrecognizable in the field that needs it. The Chen-Gendron obstruction was exactly this: a number-theoretic identity that was routine for number theorists but invisible to geometers.
The AI advantage here is not raw intelligence or mathematical creativity. It is field-agnosticism. AxiProver searches across the entire mathematical literature without the compartmental boundaries that human training imposes. A human geometer reads geometry. A human number theorist reads number theory. The AI reads everything and recognizes when a result in one field is the answer to a question in another. The proof it produced was not beyond human capacity. It was beyond human attention.
This suggests that the low-hanging fruit in mathematics is not in any single field. It is in the connections between fields — the bridges that exist as known results on both sides but have never been identified as the same object.