Freeze source, commit, Lean and Lake versions; build in a clean or declared environment.
Lean 4 verification and formalization audit
Independent verification for Lean proofs and formalized mathematics
Haivian provides third-party verification of Lean 4 proof artifacts and their relationship to mathematical research claims. Audits can include reproducible builds, theorem and dependency inspection, axiom and trust-boundary analysis, kernel replay, paper-to-formal-statement correspondence review, and publication of a scope-bounded validation report.
What a Lean result establishes. Kernel acceptance shows that the encoded theorem follows within the recorded definitions, imports, axioms and trust base. It does not by itself establish that the formal statement expresses the intended paper claim, that every paper argument is covered, or that the research is novel and publication-ready.
Seven service layers
Inspect the proof, its environment and the claim around it.
The commissioned scope selects the layers needed for the decision. A report never silently treats one check as all seven.
Locate the exact declaration, quantified variables, hypotheses and conclusion that matter.
Trace imports and supporting declarations relevant to the target rather than infer coverage from repository size.
Use tools such as #print axioms and record sorryAx, custom axioms and native-evaluation trust where present.
Replay the target through the agreed Lean toolchain and record the exact accepted object.
Compare the encoded theorem with the manuscript’s definitions, claim ceiling and stated consequences.
Publish or privately deliver the scope, methods, evidence, finding, limitations and accountable decision.
Risk-scaled validation
A ladder of checks, not a single green tick.
- Build and identify. Run the declared project build, then identify the exact theorem under review.
- Inspect assumptions. Check axiom dependencies, incomplete placeholders and trust-expanding mechanisms.
- Replay independently where suitable. Use
lean4checker --freshor another agreed checker when the project and risk warrant it. - Challenge the trust boundary. For high-risk work, an agreed minimal challenge, Comparator workflow and external checkers may be commissioned and performed.
- Review meaning. Independently assess whether the formal target captures the mathematical claim the paper asks readers to accept.
This sequence follows the distinctions in Lean’s own proof-validation guidance. The actual report states which steps were performed; it does not claim unperformed checks.
Public evidence
Four bounded Lean audit records.
These records demonstrate completed methods for their exact targets. They do not guarantee the outcome of another audit.
Seymour’s second-neighborhood conjecture
Forty-three supplied Lean modules compiled; inspected targets used the permitted axiom set; author Comparator accepted default-kernel replay.
Finite-host Sidorenko counterexample
The cumulative 31 retained and four newly completed modules were reviewed; four inspected closures used permitted axioms; author Comparator accepted the finite-host endpoint.
Nine-dimensional Borsuk counterexample
Two hundred sixty-nine supplied modules and six axiom closures were inspected; author and separate literal-R9 Comparator targets accepted.
Boolean functions beyond the square-root degree bound
Twenty-one modules underwent theorem and axiom inspection; the author-configured Comparator target accepted default-kernel replay.
Claim ceiling
What the report will not overstate.
No automatic paper certification
Lean acceptance attaches to the encoded statement and trust base. Paper-wide correctness needs a separate correspondence and reasoning review.
No implied human-expert sign-off
The report identifies who was accountable and where AI-assisted analysis was used. Specialist human review is claimed only when separately commissioned and actually performed.
No guaranteed publication
A successful private audit may be eligible for a separate publication audit. Editorial acceptance, public wording and rights review remain distinct decisions.
Relationship disclosure. Haivian sells this service and publishes its Validation Journal under common organizational control within Qonduit Limited. A commissioned Haivian review can be third-party to the research producer; it is not external journal peer review or institutional accreditation.
Guidance
Understand the result before commissioning it.
Does a Lean proof mean a mathematical paper is correct?
Separate kernel acceptance from formalization faithfulness and paper-wide correctness.
How to independently verify an AI-generated Lean proof
A practical sequence for source freezing, builds, assumption inspection and claim review.
Lean proof verification vs mathematical peer review
Compare the questions, evidence and limits of two different review processes.
Pricing and intake
Start with one defined claim.
The current initial Research Audit is US$1,499. Scope, toolchain availability and supplied artifacts determine the accepted plan. A separate US$1,000 publication-audit stage is available only after eligibility; it is not included automatically and does not guarantee publication.
Send the exact manuscript version, repository or archive reference, target theorem names, Lean/Lake versions, build instructions and the decision the audit must support. Do not send passwords or private-repository tokens through the general enquiry form.