Community research maintained by Douglas Colkitt — conditional on the original OpenAI #109 framework.
The composition of DreamingOfClouds' #276 and Rohan Arun's #279 gives
DreamingOfClouds redesigned the local bit circuits to use fewer auxiliary registers. Rohan reassigned 880 mixing gates to their existing common delivery frames, applying eumemic's earlier retiming technique. The composition retains Henry Grant and Jacob Sussman's five-stage construction, Evan McKinney and Rohan's completed banks, Chafik Boukhalfa's physical checkers, Avi Eisenberg's complex supplier and the earlier community framework.
This is 1.90% above the recently audited 0.000710046193349537 witness,
and 56.99% above 0.0004609169. It is approximately 2^-10.43258.
These compare exponent savings, not practical runtime. The all-size compiler,
chart, routing, restored-row, precision/recovery and analytic interfaces remain
conditional. Finite replay and written review do not prove the complete
asymptotic theorem in Lean.
Review and validation scope · Selected record · Construction argument · Exact certificate · Integration checks · Contributor record
python3 -m pip install -r research/five-stage-gen4-banks/requirements.txt
make gen4-bank-verifyeumemic's #210,
pinned at 298f7c1, gives the conditional witness
κ = 710046193349537 / 10¹⁸ = 0.000710046193349537.
This is the intermediate result announced before the gen4 update above.
Its complete source package and audit are now preserved on main; the newer
gen4 result remains selected.
The construction combines internal response cancellations and source reuse with Henry Grant and Jacob Sussman's five-stage geometry, Evan McKinney's completed-bank method and Rohan Arun's width-120 banking work. Chafik Boukhalfa's physical helper/checkers, Avi Eisenberg's complex helper, Dugongue's refinements and Romyxen / sennemmi's operation frames remain credited in the source notices. All eight mandatory finite stages passed, with every one of the 121 pinned inputs unchanged. The retained all-size interfaces remain conditional.
Checkpoint and publication review · Exact certificate · Construction source · Full round-nine review
python3 -m pip install -r research/five-stage-source527-banks/requirements.txt
make source527-verifyDugongue's #186 gives the conditional witness
The construction combines Chafik Boukhalfa's shared-edge complex supplier (#181) with eumemic's physical bit word and searched modules (#168), then coordinates operation frames and completes shared entrance banks. The bank scheduling supplement supplies a conflict-free schedule and its additional finite prime exclusions. The source package, dependency notices and assistance disclosures are preserved.
This is 43.60% above the preceding published saving, and 40.18% above
the intervening reviewed recycled-bit checkpoint. It is approximately
2^-10.56113; a factor 2.95085 remains to 2^-9. These compare asymptotic
exponent savings, not measured runtime speedups. The retained analytic,
uniform-recursion and fixed-tape hypotheses remain assumptions. Finite replay
and written review do not formally verify the multiplication theorem.
Review and validation scope · Selected record · Construction argument · Exact certificate · Integration checks · Contributor record
make entrance-bank-verifyThe composition of #147, #150, #146 and #148, built on icekylinx's #144 construction, gives the conditional witness
William Porter (hpst3r) eliminates unused terminal accumulators; DaysSky schedules dirty reads later and reuses dead bit registers. Thomas Marchand (Th0rgal) contributes the selected gauge subset and Rohan Gupta (gupt1156) the tighter stopping parameter. SovereignSteak's #151 independently composes the same gauge refinement and recycling, and supplies the further atom tightening used here. The composition retains the actual complete word, exact restoration and every frame transition. James Chang's compensated birth-read reuse and SovereignSteak's terminal-elimination mechanism are explicit dependencies. All prior construction and framework credits remain.
This is 2.44% above the preceding reviewed saving. It is an asymptotic exponent improvement, not a measured runtime speedup. The retained analytic, uniform-recursion and fixed-tape hypotheses remain assumptions.
Review and validation scope · Selected record · Construction argument · Exact certificate
make recycled-bit-verifyThe construction contributed by icekylinx in PR #144, building on PR #130, gives
A signed paired-cube producer and coordinate-star centers complete the identity using the original source registers. Completed dirty cores reuse one auxiliary bank across three orthogonal blocks, adopting an664's PR #128 sharing principle. The bit branch selects certified gauges from the retained PR #97 / Swapnil word. All local transitions, copied centers, complement calls, finite routers and rare-class fallback remain charged. The analytic, uniform-recursion and fixed-tape hypotheses are retained.
This is 9.03 times the preceding reviewed main saving, approximately
2^-11.0832: above 2^-12 and below 2^-11. It measures the asymptotic
exponent saving, not a practical runtime speedup.
Maintainer review and validation scope · Current result record · Proof source · Exact certificate · Incremental reproduction
make paired-cube-verifyThe construction contributed by icekylinx, extending PR #115, gives
Three signed shears on a regular Cayley cover align all interstage data frames. The complex branch combines eumemic's PR #117 local DAG with arbitrary-subspace Clifford frames; the bit branch retains the PR #97 / Swapnil physical word and uses a batched weighted q-adic cover. Local transitions, copied centers, rare-class fallback, finite routers and internal row borrowing are charged. The retained analytic and fixed-tape hypotheses still apply.
Proof source · Exact certificate · Incremental reproduction
make three-stage-cover-verifyThe construction contributed by icekylinx, extending PR #104, gives
It applies the stopped whole-projector bit interface to the physical deferred word of Zhihao Chen's PR #97, based on Swapnil Jain's witness. The new complex producer combines cyclic interval contractions, pair-first cube assembly, compatible frame enlargement and partial source gauges. Every residual, endpoint correction and target-data transition is charged. The bound retains the analytic and fixed-tape hypotheses of the preceding construction.
Proof source · Exact certificate · Incremental reproduction
make partial-gauge-verifyThe new construction contributed by icekylinx, extending merged PR #36, gives
It combines a stopped product-ring bit interchange on (23,23) with an
all-disjoint rational-center complex network on (24,24). The new generic
opposite-bank factorization pays one reversed child per projector rank;
atom adapters, ordinary leaves, endpoint copies and the exact denominator-21
grid are included in the proof. The bound retains the original analytic
and fixed-tape hypotheses.
Proof source · Exact certificate · Incremental reproduction
make stopped-product-verifyThe maintainer-reviewed community checkpoint below remains its own result and validation record.
The reviewed community witness gives
This is 23.71% above the preceding PR #49 release and remains below 2^-14. It is an improvement in the asymptotic exponent saving, not a measured runtime speedup. The model and general reduction are inherited from OpenAI's Integer multiplication below n log n.
Maintainer review and contribution ledger · Finite circuit proof · Selected parameter certificate · Independent arithmetic check
Avi Eisenberg's interval strips and core-aware pair assembly (#62) arrange additions to allow more physical wire reuse. Combined with eumemic's joint frame compiler (#57), this yields the strongest finite network in this batch. Alejandro Zarzuelo Urdiales's exact parameter refinement and scoped Lean certificate (#61) supply the selected numerical value.
The bit network has m=575 and 137,151,806 physical roles; its certified recursive saving is 102039046058023/2000000000000000000. The complex network retains saving 717/10^7. All recursive children, workspace restoration, copied centers and endpoint costs remain charged. The seven final exponent margins are strictly positive.
The preceding combination of Avi's skip-prefix strips (#53), Rohan Gupta's dual-suffix layout (#55), eumemic's compiler and Chafik Boukhalfa's composition and ranked reclamation (#58/#60) is also fully retained and reviewed.
Other reviewed contributions are retained even when their numerical witnesses are superseded: RaD's enlarged-frame and clone machinery (#51), Rohan Arun's positive-frame composition and order searches (#52/#56), Rohan Gupta's parallel order search (#50), Chafik's original-envelope clones (#54), and Rohan Garg's split-pair recursion (#59). The review records the exact validation scope of each.
The current #186 construction is contributed by Dugongue, building on Chafik Boukhalfa/chafreaky (#181/#175), eumemic (#168), and the cumulative framework and physical-word lineage. The contributor ledger also credits reviewed parallel work, including Rohan Arun’s #185 bootstrap and Chafik’s #182 refinement, without adding their gains to this witness.
Newly incorporated contributions include DaysSky (#150), William Porter / hpst3r (#147), Thomas Marchand / Th0rgal (#146), and Rohan Gupta / gupt1156 (#148), building on James Chang / jamesyc (#124) and SovereignSteak (#122). Andrew Barnes / Bortlesboat (#101) strengthens physical-word verification using rfu08's counterexample. rfu08 (#64) contributes the separately scoped formal-transfer and finite-audit package. See CONTRIBUTORS.md for their roles and the retained credits.
The names below identify GitHub contributors; they are not verified Twitter handles.
- Avi Eisenberg (ikeboy): skip-prefix and interval strips, core-aware pair assembly (#53, #62).
- Rohan Gupta (gupt1156): dual-suffix strips and parallel order improvements (#50, #55).
- eumemic: joint frame compilation and paid reclamation (#57); earlier complex circuits, Gaussian resampling and source frames.
- Chafik Boukhalfa (chafreaky): exact recovery, independent checkers, reordered sums, paid clones and joint-compiler composition/refinement (#43/#46/#48/#54/#58/#60).
- Rohan Arun (rohanarun): corner geometry, fixed-basis composition, weighted matching, order searches and positive-frame composition (#49, #52, #56).
- Rohan Garg (rohangar1): split-pair recursion, order refinement and paid-clone composition (#59).
- Alejandro Zarzuelo Urdiales (alejandrozu): Gaussian parity and finite tensor proofs, matrix/search tools, exact refinement and scoped Lean arithmetic (#45, #61).
- RaD project (hipotures): semantic precision, routing, phase-cell inversion, bulk resampling, alternating producers, physical compiler and enlarged-frame/clone machinery (#41, #51).
- icekylinx: stopped recursion, three-stage covers, weighted local-ring compilation, paired-cube construction and the selected integration (#104, #115, #130, #144); earlier batching, partial swaps and copied centers.
- an664: completed-core workspace sharing (#128), a substantial dependency of the current result.
- eumemic: the restricted positive producer used by the paired-cube construction (#117), alongside the earlier work credited above.
- Zhihao Chen and Swapnil Jain: the deferred physical bit ledger (#97) and underlying frozen word and lifted frames used by the selected bit construction.
- Zhihao Chen (jacklightChen): controlled bases, translated frames, semantic/bulk compatibility and two-stage integration.
- James Chang (jamesyc): reversed two-stage geometry and exact controls.
- Aurel Prosz (Paureel) and Swapnil Jain: attributed two-stage development and paid copied-stream endpoints.
- Dominik Scholz: dimension, parameter and fixed-basis refinements.
- Ryan S (princezuda): historical Lean certificates, algebraic contracts and independent circuit checks (#26).
- Andrew Barnes (Bortlesboat) and David Leen (dleen): aligned pairing, retained totals and sharing.
The full contribution record credits incorporated, parallel, superseded and pending work separately. Douglas Colkitt maintains the project, original research, review and integration, with OpenAI Codex assistance. OpenAI's original manuscript and Harvey–van der Hoeven's analytic work retain their attribution. Contributor-specific AI disclosures remain in NOTICE.
The round-two review extends the previous follow-up audit and PR #39 transfer review. The original #109 framework and retained all-size interfaces remain assumptions. This is not full formal verification, independent human peer review, a worldwide priority claim, or a practical multiplication benchmark.
Fresh checks cover complete emitted words and dirty basis vectors, physical frame transitions, exact fixed-basis profiles, all 4,073,300 data pairs for the retained geometry, and independent rational recurrence/assembly arithmetic. The formal packages verify their stated finite/arithmetic contracts. PR #61's integrated axiom audit contains 169 distinct declarations, including 11 concrete frontier theorems; its input rows are bound to the replayed finite profile. They do not formalize the whole multiplication algorithm.
The review receipt distinguishes fresh maintainer checks from contributor-supplied evidence. Earlier witnesses, patches and attribution remain available. Submissions after #62 are outside this checkpoint's review; exact reviewed heads are recorded in the ledger.
make verify-pair
make verify-joint
make verify-positive
make formal-matrix-verify
# Complete arithmetic, producer, historical and unit-test suite:
make verifyPython 3.11+, a C++17 compiler and Boost headers are required for the full arithmetic suite. The formal targets use their pinned Lean versions. See reproduction details and CI layout.
Each patch applies independently to the unmodified pinned source; they are alternatives, not a sequence to apply together. The result history records the earlier mechanisms and scoped ceilings. The preserved research index collects the intermediate compression, routing, Fano, and core searches, including scoped negative results and reproducible certificates.
| Patch | Conditional saving | Scope |
|---|---|---|
| frozen-154 | 2^-154 |
Original network and recurrence exponents |
| balanced-153 | 2^-153 |
Balanced assembly parameters |
| same-network-129 | 2^-129 |
Original network, sharper recurrence comparison |
| h46-111 | 2^-111 |
Smaller network, dyadic parameters |
| h46-109 | 2^-109 |
Rational recurrence saving, strict final margin |
| h46-108 | 2^-108 |
Variable stopping exponent |
| h46-rational | 5.8e-33 |
Strongest supplied parameter-only witness |
| nonadjacent-layout | Original parameters retained | Routing proof and revised layout cost only |
| frozen-nonadjacent-107 | 2^-107 |
Direct routing, original network and recurrence exponents |
| h46-nonadjacent-78 | 2^-78 |
Direct routing with the h = 46 network |
| h46-nonadjacent-76 | 2^-76 |
Direct routing with tuned dimension and stopping parameters |
| h46-shared-side-75 | 2^-75 |
Stage-1/stage-3 side-role sharing, routing, and parameter tuning |
| h46-incidence-67 | 2^-67 |
Rectangle incidence circuits, full auxiliary sharing, routing, and parameter tuning |
| h46-dag-63 | 2^-63 |
Shared intermediate sums and reversible role allocation |
| h46-shared-point | 13*2^-66 |
Cross-group sharing |
| h50-paired-59 | 2^-59 |
Paired sums, stopped guard and tighter Gaussian setup |
| compact-control-34 | 83/10^12 > 2^-34 |
Compact controls, complete reservations, local repair and separate complex arity |
| complex-compression-31 | 2^-31 |
Weighted complex circuits, binary phase frames and complete auxiliary sharing |
| ternary-30 | 2^-30 |
Ternary five-subset circuit, rational frames and fixed-alphabet interchange |
The independent rank-first pair verification and formal-transfer checkpoint record exact word/profile checks and 298 audited declarations across 27 unique Lean modules. Literal profile instantiations concern historical checkpoints, not the new selected witness. They do not verify the full multiplication machine.
Use CITATION.cff, cite the individual contributions used and include the repository version or commit. CONTRIBUTORS.md, NOTICE and source-specific manifests preserve the dependency credits.
The project is Apache-2.0. Bundled RaD sources retain their separate
CC0 license and notices. The pinned original OpenAI manuscript remains unchanged
under upstream/; its source hashes are in upstream/manifest.json.
This project is not an official OpenAI release or endorsement.