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 Oct 11, 7:04 AM PT. The verifier’s own words: “Lean and nanoda passed; permitted-axiom audit passed”.

Rows that use this check

Fourier Transform: $O(n \log^{1-1.022\cdot 10^{\scriptstyle -3}} n)$ , by Nil Mamano

The statement: The Lean file challenges/dft/UniformFourier233.lean states the problem. A proof counts only if it proves exactly this statement. Its checksum is 3a646acd3ac9. It comes from commit fd4aeeb2ee4f of the statement’s source repository.
The proof: Source repository bigospeedrun/verifier at commit f9ffbc1f9dfb, folder submissions/dft/nmamano-dft-record. The theorem checked: Race.bound.
Comparator and the Lean kernel: Both accepted the proof. Comparator is the Lean community tool that checks a proof against a fixed copy of the statement. The Lean kernel 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 proof uses only propext, Classical.choice, Quot.sound.
Lean version: leanprover/lean4:v4.34.1