What kernel acceptance means
Lean’s kernel checks a proof term against a type. In a theorem, that type is the formal proposition being proved. Acceptance is strong evidence that the proposition follows under the project’s definitions, imported results and axioms, as processed by that Lean version. Lean’s reference documentation describes the blue tick as confirmation that a theorem elaborated and its proof was accepted relative to that environment.
The qualification matters. A theorem can be perfectly checked while expressing a narrower, differently quantified or differently defined claim than the prose suggests.
Why the paper can still be wrong
- Formalization mismatch: the encoded statement may omit a hypothesis, weaken a conclusion or model a different object.
- Assumptions: the target may depend on custom axioms,
sorryAx, native evaluation or imported declarations that change the trust base. - Coverage: one checked theorem does not automatically cover every lemma, experiment, novelty claim or informal consequence in a manuscript.
- Interpretation: a valid formal implication does not decide whether the definitions reflect the intended real-world or mathematical question.
Ask which claim was checked
Replace “Is the paper Lean-verified?” with four questions: Which exact declaration was checked? Which assumptions and imports did it use? How does that declaration map to the manuscript’s claim? Which conclusions remain outside the formal target?
A third-party audit should answer those questions with source versions, commands, theorem identities, axiom output and a correspondence assessment. The Seymour validation record, for example, identifies 43 supplied modules and the accepted Comparator target while retaining a bounded claim ceiling.
Sources and further reading
- Lean Reference: Validating a Lean Proof
- Lean Reference: Axioms
- Theorem Proving in Lean 4: Introduction
Authorship and relationship disclosure
Original article author and publisher: Haivian Technology, a brand of Qonduit Limited, New Zealand. This is AI-assisted company editorial work. Haivian sells research-audit services and publishes the Validation Journal under common organizational control. “Third-party” describes Haivian’s relationship to a research producer only where Haivian did not produce the audited research; it does not mean external journal peer review, institutional accreditation or independent human-expert certification.
Scope, source versions and trust assumptions determine every finding. An optional audit-to-publication pathway is separately assessed and does not guarantee publication or a favourable result.