Open to project work, technical leadership, and engineer-in-residence gigs. Let’s talk

Get in touch

← Back

The Leiden Declaration's real worry

June 04, 2026 aiopinionmathematics

The thing about the Leiden Declaration on AI and mathematics is that, well, it's not really about mathematics, is it? It's more about power economics and commercial disputes.

The declaration bundles four worries: proof reliability, understanding, attribution, and commercial capture. Pull them apart and only two are about mathematics at all. It reads a bit like when you have something hard to say, so you lay down some filler first to soften the focus. Great technique.

Reliability is solved. If a proof is written in a language like Lean or Coq, anything machine-checkable, its correctness is mechanical. No human needs to vouch for it. Or, easier, if we can simply follow a proof without fully internalizing it, it's still a valid proof. Which takes me to the next point.

Understanding the "why" was never universal to begin with. There's a quiet conflation in the declaration between following a proof and understanding it. They are not the same thing, and plenty of working mathematicians produce results they can follow but cannot truly explain. Even at the highest levels, we already keep a tolerated bin for verified-but-unilluminating proofs (e.g. four colours, Kepler). An AI proof we can check but not understand simply joins that bin. Either way the field gains: a verified truth is a win, an understood one is a bigger win. Neither is a loss.

So the two genuinely mathematical concerns are non-issues, provided the output advances the field or points the way.

That leaves credit and commercial capture, and those are a guild protecting a closed economy: who gets named, whose corpus gets used, who owns the model. I don't find it interesting.

Mathematics draws from the laws of the universe. You can't own it. The theorems are out there whether or not we arrive, and they'll be found one way or another. Being first feels enormous up close, but shrinks to nothing at the scale of the field. What's left of this declaration, once the epistemics dissolve, is mostly the ego that already poisons academia, now frightened that the machine doesn't care whose name is on the page.

← All articles