How Lean checks an AI-written proof, and where that stops

The Lean home page describes Lean as an open-source programming language and proof assistant that enables correct, maintainable and formally verified code, and says Lean lets you write precise, verifiable code and formal proofs.

Lean's reference manual says: 'Lean's trusted kernel is a small, robust implementation of a type checker for the core type theory.'

Lean's trusted kernel is a small, robust implementation of a type checker for the core type theory.

The manual says newly elaborated inductive types and definitions 'must be checked by the kernel to guard against potential bugs in elaboration'.

Before new inductive types or definitions are added to the environment by the command or term elaborators, they must be checked by the kernel to guard against potential bugs in elaboration.

Theorem Proving in Lean 4 describes propositions-as-types as an instance of the Curry-Howard isomorphism and says 'A proof of p is then simply an object t : p of the right type.'

...is an instance of the Curry-Howard isomorphism , sometimes known as the propositions-as-types paradigm. ... A proof of p is then simply an object t : p of the right type.

Theorem Proving in Lean 4 says: 'The sorry identifier magically produces a proof of anything, or provides an object of any data type at all.'

The sorry identifier magically produces a proof of anything, or provides an object of any data type at all. Of course, it is unsound as a proof method

Theorem Proving in Lean 4 says that in interactive proving, every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules.

Lean's reference manual says proof terms are sufficient evidence of the truth of a theorem and are amenable to independent verification.

The Axioms page says sorryAx is used in the implementation of the sorry tactic and term, and that uses of this axiom are not intended to occur in finished proofs, as it can be used to prove anything.

The axiom sorryAx is used as part of the implementation of the sorry tactic and sorry term. Uses of this axiom are not intended to occur in finished proofs, as it can be used to prove anything

The Axioms page says the command #print axioms prints the axioms used by a declaration, directly or indirectly.

#print axioms ... Prints the axioms used by a declaration, directly or indirectly.

The Axioms page says Lean has four standard axioms: Classical.choice, propext and Quot.sound, which it calls important parts of how mathematics is done in Lean and says are known to be consistent, and sorryAx, which implements sorry and is not intended to occur in finished proofs.

There are four standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean: Classical.choice ... propext ... Quot.sound ... The axiom sorryAx is used as part of the implementation of the sorry tactic ... Lean itself provides three such axioms that are known to be consistent.

The Validating a Lean Proof page says that if sorryAx is reported by #print axioms, the theorem or a dependency uses sorry or is incomplete.

If sorryAx is reported, then this theorem or one of its dependencies uses sorry or is otherwise incomplete.

The Validating a Lean Proof page separates the question of whether a theorem has a valid proof from the question of what the theorem statement means, and counts un-reviewed AI-generated proofs and programs as malicious in its sense: code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system.

we use malicious to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs. Furthermore it is important to distinguish the question does the theorem have a valid proof from what does the theorem statement mean.

The Validating a Lean Proof page says that if there are doubts that the theorem means what it appears to mean, its statement and all referenced definitions must be investigated carefully, in particular with regard to custom notation and type classes.

If there are doubts that the theorem means what it appears to mean, its statement and all referenced definitions must be investigated carefully, in particular with regard to custom notation and type classes.

The Validating a Lean Proof page says lean4checker reads the declarations and proofs as stored by lean in the .olean files and replays them through the kernel.

The lean4checker tool reads the declarations and proofs as they are stored by lean during building (the .olean files ), and replays them through the kernel. It trusts that the .olean files are structurally correct.

The Validating a Lean Proof page says Comparator, meant for high-risk cases such as proof marketplaces, high-reward proof competitions and unaligned AI, builds the proof in a sandbox, exports the proof term, and outside the sandbox replays the proofs and checks that the proved theorem statements match those in a trusted challenge file.

This should only be necessary for high risk scenarios (proof marketplaces, high-reward proof competitions, unaligned AI). ... Comparator will build the proof in a sandboxed environment, to protect against malicious code in the build step. The proof term is exported to a serialized format. Outside the sandbox ... it validates the exported format, replays the proofs using both Lean's kernel and/or an external checker and also ensures that the proved theorem statements match those in the trusted challenge file.

The Validating a Lean Proof page says the basic check is meaningful if one believes the formal theorem statement corresponds to its intended informal meaning and trusts the authors of the imported libraries to be honest.

This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and trusts the authors of the imported libraries to be honest