Proof at Machine Speed

Most of the work we give AI has no built-in way to tell the system when it is wrong.

Ask a model to write a strategy, interpret a regulation or explain why a customer abandoned an application, and it may produce a plausible answer with no reliable way to know whether the answer is sound. A person still has to judge it, and the fluency of the response can make that harder than it sounds.

Mathematics is different. A proof can be checked.

Earlier this year, Google DeepMind gave a proof-search system 353 open problems from a collection associated with Paul Erdős. These were not benchmark exercises with answers withheld from the model. They were unsolved research problems. The system produced formal proofs for nine of them. Two had remained open for 56 years. [1]

One problem concerned an infinite collection of whole numbers. Could the collection remain surprisingly large if none of its numbers divided the sum of two larger numbers in the same collection? The system found that it could. Its proof connected ideas from two areas of mathematics in a way no one had tried before.

Nine out of 353 may not sound like much, but research mathematics is not a test where 97% means failure. Each question came from a collection of problems that had resisted existing methods. Finding even one new proof matters. Finding several suggests that something has changed.

The obvious explanation is speed. A machine can try more approaches than a person can. But speed alone does not explain why anyone should trust the result. A machine can make mistakes faster too.

What made the results credible was that the system wrote its proofs in Lean, a language and proof assistant for formal mathematics. Each proof is expressed as a series of logical steps, and Lean checks whether the conclusion follows from the stated premises. If the system skips a step or relies on something it has not established, the proof does not pass.

This gives the model something to push against. It proposes an argument, Lean identifies what does not hold, and the model revises the argument and tries again. It does not have to know in advance which path will work. It needs a reliable way to distinguish progress from persuasive nonsense.

There had been signs that this was coming. In 2024, AlphaProof reached silver-medal performance on International Mathematics Olympiad problems. Those problems were extremely difficult, but they had known answers and were designed to be solved in a competition. Open research is less accommodating. No one knows whether a statement is true, whether the available tools are sufficient, or whether the useful idea will come from an apparently unrelated corner of mathematics. [2]

That is why the Erdős results feel different. The system was no longer reproducing a path that human beings already knew existed. It was searching where there might be no path at all.

Other groups have arrived at a similar arrangement. Axiom Math's AxiomProver system produces formal proofs in Lean and pairs them with conventional mathematical papers. In May, Axios reported that five of those papers had been accepted by peer-reviewed journals. [3]

The two formats do different jobs. The Lean file establishes that the conclusion follows from the premises. The paper helps mathematicians understand what the proof means: where the main idea came from, how the result fits into the field and whether the technique might work somewhere else.

A machine could prove a theorem by exhausting thousands of narrow cases. The result would be valid but might teach us very little. A more revealing proof could expose the underlying reason and become useful in problems no one had thought to connect to the first. Mathematicians want correctness, but they also want to understand what makes a theorem true.

Recent work on the planar unit distance problem offers a good example. Put some dots on a sheet of paper and connect every pair that is exactly one unit apart. How many unit-length connections can there be as the number of dots grows? Erdős posed the problem about 80 years ago, and for decades the best arrangements resembled square grids.

A general-purpose OpenAI model found a better family of arrangements by drawing on algebraic number theory, which was not the obvious place to look. It did not solve the whole problem. It did something else that can be valuable in research: it broke a long-standing assumption about what the best construction should look like. Mathematicians checked the construction, improved the proof and began investigating the path it opened. [4]

Across these examples, the division of work is beginning to take shape. The machine searches farther than a person could. Formal tools reject invalid steps. Mathematicians determine whether the result is new, what it means and where to look next.

Formal verification still has a boundary. Lean can prove that a conclusion follows from the premises it was given. It cannot tell whether those premises faithfully represent the question a mathematician meant to ask. Leave out a condition while translating the problem into Lean, and the machine may produce a flawless proof of the wrong theorem.

This is less exotic than it sounds. You can check every calculation in a financial model and still fail to notice that the model describes a different transaction. The arithmetic is correct. The connection to reality is where the error entered.

DeepMind addressed this by asking experts to compare each formal statement with the original Erdős problem. Human judgment was still required where ordinary language became mathematics. It was required again after the proof was finished, because a theorem can be correct without being new, useful or revealing.

Saying that AI is "doing mathematics" compresses several kinds of work into one phrase. Solving an Olympiad problem, proving an open conjecture, proposing a construction and writing a paper are different activities. What gives the serious examples credibility is that the model eventually meets something it does not control. A proof checker rejects a bad inference. The existing literature reveals that a result is already known. A journal referee finds a gap. A mathematician notices that the formal statement does not match the original question.

In other words, the work can answer back.

That may matter more than speed. Intelligence becomes more useful when it operates inside an environment that can reject its output. The system can explore freely because it cannot simply declare itself correct.

You can begin to see how this changes the division of labour. A mathematician might ask a model to test dozens of constructions that would otherwise consume weeks, then spend their own time on the few that survive. Choosing the question becomes no less important. Mathematics contains an unlimited number of true statements that no one has a reason to care about. Someone still has to know which problems matter, whether an answer changes anything and which idea inside a large proof is worth carrying elsewhere. [5]

There is a useful lesson here for software in regulated markets, although the comparison has limits. Securities law is not mathematics. The meaning of a definition can depend on context. Facts arrive incomplete. Two competent people can read the same rule and disagree about how it applies.

But much of the surrounding work has more structure than our software usually acknowledges.

Suppose an investor wants to buy securities under an exemption. Eligibility depends on facts about the investor, the issuer and the transaction. Each fact should be traceable to a source. Certain answers require specific acknowledgements. Some exemptions depend on financial thresholds. If the investor's answers do not support the selected exemption, the transaction cannot move forward. A well-written explanation cannot supply evidence that is not there.

The same is true as the transaction moves forward. The amount funded should match the signed subscription agreement and the record sent to the fund administrator. A person signing for a company needs authority to do so. Identity must be verified, approvals recorded and payment confirmed before the actions that depend on them can occur.

None of these checks is as absolute as a proof in Lean. Together, however, they allow the work to resist an unsupported conclusion. A transaction that does not reconcile remains unresolved. Confident language cannot smooth over a missing approval. The system has to show what it relied on, and a person remains accountable for the decisions that require judgment.

This is how we think about the systems we build at Decimal. Investor records, entities, transactions, governing documents and approvals remain connected as the work moves. Intelligence can assemble information, prepare documents, notice what is missing and carry routine actions forward, but its conclusions remain attached to the records that support them. When the facts do not justify the next step, the work returns to the person responsible for deciding it.

The lesson from mathematics is not that every field needs its own version of Lean. Capability alone is a poor foundation for trust. The most useful systems combine intelligence with a structure that can challenge what it produces.

Mathematics has formal statements and proof checkers. Private capital has source records, permissions, rules, reconciliations and accountable decisions. When those are carried properly into the software, models can do far more of the work without asking us to take far more on faith.

Notes and further reading

1. Advancing Mathematics Research with AI-Driven Formal Proof Search

   Google DeepMind's research on applying Lean-based proof search to open Erdős problems and other research-level conjectures.

2. Mathematicians put AlphaProof to the test

   On the earlier system that reached silver-medal performance on International Mathematics Olympiad problems.

3. AI math startup's proofs land in peer-reviewed journals

   On AxiomProver and the pairing of machine-checkable proofs with papers written by mathematicians.

4. OpenAI makes a breakthrough on an 80-year-old maths problem

   On the planar unit distance result and the mathematicians who checked and developed the construction.

5. How AI is reshaping discovery in maths and physics

   On how these tools change exploration while leaving the choice and interpretation of important questions with researchers.

6. How AI is transforming mathematics

   A wider account of recent systems beginning to affect mathematical research.