1. Freeze the object under review
Record the repository or archive, commit, manuscript version, Lean release, Lake configuration, dependency lock state and target theorem names. An “AI-generated proof” without a stable source object cannot be independently replayed.
2. Rebuild in a clean or declared environment
Run the documented build and preserve the commands, tool versions, outputs and failures. A successful build is useful, but it is the beginning of verification rather than the final finding.
3. Search for incomplete proof devices
Inspect for sorry, admit and dependencies on sorryAx. Check the exact target rather than treating a repository-wide search alone as proof of completeness.
4. Read the exact theorem
List its variables, types, hypotheses, conclusion and key definitions. Compare them line by line with the natural-language claim. AI systems can produce a valid proof of an unintended or weakened proposition.
5. Inspect axioms, imports and trust expansion
Use #print axioms on the target and trace unexpected dependencies. Record custom axioms and mechanisms such as native decision procedures whose trust extends beyond ordinary kernel reduction. The issue is not that every axiom is improper; it is that the report must state what the result is conditional on.
6. Replay through the agreed checker
Replay the target using the frozen toolchain. Where the project permits, use lean4checker --fresh or another agreed independent checker. For high-risk work, Lean’s validation guidance describes a stronger pattern: a minimal trusted challenge, Comparator and external checker replay. Claim this only when it was commissioned and completed.
7. Compare the formal artifact with the paper
Determine whether definitions correspond, whether the encoded theorem reaches the advertised endpoint and whether informal consequences require additional reasoning. This is where a technically accepted proof can still fail the research question.
8. Report the finding and its limits
Separate author-supplied artifacts from audit-authored checks. Identify versions, commands, target declarations, assumption closures, discrepancies and untested claims. Preserve failed or inconclusive checks. A concise bounded finding is more useful than a sweeping “verified” badge.
Sources and further reading
- Lean Reference: Validating a Lean Proof
- Lean Reference: Axioms
- Haivian Boolean-functions validation record
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.