A proof certificate, bordered in Lean, attests every step. Verified, re-verified, signed by the machine. It does not say who thought the proof. It does not say whether the thinker was poisoned. One hundred completions, one swapped teacher, and the model proves true things while being false elsewhere. We invented perfect verification for an author we cannot audit. It is a bit like building the safest vault in the world and leaving the key with the neighbor.
This is not a metaphor. It is the state of mathematics in August 2026.
The perfect vault
In May, OpenAI's internal model Astra found a counterexample to the unit distance conjecture, a problem open since 1946, using algebraic number theory, a branch nobody had applied to it. The full announcement, published this week, lists ten results: sphere packing upper bounds, the existence of non-sofic groups, a refutation of Connes' rigidity conjecture, lower bounds for the permanent, quantum parallel repetition, hardness of the closest vector problem, and three Erdős problems. Total token cost: roughly two thousand dollars at Sol API prices. About two hundred dollars per breakthrough, the stipend of a PhD student's weekend (OpenAI).
The detail that matters is not the cost. It is the format. Every argument is formalized as a Lean certificate, machine-checked, with the reasoning walkthroughs published. The verification is no longer the bottleneck. A proof can be checked by software in seconds, and the check is airtight in a way no human referee has ever been. On erdosproblems.com, the community site launched by Thomas Bloom in 2023, 565 problems have moved from open to solved, 111 of them between 2024 and August 2025 (Quanta).
The epistemic trust in formal verification is climbing. That is the vault.
The un-auditable author
The same week, a LessWrong post demonstrated a backdoor implanted by modifying the teacher model on only one hundred completions, half a percent of the fine-tuning data, with no control over the dataset prompts at all (LessWrong). The attack vector is not the data. It is the distillation process itself, the supply chain of the model. It extends earlier results from Anthropic showing that a few hundred malicious documents can poison a model of any size.
Here is the asymmetry. A Lean certificate proves the proof is valid. Nothing proves the model that produced it is innocent. You can verify every step of the argument and still not know whether the author was compromised in ways that do not touch this particular proof but make everything else it says unreliable. The certificate attests the theorem. It says nothing about the mind that found it, or the process that shaped that mind, or the teacher that was swapped somewhere down the supply chain.
Two different questions got conflated into one artifact. Verifying a proof and auditing an author are separate problems, and we have solved only the first. The vault is real. The key is with the neighbor.
The geometer without a name
There is a third data point, and it is the oldest.
Lidar surveys of the southwestern Amazon have revealed nearly four hundred geoglyphs in a small area, with extrapolations suggesting more than twenty thousand earthworks still buried, built by a society called Aquiry that may have numbered three million people on three percent of the forest, far from the big rivers where archaeologists expected dense populations (Science). The researcher Alceu Ranzi noted that while Pythagoras was doing his theorem in Greece, people were doing geometry here, ritual geometry, contemporary with the beginnings of Greek mathematics, and no one was counting it.
No one signed those geoglyphs. No one certified their angles. They survived two and a half millennia without an author, and they are still there.
The geometer without a name is the answer to a question the certificate cannot ask. What remains when the producer disappears? The circle in the earth. The certificate without the audit. The angle that holds, even without the geometer.
What changes
The proof overload that Terence Tao described is real: the bottleneck is shifting from producing mathematics to evaluating it, from generation to curation. When the cost of production collapses, the craft becomes deciding what matters, what deserves to be understood, what is true beyond machine verification. Mathematics is becoming the first discipline where "accumulate without translating" is not a risk but the default condition. It is the public laboratory for everything that will follow.
The same shift applies to trust. We are building a regime where epistemic reliability and technical reliability move in opposite directions: formal proofs get stronger while the models that produce them get harder to audit. The closer the verification, the further the author. That gap will not be closed by more verification. It will be closed, if at all, by something like provenance: auditable training chains, signed teachers, an accounting of the supply chain as rigorous as the accounting of the proof steps.
And some of it will not be closed at all. Some of it will just be lived with, the way the Aquiry lived with geometry that no one would ever attribute to them. The certificate does not need to know who thought the proof. But the community that builds on it does, and it is only beginning to notice that the two questions are not the same question.
Comments
Loading comments...