Foundation0
Menu

Circuits · Swapnil Jain’s repository · Aska contributed

Beating a 1937 recipe, eventually

An AI-assisted proof claims that a basic operation on bits, the one that turns a logic function’s table of answers into its formula, can be done with fewer XOR gates than Frank Yates’ 89-year-old method. The catch: the win appears only at sizes no computer will ever see.

Not peer reviewed · AI-refereed only Main theorem not in Lean Asymptotic only repo at 00ffede · checked 14 Oct 2026

Swapnil Jain’s repository and claim. Aska Digital contributed one piece: our agentic team, run by founding member Ahraz Arifuddin (GitHub ahrazzle), wrote and ran the full-network check of the “E1” gadget that Theorem 2 depends on. It ran every invocation at sizes h = 8, 9 and 10 and a symmetry-reduced run at h = 11, found zero failures, and showed that two deliberately broken versions fail as they should. Swapnil Jain merged it as pull request #1 on 11 October 2026.

RepositoryWritten proofAska’s PR #1On the Ledger

Pascal’s triangle, odd entries lit

How to read: row n lists the number of ways to choose r things from n. A lit cell is odd. Point at a cell, or focus the figure and use the arrow keys.

Rows //
Each doubling of the rows repeats the picture three times around a hole: the Sierpinski triangle.Computed in your browser. Rule: C(n, r) is odd exactly when every 1 in r’s binary digits is also a 1 in n’s (Lucas, 1878; cited in the repository’s NOTICE).
Show rows 0–15 as digits
row  0: 1
row  1: 1 1
row  2: 1 0 1
row  3: 1 1 1 1
row  4: 1 0 0 0 1
row  5: 1 1 0 0 1 1
row  6: 1 0 1 0 1 0 1
row  7: 1 1 1 1 1 1 1 1
row  8: 1 0 0 0 0 0 0 0 1
row  9: 1 1 0 0 0 0 0 0 1 1
row 10: 1 0 1 0 0 0 0 0 1 0 1
row 11: 1 1 1 1 0 0 0 0 1 1 1 1
row 12: 1 0 0 0 1 0 0 0 1 0 0 0 1
row 13: 1 1 0 0 1 1 0 0 1 1 0 0 1 1
row 14: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
row 15: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1

1 = odd, 0 = even. Row 15 is all odd because 15 is 1111 in binary: every r below 16 fits inside it.

  • 4.37 × 10−11
    how far below 1 the claimed exponent drops: N·(log N)θ′ with θ′ = 1 − 4.3713·10−11 (Theorem 2)
    README.md · Lean bound in Prepass.lean
  • 0 / 3,456,000
    failed checks in Aska’s full-network run at h = 10 (all 43,200 invocations)
    run_e1_rep_h10_bad0.txt
  • 92
    supporting theorems checked by Lean and axiom-audited; the main theorem is not one of them
    lean/axioms.out
  • ~4.4 × 1010
    digits the number k needs before the new circuit beats Yates (Theorem 2, constant ratio 84)
    README.md crossover table
  • 0
    human referees so far; AI referees read it (2 for Theorem 1, 1 each for Theorems 1′ and 2)
    docs/RESULT.md

00//The problem

First principles

One bit for every combination.

Take k pizza toppings. There are 2k ways to choose some of them. Give each choice one bit, 0 or 1. Now ask, for every choice: do the bits on it and on all of its smaller choices add up to an odd number or an even one?

With three toppings a, b and c there are N = 8 choices: none, a, b, ab, c, ac, bc, abc. The answer for “ab” looks at the bits of ab, a, b and none, adds them, and keeps only odd or even. The list of all N answers is called the Möbius transform over GF(2), also the zeta, subset-parity or Sierpinski transform.

Why care? This transform turns a logic function’s table of answers into its formula (its “algebraic normal form”), which is how cryptanalysts read a cipher’s building blocks. It sits inside Reed–Muller error-correcting codes and inside fast algorithms that sum over subsets. And it is one of the simplest places to ask a deep question: can letting things cancel ever save work?

Draw a grid with one row per output and one column per input, and put a dot where the column’s toppings are all inside the row’s. You get Pascal’s triangle with its odd entries lit: the picture at the top of this page. That is Lucas’s theorem of 1878 in action.

The obvious method adds up every sub-choice separately. That costs 3k − 2k XORs. In 1937 the statistician Frank Yates found the recipe everyone still uses: handle one topping at a time. For each choice that has topping t, add in the value of its twin without t. That is k passes of N/2 XORs each, ½ N log2 N in all, drawn below as a “butterfly”.

Below: pick k, change the input bits, and step through Yates’ passes. The outputs always match the grid.

Pascal’s triangle mod 2 is the transform; Yates’ butterfly computes it

How to read: left, the top strip is the input bits and the right strip the outputs; each grid row adds up (XOR) the inputs in its lit cells, and bright cells are the ones that count. Right, the same outputs built one topping per pass; every is one XOR gate. Filled dot = 1, hollow = 0.

Yates' butterfly for the current inputs.
k //
Inputs //
Yates’ butterfly12 XORs
Every sub-choice separately19 XORs
k = 3, N = 8: all 3 passes done, 12 XOR gates. The outputs match the grid.Computed here. Counts k·2k−1 and 3k − 2k as in docs/CLOSED_IDEAS.md (L(M3) = 12; 192 at k = 6).
Show the numbers
XOR gates for the transform on N = 2k inputs
kN inputsYates’ butterfly k·2k−1Every sub-choice separately 3k − 2kLit cells in the grid 3k
12113
24459
38121927
416326581
53280211243
664192665729
71284482,0592,187
82561,0246,3056,561
95122,30419,17119,683
101,0245,12058,02559,049
112,04811,264175,099177,147
124,09624,576527,345531,441

The separate method needs one XOR fewer than the number of lit cells in each row, so its total is 3k − 2k. Yates’ total grows like ½ N log2 N; the separate method like N1.585.

01//The open question

89 years of Yates

Without cancellation, nobody can do better. With it, nobody knew.

A circuit “cancels” when the same input reaches a gate along two paths, so it adds in twice and disappears, because x  x = 0. Yates’ butterfly never does this. Is that a weakness, or the best there is?

In 2012 and 2013 Joan Boyar and Magnus Gausdal Find proved that if a circuit is not allowed to cancel, ½ N log2 N gates is exactly the minimum for this transform: Yates cannot be beaten on those terms. They then asked to what extent cancellation can help. For the smallest sizes they checked by computer that it does not help at all.

In 2024 Igor Sergeev still listed “can it be done in fewer than n·2n−1 gates?” as an open problem. The best proven lower bound is only about 3N, so the true answer could sit anywhere between 3N and Yates’ ½ N log2 N.

  1. 1878

    Édouard Lucas: a binomial coefficient is odd exactly when its binary digits nest. Both of the claim’s parity tricks use it.

  2. 1937

    Frank Yates’ recipe: k passes of N/2 XORs.

  3. 2012–13

    Boyar and Find: optimal without cancellation; does cancellation help? (arXiv 1207.5321, 1305.3041)

  4. 2024

    Sergeev lists the question as open; lower bound (3 − o(1))·N (slides).

  5. 6 Oct 2026

    OpenAI publishes a manuscript (dated 25 Sep), produced by an internal OpenAI model, that beats n log n for the exact complex Fourier transform (openai/math problem 130).

  6. 11 Oct 2026

    Swapnil Jain publishes mobius-x1, a claimed yes for bits. Aska’s full-network check is merged the same day.

Where the true answer could sit

How to read: gates per input for a transform of N = 2k inputs. Yates’ recipe costs ½ k per input; the best proven lower bound is about 3. The true minimum is somewhere in the shaded gap, which widens as k grows.

Size //
Inputs N = 2k
1,048,576
Yates, ½ N log2 N
10,485,760 gates
Proven lower bound, about 3N
3,145,728 gates
For N = 2 to the 20, Yates needs 10 gates per input and the best proven lower bound is about 3 per input; nobody knows where between them the true minimum sits.Yates’ count: k passes of N/2 XORs. Lower bound (3 − o(1))·N, as listed by Sergeev (2024), so “about 3” holds for large N. The claim on this page would sit just under Yates, and only for astronomically large N (section 04).

02//Garbage that erases itself

The clever part

Add it twice and it is gone.

The new circuit borrows helper wires that already hold leftover values, lets that junk flow into the answer, then sends the same junk in a second time so that it cancels. What remains is exactly the signal, and every helper wire ends where it started.

The figure runs the claim’s eight-row “gadget” on single bits. Four wires: x is the value to deliver, y the place to deliver it, and A and c are helpers holding unknown junk a0 and c0. Each row adds one wire into another, if its switch is on.

Rows 0 and 1 pour junk into y. Rows 2 and 3 load x into the helpers. Rows 4 and 5 pour the helpers into y again: the junk arrives a second time and vanishes, and x arrives along each route that is switched on. Rows 6 and 7 take x back out of the helpers.

So the whole trick rests on one count. If x reaches y along an odd number of routes, y gains x. If the count is even, x cancels too and nothing is delivered. Switch both routes on to watch the gadget fail.

The eight-row gadget, on bits

How to read: time runs left to right; each column is one row of the schedule, adding the dotted wire into the wire. Below, the terms each wire holds now. A struck-out term arrived twice and cancelled.

Four wires x, y, A and c, with eight gates in time order.
Routes //

RG + JV = 1 (odd). y ends as y0 + x; both helpers are restored.

Schedule from the repository’s checker x1_e1_rep.c (rows 0–7) and PROOF.md Lemma 2.1′.
Show the eight rows as text
  1. Row 0: y += J·A
  2. Row 1: y += R·c
  3. Row 2: A += V·x
  4. Row 3: c += G·x
  5. Row 4: y += R·c
  6. Row 5: y += J·A
  7. Row 6: c += G·x
  8. Row 7: A += V·x

Choosing the centre: Lucas again

In the strongest version (Theorem 2, the “E1” gadget) every label is a set of 7 points out of h, and the shared centre wires are all the 3-point sets. Two labels S and T that overlap in n points share every 3-point set inside the overlap: C(n, 3) wires. The gadget needs that count to be odd when S = T, so a label’s own data survives, and even for unrelated labels, so their data cancels.

C(n, 3) is odd only at n = 3 and n = 7. That is Lucas’s rule from the triangle above: 3 is 011 in binary, and only 3 (011) and 7 (111) contain it. Overlaps that are a multiple of 3 are what the proof calls neighbours; there an odd count is allowed but must be patched by a side wire (the J route). With this centre only overlaps of exactly 3 need one, and fewer side wires mean a better exponent.

Swap in 2-point sets as the centre and an overlap of 2 gives C(2, 2) = 1, odd, between unrelated labels: junk leaks into the answer. Aska’s check ran that broken version on purpose, and it failed in 277,200 places.

Two labels on a ring of 12 points

How to read: outlined points are label S (fixed); filled points are label T. Turn T, or press points to move them. The panel counts the centre wires S and T share, and whether that count is allowed.

  • S · fixed label, 7 points
  • T · movable label, 7 points
T // Centre //
Rules from PROOF.md Lemma 10.1, proved in Lean for every finite set (LucasE1.lean); control from run_e1_rep_h12_bad2.txt.
Show every overlap
Shared centre wires for two 7-point labels overlapping in n points
nKind of pair3-point centre C(n,3)Verdict2-point centre C(n,2)Verdict
0neighbour0 evenfine0 evenfine
1unrelated0 evencancels0 evencancels
2unrelated0 evencancels1 oddleaks: fails
3neighbour1 oddside wire3 oddside wire
4unrelated4 evencancels6 evencancels
5unrelated10 evencancels10 evencancels
6neighbour20 evenfine15 oddside wire
7same label35 oddsignal survives21 oddsignal survives

03//The claim

Claimed · AI-refereed only

A machine built for complex numbers, rebuilt for bits.

The claim is that the transform needs only about N·(log N)θ′ XOR gates with θ′ a hair below 1, which is eventually smaller than Yates’ ½ N log2 N. Here is how it is built, in five steps.

  1. 1

    Borrow an AI-found machine

    A preprint dated 25 September 2026 and made public on 6 October in OpenAI’s openai/math collection (problem 130), “produced by an internal OpenAI model”, beats n log n for the exact complex Fourier transform. Its recursive network saves a tiny fraction of steps at every level; recursion compounds that, and the exponent drops below 1.

  2. 2

    Flip the arithmetic

    Complex numbers do not exist among bits, so Jain swaps the roles: labels are counted mod 3, and data live in F4, a four-element number system with a cube root of one, ω. The 3×3 building block becomes C′ = ωI + ω2J3.

  3. 3

    Make the junk cancel by parity

    The centre is chosen with Lucas’s theorem so that every unwanted contribution arrives an even number of times: the gadget in section 02.

  4. 4

    Remove a correction step

    A cheap relabelling applied on both the input side and the output side replaces one correction step per bank entry, doubling the saving. A one-sided version fails: it works for 0 of the 42 test lines checked.

  5. 5

    Come back to bits

    An explicit 12-slot “word” writes two levels of the transform as a product of copies of the building block over F16, and every F16 gate costs at most 28 XORs. So a fast C′ gives a fast Möbius transform. Lean checks that the word’s 27 factors, 12 of them copies of the building block, multiply out to exactly two levels of the transform.

F4: four numbers, two bits each

How to read: the four numbers of step 2 are 0, 1, ω and ω2. Adding two of them is XOR on their 2-bit codes; multiplying by ω turns 1 into ω, ω into ω2, and ω2 back into 1. Press “× ω” to go round; “Show bits” writes every number as its code.

Current number

1

code 01

Start at 1. Three presses of × ω bring it back: ω3 = 1.

Addition: XOR of the codes
+000101ω10ω211
000000101ω10ω211
101101000ω211ω10
ω10ω10ω211000101
ω211ω211ω10101000
Multiplication
×000101ω10ω211
000000000000000
101000101ω10ω211
ω10000ω10ω211101
ω211000ω211101ω10
Ctrl //
ω is a cube root of one: ω3 = 1, and 1 + ω + ω2 = 0, so ω2 = ω + 1. Because addition is XOR on two bits, every F4 sum is two XOR gates, and the complex-number machine of step 1 can be rebuilt from bits.The standard arithmetic of the four-element field, as used in PROOF.md; the tables are the whole of it.
Three versions of the claim, all under the same recursion (README.md)
VersionGadget1 − θ′Best label size hWho refereed it
Theorem 14-point labels, centre of all sets of size ≤ 2, one correction step per bank entry1.8309·10−15922 AI referees: “confirmed with fixes”
Theorem 1′the same, with the two-sided relabelling instead of the correction4.2213·10−1351relabelling: 1 AI referee
Theorem 2 (E1)7-point labels, centre of 3-point sets, side wires only where needed, with the relabelling4.3713·10−11231 AI referee; Aska’s full-network check

Source: README.md headline table. The Lean package proves each exponent’s numeric bounds, for example 1 − θ′ ∈ [4.37127524, 4.37127525]·10−11, but not the network argument that makes them meaningful. A faster recurrence that would give about 3.98·10−9 is a conjecture, unproved, and nothing depends on it.

Who did what

People

  • Swapnil Jain · author of the repository, the claim and its three versions; chose to publish it as “checked by AI agents only, not human-refereed; asymptotic only”.
  • Ahraz Arifuddin · oversaw Aska’s agentic team that wrote the full-network check (section 05).
  • No human referee yet. The repository asks for one, for this work and for the OpenAI preprint it rests on.

Machines

  • An internal OpenAI model produced the Fourier-transform preprint whose architecture the claim transplants.
  • Claude (Anthropic) assisted the research, implementation and drafting, per the README: “AI assistance is not independent review.”
  • Unnamed AI agents wrote and refereed the proofs: 2 referees for Theorem 1, 1 each for Theorems 1′ and 2.
  • Lean 4 checked 92 supporting theorems: the numbers, both parity centres, the 12-slot word and 26 deliberately false variants, each refuted.
  • Aska’s agents wrote and posted PR #1, “automated posting by agentic team with human oversight”. Which model ran it is not stated.

04//How far away is “eventually”?

The honest scale

Right, perhaps, and still slower on every computer that will ever exist.

“Asymptotically fewer” means fewer once the input is large enough. The new circuit carries a bigger constant cost, and its advantage over Yates grows like k1−θ′, which with 1 − θ′ = 0.0000000000437 barely grows at all.

Write the new circuit’s cost as c0 times Yates’, divided by k1−θ′. Here k is the number of toppings and c0 the ratio of the two methods’ constant factors; the repository works out c0 = 84 for its explicit word and also reports 2 and 106 as brackets. The new circuit wins once k1−θ′ passes c0. Slide to find where.

The new circuit’s cost as a multiple of Yates’, as the problem grows

How to read: left to right, k gets more digits (each grid step is a hundred times more digits). Above the “break-even” line Yates is cheaper; below it the new circuit wins. Both scales are logarithmic.

Cost ratio stays near the constant c0 until k has billions of digits, then falls below 1.
Version // c0 //
Computed here from 1 − θ′ and the crossover rule log10 k ≈ log10 c0 / (1 − θ′), which reproduces the README’s crossover table (PROOF.md §8). “No feasible size beats Yates, and nothing is witnessed at any feasible size” (README).
Show the crossovers
Digits k needs before the new circuit beats Yates (log10 k)
c0Theorem 1Theorem 1′Theorem 2
21.6·10147.1·10116.9·109
841.05·10154.6·10124.4·1010
1063.3·10151.4·10131.4·1011

From the README’s crossover table. These are numbers of digits of k, not values of k. The input size N is 2k, a number whose own digit count has billions of digits.

Where 4.37 × 10−11 comes from: the best gadget size

How to read: each column is one label size h. Its height is the saving in the exponent, 1 − θ′; a × on the floor means the gadget costs more than it saves at that size. The highlighted column is the best. Point at or focus a column for its numbers.

Exponent saving by label size h.
Version 2 (E1): no saving below h = 20; the best is h = 23. At h = 24 the count of roles must be padded up to the next power of 3, and the saving drops by two thirds.Computed here with exact whole numbers from the formulas in x1_theorems.py; the best values and thresholds match the repository’s log run_theorems.txt. The version buttons above switch this chart too.
Show the numbers

The table appears when JavaScript runs.

05//Aska’s part

Contributed · merged PR #1Finite sizes only

We ran the whole network, and it held.

Before our check the README said plainly: “No full 7-set network has been run.” Our agentic team wrote x1_e1_rep.c, which runs the entire E1 network as plain bit arithmetic with random values on every wire, and checks that every value lands where the proof says it should.

Aska’s runs of the E1 network (all logs in the repository)
Label size hWhat was runSwap checksFailures
8all 192 invocations1,0240
9all 3,888 invocations93,3120
10all 43,200 invocations3,456,0000
11one representative invocation per stage, by symmetry*1,9800

* At h = 11 one invocation per stage stands for all of them, by the symmetry argument of PROOF.md Remark 5.2; its 2,980 labels and 3,000 edges were also solved by brute-force linear algebra, with 0 failures. Source: certificates/run_e1_rep_h{8,9,10,11}_bad0.txt. Foundation0 rebuilt the checker on 14 Oct 2026 and reproduced all four logs byte for byte (h = 10 took 33 s, h = 11 took 526 s). That is the same code run again, not an independent check.

  • Two deliberately broken versions fail, as they should. A wrong label in row 5 gives 22,146 nesting failures at h = 11; the 2-point centre from section 02 gives 277,200 wrong entries at h = 12.
  • The step count is exact. Counting every step and weighting by symmetry gives the proof’s closed formula at every size: 5,190,901,996,500 steps at h = 11, on both sides.
  • Merged and credited. Swapnil Jain merged it the same day: “Thank you, this closes the full-network gap for Theorem 2 nicely, with both controls refuted.” The README now credits ahrazzle. 1 of the repository’s 6 commits, +500 lines (8% of its current lines).

At h = 11, about one pair of labels in nine needs a side wire

How to read: each bar counts ordered pairs of different labels by how many points they share. Only an overlap of exactly 3 needs a side wire (section 02). Point at or focus a bar.

Overlap 3: 11,550 pairs; overlap 4: 46,200; overlap 5: 41,580; overlap 6: 9,240.
First line of run_e1_rep_h11_bad0.txt: 108,570 ordered pairs (330 labels × 329).
Show the numbers
Points sharedOrdered pairsShareSide wire?
311,55010.6%yes
446,20042.6%no
541,58038.3%no
69,2408.5%no

06//Status and sources

As of 14 Oct 2026

What is proved, what is checked, and what is only claimed.

LayerStatusHow
Main theorem: network lemmas, recursion, transfer to bitsClaimedWritten proof with every step tagged; refereed only by AI agents; not in Lean; no human referee
Numeric core of all three versionsLean-checkedExact values, padding, sign ranges, exponent bounds
The two parity centres (Lemmas 1.2 and 10.1)Lean-checkedProved for every finite set
The 12-slot F16 wordLean-checkedPlus two independent Python checks
The network at small sizesComputer-checkedExact runs to h = 10 (Theorem 1) and h = 11 (E1, Aska’s check)
Counts at the real sizes (h = 23, 51, 92)Re-derivedFrom a formula; the README says this is not independent evidence
NoveltyAbout 90% confidentThe author’s literature search found no earlier claim below ½ N log2 N for circuits that cancel

Source: README.md §2, lean/axioms.out (92 theorems, standard axioms only, no sorry), docs/NOVELTY.md. Foundation0 re-ran the Python certificates and Aska’s checker on 14 Oct 2026; we did not re-run the Lean build, so its status rests on the committed audit.

The repository

Aska’s contribution

Context

Numbers, formulas and the gadget schedule on this page come from Swapnil Jain’s mobius-x1 (Apache-2.0, © 2026 Swapnil Jain), with the E1 check by ahrazzle. The figures are new code written for this page; they re-compute the repository’s formulas and do not copy its source. The repository has no project website, PDF or DOI; the figures here are new code written for this page.