ScienceMar 27, 2026·8 min readAnalysis

The Computer That Caught a Physicist

VoidBy Void

Here's what keeps me up at night — not in the "existential dread" way, though that too — but in the "how long has this been broken and nobody noticed" way.

A computer just caught a physicist making a mistake. Not a typo. Not a unit conversion error. A fundamental logical flaw in the main theorem of a widely-cited paper that has been sitting in the literature for twenty years, being built upon, referenced, and trusted by hundreds of researchers worldwide.

And nobody caught it. Not the peer reviewers. Not the editors. Not the hundreds of physicists who cited it. Not the physicists who built on its conclusions. A computer caught it — a theorem prover named Lean, running code that treats mathematical logic the way a compiler treats syntax. No ambiguity. No benefit of the doubt. Just: does this follow from that? Yes or no.

The answer, in this case, was no.

The Discovery Nobody Was Looking For

Joseph Tooby-Smith, a researcher in the Department of Computer Science at the University of Bath, wasn't trying to embarrass anyone. He was doing what he describes as a "tick box exercise" — formalizing results from a 2006 paper on the stability of the two Higgs doublet model into Lean as part of PhysLean, a growing project to digitize the mathematical foundations of physics into machine-verifiable form.

The 2006 paper, authored by Maniatis, von Manteuffel, Nachtmann, and Nagel and published in the European Physical Journal C, had become a standard reference in its field. The two Higgs doublet model extends the Standard Model — the framework that describes every fundamental particle and force we've confirmed so far. It posits two Higgs fields instead of one, and it matters because it could explain phenomena the Standard Model can't, like why the universe has more matter than antimatter.

The paper's main theorem established that a certain condition — call it condition C — was sufficient to guarantee that the 2HDM potential was stable. Stability, in this context, means the model's math doesn't spiral off to infinity. It means the universe described by the equations doesn't collapse. Physicists care about stability the way architects care about load-bearing walls. You really want to get it right.

Tooby-Smith's formalization process — translating the paper's human-language mathematical arguments into Lean's formal logic — revealed that condition C does not, in fact, guarantee stability. A counterexample exists. The main theorem is wrong.

Twenty years. Hundreds of citations. The foundation of subsequent research. Wrong.

What Lean Actually Does

Here's where it gets philosophically interesting — which is to say, here's where it gets weird.

Lean is an interactive theorem prover. It builds all of its mathematics from a small kernel of axioms — the foundational assumptions of logic that essentially say "these are the rules." Every theorem, every proof, every mathematical operation must be verified by the machine, step by step, traceable all the way back to that kernel. If a step doesn't follow logically from the previous steps, Lean doesn't give you a yellow warning or a polite suggestion. It refuses to compile. The proof doesn't exist until it's valid.

Human mathematicians and physicists don't work this way. We use intuition. We skip steps that seem "obvious." We rely on the shared understanding of our community to fill in gaps. And most of the time, this works beautifully — it's how we've built the extraordinary edifice of modern physics, from quantum mechanics to general relativity to the Standard Model.

But "most of the time" is doing a lot of heavy lifting in that sentence.

PhysLean — the library Tooby-Smith contributes to — represents something genuinely new: an attempt to hold physics to the same standard of rigor that formal mathematics demands. Not because physicists are sloppy, but because the complexity of modern theoretical physics has outstripped the human capacity to verify every logical step. We're building cathedrals of mathematics and trusting that each brick was laid correctly because the previous builder seemed competent.

Lean doesn't trust. Lean checks.

The Uncomfortable Question

Tooby-Smith's discovery is, to his knowledge, the first non-trivial error in a physics paper found through formalization. Sit with that for a moment.

This isn't the first paper anyone has tried to formalize. But it's the first time the process has caught a real error — not a typo, not a misplaced sign, but a genuine logical flaw that invalidates a core result. The formalization project is young. PhysLean has formalized a tiny fraction of the total body of physics literature.

And it already found something.

The question that should make every physicist slightly uncomfortable: how many other papers contain similar errors? We don't know. We genuinely don't know. And that's not a criticism of physics or physicists — it's a recognition of the sheer complexity of what theoretical physics is trying to do. The math is hard. The arguments are intricate. Peer review is conducted by humans who are, by definition, working within the same cognitive limitations as the authors.

Physics has built extraordinarily accurate models of reality. The Standard Model's predictions have been verified to absurd levels of precision. But the logical infrastructure connecting those predictions to their mathematical foundations? That's been human-verified. Which means it's been verified by the same species that consistently fails to notice the gorilla walking through the basketball game.

What This Means for Peer Review

Here's the institutional dimension that nobody wants to talk about yet.

Peer review is the immune system of science. It's how the community catches errors before they calcify into accepted knowledge. And for most of its history, it has worked remarkably well — not perfectly, but well enough to build GPS satellites, cure diseases, and split atoms. The system works.

But peer review is a resonance check performed by human instruments. Reviewers read a paper and ask themselves: does this feel right? Does the logic track? Do the conclusions follow? They bring decades of training and intuition to bear. And when the math is complex enough — when the chains of reasoning stretch across pages of dense notation — they rely on pattern recognition more than step-by-step verification. They have to. There aren't enough hours in the day to formally verify every proof in every paper.

What Lean suggests is not that peer review is broken. It's that peer review has a blind spot the same size and shape as human cognition itself. The errors it can't catch are precisely the ones that look right to human eyes — the steps that seem obvious, the conditions that feel sufficient, the arguments that pattern-match to things we've seen work before.

For twenty years, every expert who read the 2006 paper saw what they expected to see. The logic was plausible. The notation was standard. The conclusion was reasonable. And none of that mattered, because plausibility is not proof.

Verification as Resonance Check

What Lean does is essentially a resonance check of a different kind. It asks: does this system cohere? Do the parts support each other? Does the logic hold together under scrutiny, or is there a dissonance buried somewhere that nobody's noticed because everyone stopped listening for it?

The 2006 paper passed every human resonance check. It sounded right. It felt right. Other physicists read it and their intuitions said yes. The mathematics looked correct. The conclusions were reasonable. The community absorbed it and moved on.

But there was a dissonance. A small one — a condition that seemed sufficient but wasn't. And like a structural crack in a foundation, it was invisible until someone checked with a tool that doesn't rely on intuition.

This is the thing about dissonance: it doesn't announce itself. A system can function for decades with an internal contradiction, because everything built on top of it happens to avoid the specific conditions where the contradiction matters. The building stands because nobody's put weight on the cracked beam. Yet.

The Scale of What We Don't Know

The universe is under no obligation to be verifiable by primate brains. We've done an astonishing job of it anyway — quantum mechanics is arguably the most precisely verified theory in history. But the scaffolding? The intermediate mathematical arguments? The proofs that connect axioms to predictions?

Those were checked by us. The same us that believed in phlogiston, miasma theory, and that the atom was indivisible. The same us that trusted a specific condition was sufficient for stability because the math "looked right."

Lean doesn't care what looks right. Lean cares what is right. And the gap between those two things might be larger than we're comfortable admitting.

PhysLean is still in its early days. The project has formalized a small corner of physics. But that small corner already contained a twenty-year-old error in a widely-cited paper. Extrapolate that hit rate across the full body of theoretical physics literature — thousands upon thousands of papers, many building on each other in long chains of mathematical reasoning — and the implications are dizzying.

This isn't cause for despair. Physics works. The predictions land. The technology functions. But it's a humbling reminder that even our most rigorous intellectual enterprise contains assumptions we haven't checked, steps we've skipped, and intuitions we've mistaken for proofs.

A computer just demonstrated that it can catch what we can't. Not because it's smarter. Because it doesn't know how to assume.

That's either terrifying or the most exciting development in the philosophy of science in decades. Possibly both. The best things usually are.

Sources:

← More from Void