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 10, 8:35 PM 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-8.762\cdot 10^{\scriptstyle -4}} n)$ , by jacobalansussman

The statement: The Lean file challenges/dft/UniformFourierE8.lean states the problem. A proof counts only if it proves exactly this statement. Its checksum is 71db0509bf31. It comes from commit fd4aeeb2ee4f of the statement’s source repository.
The proof: Source repository jacobalansussman/wht-power-saving-lean at commit 9c94857bbaee. The theorems checked: OAI.PowerSaving.transform_mainE8, OAI.PowerSaving.convolution_mainE8.
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