- Lean's manual describes its trusted kernel as a small implementation of a type checker, and says newly elaborated inductive types and definitions must be checked by it.
- #print axioms lists what a declaration uses; sorryAx in the list means the theorem or a dependency uses sorry or is incomplete. Lean has four standard axioms.
- The manual separates whether a theorem has a valid proof from what its statement means, and calls the basic check meaningful if the statement matches its intended meaning.
Lean is an open-source system that works both as a programming language and as a proof assistant. You use it to write precise, verifiable code and formal proofs.
Lean's manual describes its trusted kernel as a small, robust implementation of a type checker for the core type theory. New inductive types or definitions must be checked by the kernel to guard against potential bugs in elaboration.
The idea behind the check is called propositions as types. A statement is a type, and a proof of it is simply an object of that type. In interactive proving, every step has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules.
Lean's manual says proof terms are sufficient evidence of the truth of a theorem and are amenable to independent verification.
The check has limits, and the manual lists them. A proof can contain the sorry placeholder, which Lean says can prove anything and is not intended to occur in finished proofs. Running the command #print axioms on a theorem shows which axioms it depends on. A result that lists sorryAx is incomplete. Lean counts four standard axioms: propext, Classical.choice and Quot.sound, which the manual calls important parts of how mathematics is done in Lean, and sorryAx, which is not intended to occur in finished proofs.
The manual also separates two questions: whether a theorem has a valid proof, and what the theorem statement means. It says that if there are doubts the theorem means what it appears to mean, its statement and all referenced definitions must be investigated carefully.
For higher stakes it describes the lean4checker tool, which replays the stored declarations through the kernel, and a tool called Comparator, which builds the proof in a sandbox and checks that the proved statements match those in a trusted challenge file.
The manual says the check is meaningful if one believes the theorem statement matches its intended meaning and trusts the authors of the imported libraries to be honest.
What it means for you Our view
A passing Lean check answers whether a proof is valid, and leaves open whether the theorem proved is the one you wanted. The manual says to investigate the statement and the definitions it refers to when there is doubt, in particular custom notation and type classes. For higher stakes it describes lean4checker, which replays stored declarations through the kernel, and Comparator, which checks the proved statements against a trusted challenge file. When someone presents an AI-written result as verified in Lean, ask for the #print axioms output and read the theorem statement against the claim being made before you rely on it.
TAGSFormal verificationLeanlean4checker
