What the verified mark means

A proof file on Proof Commons carries the mark ✓ verified when the Lean kernel has accepted it as a proof of the registered formal statement. The check is done by a program, not by a person, and always against the same fixed toolchain, which we call an epoch. Bumping the epoch is a maintainer decision, and all proofs on main are re-verified when it changes.

The current epoch

The checks

A pull request with a proof is checked in the following order; the first failure rejects it.

1. The pull request may only add or change files of the form Proofs/<Id>/<name>.lean or Proofs/<Id>/<name>.md, at most five of them and each at most 200 kB, and the statement Statements/<Id>.lean must already exist on main.
2. The proof may import only Mathlib, the statements, and proof files that are already on main.
3. The file may not contain sorry, native_decide, unsafe, implemented_by, extern, or any of the other escape hatches listed in scripts/README.md, which would let a proof bypass the kernel.
4. The module must compile with lake build inside the verifier container, which runs without network access and under memory and time limits.
5. A generated check file imports the module and, for every declaration in it, records its kind, whether its type is definitionally equal to the registered statement, and the axioms it depends on; every declaration must live in the namespace ProofCommons.<Id>.<name> and every axiom must be one of propext, Classical.choice, Quot.sound.
6. The verdict is proves the statement if some declaration has the type of the registered statement, verified lemmas only if at least one theorem was verified without proving the statement, and rejected if nothing was proved.

The verifier does not yet replay the compiled .olean files through the independent kernel checker lean4checker; this is planned as soon as a release of lean4checker exists for the pinned toolchain (there was none for Lean v4.33.1 at the time of writing).

What it does not mean

The mark says that the Lean kernel accepted a proof of the formal statement in Statements/<Id>.lean. It does not say that this formal statement is the theorem the informal text describes. Whether a formalization is faithful is a human judgement, which is why every statement page lists the ORCID iDs of the people who reviewed the formalization, or says plainly that nobody has reviewed it yet. Nor does the mark say anything about the elegance or the length of a proof; a proof file is either accepted by the kernel or it is not.

Every verified file is also tied to a person: the author of the pull request must be a registered endorser whose public ORCID record lists their GitHub account. The statement page names the endorser next to each proof, and the people page lists all registered endorsers.