What was already known
The textbook transform uses N log₂ N operations. Coppersmith, Feig and Linzer’s 1994 multiply-add construction uses (7/8) N log₂ N at powers of four, with an extra N/8 at odd powers of two. Sussman’s original 11 October note gives the new circuit; revision 2 adds its complete Lean checking report on 22 October.
AI involvement
Jacob Sussman directed the project. Claude agents wrote and ran the searches that found the retained circuits and wrote their proofs. The new sharing pattern and recursive circuit are the retained AI construction; the older Coppersmith–Feig–Linzer four-point step is credited separately.
Importance
Provides an explicit recursive circuit with a smaller leading operation count in this fixed model.
Limitations
This is a constant-factor bound, not a sub-N-log-N algorithm or an optimality result. A multiply-add counts as one line; charging each scalar multiplication separately changes the bound. The separate 5/6 arithmetic-operation theorem, asymptotic power-saving projects, hardware measurements and processor timings are outside this assessed contribution. Priority over the complete hardware literature remains unestablished.
Technical verification
The project reports successful Lean 4 builds and standard-axiom checks for the exact all-powers-of-two theorem on 22 October. Its separate, agent-written comparison script matches the statement and its definitions to the proof. This is a reported project check, not an outside researcher audit or a run reproduced here.
Formal checking
Revision-2 report: complete all-powers-of-two theorem, standard axioms, statement comparison and negative controls; the comparison tool is the project’s own, distinct from the official Comparator.
- Checker
- Sussman project: Lean 4 / Mathlib
- Scope
- For every commutative ring R and every k≥0, the exact, unscaled Walsh–Hadamard transform on N=2^k inputs has a straight-line circuit with at most (3/4) N log₂ N + N/4 lines. Each line creates u+c·v or c·v−u from available values, with a fixed ring constant c, and costs one. Reuse, output selection and permutations are free.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-22
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. The author says no person has read the Lean files or checked the written arguments line by line. The released explanations were also written by agents. A named human account of the retained recursive mechanism is not documented.
Correction and publication history
Added the 22 October Lean checking report for the exact multiply-add circuit bound.
Read this published revisionRecorded the original 11 October circuit construction and its finite exact checks. Complete all-size Lean checking is documented separately.
Read this published revision