The landscape
Who checks the AI mathematician?
Machines now generate formal proofs faster than any human can read them. The hard problem is no longer producing proofs — it's deciding which ones to trust. That question doesn't have an owner yet.
In the span of two years, "can AI do real mathematics?" stopped being a thought experiment. AlphaProof reached silver-medal performance on International Mathematical Olympiad problems under formal conditions. DeepSeek-Prover and its successors pushed automated theorem proving into problems that resisted every prior method. Labs like Harmonic and Math Inc raised serious money — Harmonic closed $120M at a $1.45B valuation in late 2025 — on the premise that a machine can produce mathematics you can rely on.
The engine of all of it is the proof assistant. Lean gives these systems something no natural-language model has: a ground-truth reward signal. A proof either checks or it doesn't. You can generate millions of attempts and keep only the ones the kernel accepts. Formalization is what makes AI mathematics trainable, and it is what makes the results feel trustworthy.
Which is exactly where the story gets complicated.
The seductive claim
Here is the pitch, in its strongest form, from Harmonic's own framing of its Aristotle system:
When our system outputs the proof, nobody has to look at it. You know it's correct.
— Harmonic, on Aristotle
It's a genuinely exciting idea, and for the proof, it's essentially true: if the kernel accepts a proof of statement S, you do not need to read the proof. The kernel read it, more carefully than any human could.
But "nobody has to look at it" quietly smuggles in a second claim: that S is the theorem you cared about. And that nobody checked. The kernel certifies the proof against the statement. It is silent on whether the statement faithfully captures the intended mathematics — the specification gap that a wrong-but-type-correct statement sails straight through. Somebody wrote S, or a model did, and if S has a vacuous hypothesis, a junk-value convention, or a subtly wrong definition, the checkmark certifies a hollow claim with total confidence.
The bottleneck moved
For decades the hard part of formal mathematics was the proof — the sheer labor of getting a machine to accept an argument a human found obvious. AI is dissolving that bottleneck. What it reveals underneath is a different one.
Two of the largest formalization efforts of the past year make the point from opposite directions. Tao's Equational Theories Project — a massive, distributed formalization — reported that on the genuinely hard implications, public LLMs "did not provide useful suggestions beyond what the human participants could already propose"; the workhorses were human expertise and classical automated provers. And a separate marathon effort noted that verifying an entire research paper — every definition, lemma, and theorem formalized so the whole thing type-checks with no sorry — "remains largely open."
The pattern is consistent across the 2026 literature: producing a proof of a given statement is increasingly automatable; producing a faithful statement, and trusting a whole development end to end, is not. Autoformalization and human-in-the-loop verification are where the difficulty concentrated. And they are the parts a checkmark doesn't cover.
Trust doesn't vanish. It moves.
There's a tidy way to say what formal verification actually buys you: it doesn't eliminate the need for trust, it relocates it. A machine-checked proof shrinks the gap between an implementation and its specification almost to zero — for the properties someone thought to state, within a model, relative to a trusted base. Everything outside that — is the spec right? are the definitions honest? is the trusted base sound? — is where the risk now lives.
In software formal methods, an entire industry grew up around exactly this realization. Firms like Galois have spent years, much of it under DARPA funding, on the premise that specifying and auditing what you're verifying is skilled, expensive, human work — and that getting the spec wrong is the failure mode that matters. Mathematics is now walking into the same realization, at speed, with AI as the accelerant.
An independent layer, or nothing
So: who checks the AI mathematician? Right now, the answer is uncomfortable. Often it's the same lab that produced the result, using the same tools that produced it — or nobody, because the checkmark was taken as the final word. When an AI-assisted proof of an Erdős problem circulated with a machine-verified badge and a statement that didn't match the intended problem, it wasn't a proving failure. It was a specification failure that verification had made look settled.
Peer review, the traditional answer, is slow, unpaid, and increasingly not fluent in Lean. Automated faithfulness checkers are improving but, by their own authors' admission, not yet reliable. That leaves a gap with a specific shape: independent people, fluent in both the mathematics and the proof assistant, who audit the statement and definitions — not the lab, not the model, not a badge.
That's the layer we think has to exist as AI mathematics scales, and the reason we're building Qed. Not to re-run your build — the kernel already did that, perfectly. To answer the question the kernel can't: is this the theorem you meant, and can you stake your name on it?
As the volume of machine-generated mathematics grows, that question doesn't get easier. It gets more expensive to answer, and more expensive to get wrong.