Lean certificate

A machine-checkable formal proof shipped with a mathematical result, so that accepting the result requires trusting a proof kernel rather than trusting whoever announced it. Named as such by ten-proofs, where OpenAI released one for each of ten claimed advances.

The idea is older than the phrase — a formalization in Lean, Rocq or Isabelle has always been checkable by anyone. What ten-proofs adds is the release convention: the certificate travels with the announcement as a standard deliverable, and an independent checker (Comparator) is named alongside it.

Why it changes the epistemics

This hub’s standing complaint about capability claims is that they are self-reported, measured by the party with an interest in the number, on a sample it chose. ten-proofs is the first source in the corpus where that objection does not apply, and not because OpenAI is more trustworthy — because the claim isn’t a percentage. A proof term type-checks or it doesn’t. Verification costs a laptop and a mathlib cache, needs no access to the model, and returns the same answer for a skeptic as for an advocate.

That is a rare thing: a class of AI capability claim that is falsifiable by a stranger. It is worth noticing how narrow the class is — it exists only where the output is a formal object, which is mathematics, some program verification, and very little else.

What it does not certify

• Significance. The kernel says the theorem follows from the axioms. It has no opinion on whether the theorem is worth proving, which remains a human judgment the mathematical community has to make.
• Provenance. A valid proof says nothing about how it was found. ten-proofs ships narrations of the model’s reasoning, and those are ordinary unverifiable claims sitting next to a verified one — the certificate lends them no credibility.
• The statement. A certificate proves the formalized statement, and formalizing the right statement is itself an act of interpretation. A subtly weakened hypothesis passes the kernel perfectly.
• Trust in the toolchain. Lean’s kernel, mathlib’s axioms, and the absence of sorry or bespoke axioms in the file are what the trust actually rests on. Small, well-audited, and not nothing.

Cluster E’s arc

The mechanization story here has run Leibniz → Hilbert → Gödel → Lean: each step formalizing more of reasoning, each limit logical in character. alphaproof added machines producing proofs in that formal language. The certificate is a further turn — formalization used not to explore what can be proved, but as the social protocol by which a result from a source nobody can inspect becomes admissible anyway. Verification substituting for authority is a very old idea in mathematics; the new part is that the thing lacking authority is the author.

Related

ten-proofs · lean-theorem-prover · alphaproof · rocq · isabelle · llms-cant-jump · synthesis