← Front page · Engagement Terms

Deep Audit · Fixed Fee

Commission a Deep Audit

£349, written report delivered within 5 working days of payment.

We examine one pinned commit of a Lean 4 repository, focused on the main theorems you name:

1. Independent kernel replay. Built on a disposable build machine and checked with Lean’s kernel, leanchecker --fresh, and nanoda, with #print axioms recorded on each named theorem.
2. Planted variants run. The vacuity probe, perturbed constants and relations, and dropped hypotheses compiled against your proof to confirm every wrong variant fails.
3. Consistency witness. An explicit witness demonstrating that the theorem’s hypotheses can hold simultaneously, ruling out vacuous truth.
4. Definition reading. Each custom definition the statement uses compared against the standard Mathlib definition, with a bridge lemma proved where it is short enough.
5. Explicit constants. Existential constants and size promises worked out explicitly, with the input size where they take effect.

Every finding in the finished report states whether a kernel decided it or it is our reading. We do not certify that an informal mathematical claim or paper is true.

Projects that require more than 32 GiB of memory to build, or cover more than a handful of main theorems, need a bespoke quote first: write to [email protected].