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, 7:25 AM PT. The verifier’s own words: “Both kernel checks passed: Lean and nanoda.”.

Rows that use this check

Fourier Transform: $O(n \log^{1-7.547\cdot 10^{\scriptstyle -4}} n)$ , by jacobalansussman, chafreaky

The proof: at commit 837dc3130adc.
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: This receipt does not record an audit. An axiom is a statement that Lean accepts without proof. The proof uses only propext, Classical.choice, Quot.sound.
What the receipt says it covers: All-positive-length exact DFT and convolution in the OpenAI family-130 exact scalar/index RAM model; transform_mainY and convolution_mainY.