Lean proof check

Our verifier rebuilt a Lean proof from its source and checked it against the Lean statement of the problem. This page is the receipt of that check.

It passed on Nov 3, 8:36 AM PT. The verifier’s own words: “Lean and nanoda passed; permitted-axiom audit passed”.

Rows that use this check

Directed Shortest Paths: $m \le n \log^{3/4} n:\ O(n \log^{11/12} n)$ , by Vals AI

The statement: The Lean file challenges/directed-sssp/CHDRow.lean states the problem. A proof counts only if it proves exactly this statement. Its checksum is b9569daeed41. It comes from commit 98c53accb47a of the statement’s source repository.
The proof: Source repository bigospeedrun/sssp-lean-scratch at commit 98919233966f. The theorem checked: Race.bound.
The Lean kernel: The Lean kernel accepted the proof. It is the small program that checks every step of the proof.
A second kernel (nanoda): nanoda, a proof checker written separately from Lean’s own, also accepted the proof.
The axioms: The audit passed. An axiom is a statement that Lean accepts without proof. The check allows only propext, Quot.sound, Classical.choice.
Lean version: leanprover/lean4:v4.34.1