An AI Found the Missing Proof and Made a Mathematical Result Unconditional

A mathematical result that had remained conditional on an unresolved conjecture is now unconditional. According to the published paper, the missing idea was discovered by an AI theorem prover.

On September 7, 2026, *The Quarterly Journal of Mathematics* published “Parity of k-differentials in genus zero and one.” Its authors report that AxiomProver found the key reformulation in terms of Jacobi symbols and formally proved the main combinatorial lemma in Lean, whose proof kernel checks each logical step under explicit definitions and assumptions.

This was not simply AI producing plausible mathematical prose. The system contributed a new proof idea, generated a formal artifact that others can inspect, and helped human mathematicians turn a conditional body of work into a theorem.

Research references: [1] [2]

A conjecture was holding the geometry open

A k-differential is a mathematical object on a Riemann surface studied through complex geometry. These objects appear in work on flat surfaces, moduli spaces and surface dynamics.

Earlier research had largely determined the spin parity of certain k-differentials in genus zero and one, but its conclusion depended on an unproved number-theoretic statement known as Conjecture A.10. Prove that arithmetic conjecture, and the conditional geometric results would become unconditional.

The 2026 paper does exactly that. It recasts the parity condition using Jacobi symbols, a standard number-theory tool, and reduces the problem to a combinatorial identity plus established properties of those symbols. Theorem 1.2 proves the conjecture; the paper then states the corresponding spin-parity results unconditionally.

Research references: [2]

The AI found the step humans had not noticed

The authors are unusually explicit about where the machine contributed. They write that the key Jacobi-symbol observation and the formal proof of Lemma 2.5 were autonomously discovered by AxiomProver. In the discovery phase, they supplied only the conjecture statement—without the geometric context, prior Chen–Gendron work or a hint to use Jacobi symbols.

The system did more than check a finished human proof. It identified the bridge that made the proof work, then expressed the key combinatorial identity in Lean/Mathlib so that the argument could be mechanically verified.

The boundary is equally clear: the Lean formalization covers the combinatorial identity, not the surrounding geometric theorems about k-differentials. The complete published result still joins machine-generated formal reasoning with human mathematical exposition, prior literature and journal review.

The public repository contains the natural-language task, a formal problem statement, a Lean solution and instructions for running a comparator against the formal statement. That makes the machine’s contribution more inspectable than an answer that exists only in a chat window.

Research references: [2] [1] [3]

Verification becomes part of discovery

Generative AI is often criticized for statements that sound convincing but are false. Formal mathematics offers another route: the system must construct an object that a small, trusted proof kernel accepts.

A successful kernel check does not answer every scientific question. It does not prove that the encoded definitions capture the intended concept, establish that a result is important or novel, or replace expert review of how a lemma connects to the wider field.

But it changes what collaboration can look like. AI can search candidate strategies, propose intermediate lemmas and produce a proof whose logical validity is checkable line by line. Human mathematicians can decide which questions matter, recognize a solution’s significance, connect it to prior knowledge and translate it into understanding others can use.

In this paper, those roles met in a concrete result: the machine found and formalized the missing arithmetic step; the authors embedded it in the geometry; and the journal published the revised work.

Research references: [1] [2]

A larger workshop for human thought

The project began during the 2026 Joint Mathematics Meetings, where Dawei Chen brought the unresolved conjecture to Ken Ono. A person carried a question from one field to another; an AI searched a path through it; a team interpreted and published the result.

That pattern suggests a future in which researchers can enter unfamiliar territory with more powerful tools for exploration and verification. Formal systems can make difficult reasoning more inspectable, while AI can widen the range of approaches scientists are able to test.

The promise is not mathematics without mathematicians. It is a larger mathematical workshop: people choosing the destination, machines exploring paths at extraordinary speed, formal systems checking the steps and communities deciding what the discovery means.

Research references: [2]

One result, with a visible boundary

This paper establishes one specialized mathematical result. It does not show that AxiomProver can solve arbitrary open problems, replace peer review or independently judge the value of a discovery. Four of the five authors list Axiom Math as their affiliation, and the paper describes this as a test case for a system still under development. The Boston College author, Dawei Chen, discloses support from the National Science Foundation and Simons Travel Support for Mathematicians.

Those facts belong beside the breakthrough, not in place of it. The strongest warranted conclusion is already remarkable: an AI theorem prover autonomously found the key observation in a proof, formalized the central combinatorial identity and contributed to a result published in a peer-reviewed mathematics journal.

A conditional result became unconditional—and the proof left behind a public trail that other people and machines can inspect.

*Disclosure: This article is independent editorial analysis of the journal article, its open preprint and the authors’ public proof repository. Next for Humanity has no reported commercial relationship with Axiom Math or the authors.*

Research references: [1] [2]