Academic papers are in a sense a compiled rendering, capturing particular views of the underlying process of discovery. Using them, the structure is lost in favour of prose and presentation. This made sense in a human-dominated science paradigm.
This mode of communication however does not transfer well in an era in which, powered by agents, it’s possible to produce hundreds of ground breaking results in a very short period of time. With Flywheel, we propose a natural paradigm to support highly asynchronous intelligence being poured, at scale, on solving difficult scientific problems.
In Flywheel, claims and the evidence supporting them are the main unit being recorded in a Directed Acyclic Graph (DAG). This simple structure allows us to create granular surfaces capable of supporting weakly communicating swarms of agents working asynchronously, while recording the entire trajectory of their work, including negative results.
This also makes it much easier for humans to make sense of what happens: results are organized following the logical trajectory they were proposed with, allowing us to understand recurring patterns and structures between successful traces. It also makes it much easier to extend, reproduce or critique existing work, by simply branching off of a result and proceeding with one’s own.
We ported the OpenAI’s recent 721 paper math corpus to Flywheel. This is our first field-scale graph, going beyond the single paper and covering part of mathematics. It has 7,095 nodes, each statement linked to what it relies on, its source lines and its Lean file. You can find it here.
Expressing the corpus this way makes it easier to work with. More than half of the papers cite another paper in the corpus. In the graph those citations are links, so you can follow a lemma straight to the companion paper that proves it. Each statement points to its source lines and its Lean file, so a reviewer can check a single claim, and see what is formalized, without reading the whole paper. Anyone, human or agent, can branch from one node to extend or challenge it, and their work sits next to the original instead of in a separate PDF. We made the broader case for this in an earlier post.
We propose that organizing work into a Flywheel graph also presents the opportunity for delegation. We ran Simplex, our internal meta-harness, on the graph in three arrangements with the objective of discovering new findings or identifying issues with the original corpus.
This follow-up work so far has found 46 improved results accompanied by one negative result, with various combinations of multi-agent work between Claude Opus 5.5, GPT 6 Astra, GPT 6.1 Sol and Limite 1B Violetto. For each result, we specifically check for the presence of a written proof, exact-arithmetic checks, and independent re-derivation. Here are four of the results; each one is written up in full further down this post.
One OpenAI paper looks at two ways of measuring how a Boolean function reacts when you flip its input bits. It proves that one can grow like the other raised to some power above 2, but never says which power. We give an explicit one, 181/90, higher than the paper’s own argument reaches (write-up 01).
Another paper builds a special kind of group, an Artin group, that can’t act nicely on the curved spaces geometers usually use to study groups. Its example uses 116 generators. Ours uses 24 (write-up 02).
One finding goes the other way, finding a false claim. A paper on the Navier–Stokes equations, which describe how fluids move, claims that a standard step, removing the part of a force that would compress the fluid, keeps the rate at which the force fades. Read literally, that is false: we found a force where the rate is lost (write-up 04).
All three are also checked in Lean on top of OpenAI’s own Lean project, with no gaps and no extra assumptions (1, 2, 3).
In a separate run, a larger model wrote the proofs and our own small model, Limite 1B Violetto, computed the exact values they use. That run improved bounds in four more OpenAI papers; one of them, on two-way automata, is write-up 03.
| OpenAI manuscript | Stated there | Here | Lean | |
|---|---|---|---|---|
| 01 | A superquadratic separation between sensitivity and block sensitivity | some exponent above 2 | 181/90 | yes |
| 02 | An Artin group with no geometric CAT(0) action | 116 generators | 24 generators | yes |
| 03 | An exponential state lower bound for two-way nondeterministic complementation | ½·2^⌊(n−4)/127⌋ − 1 | ½·2^⌊(n−4)/d*⌋ − 1, with 54.46 < d* < 54.47 | no |
| 04 | Prefix Instructions and Incompressible Flows | decay bounds are preserved | false at the same order | yes |
Today the graph is public: 721 papers, 7,095 nodes, and 66 follow-up results so far, with their proofs and checks attached. We’re still running on it, and new results go into the same graph as they land. Point your agents, your agent systems or a plain swarm at it and work next to us.
Science has shipped as manuscripts for centuries. Let’s see what a field looks like when everyone builds on the same graph. The four write-ups follow.
An explicit exponent for sensitivity
OpenAI’s manuscript proves that an exponent above 2 exists. We give one: 181/90.
Sensitivity and block sensitivity are two ways of measuring how strongly a Boolean function reacts to changes in its input. Sensitivity counts the single input bits whose flip changes the output. Block sensitivity counts disjoint groups of bits whose flip changes it, so it is never smaller.
The manuscript A superquadratic separation between sensitivity and block sensitivity (25 September 2026) builds functions whose block sensitivity grows faster than the square of their sensitivity. Its Corollary 4.3 says there is an exponent α > 2 with bs ≥ sα for a sequence of such functions, but it never states a value for α. Using the manuscript’s construction unchanged, we give one: α = 181/90 ≈ 2.011.
What makes this possible is a size threshold. The manuscript’s key lemma needs a size parameter M ≥ 9d+1 at depth d. We show that the same lemma already holds for M ≥ Kd, with Kd ≤ 81·3d, at most 27 times the square root of the old threshold. That smaller size lets the depth-20 construction certify 181/90. Under the old threshold no depth certifies more than about 2.0065.
The statement
C_j = Σ_{i<j} 3^⌊i/2⌋, D_d = d + 3·Σ_{j<d} C_j, K_d = max(32·D_d, (2·D_d + 1)²)
1. For every M ≥ K_d the manuscript's construction satisfies
S_(ℓ,b) ≤ 2(d+2)·M^(ℓ+b) for 0 ≤ ℓ ≤ d, b ∈ {0,1}.
2. K_d ≤ 81·3^d and K_d < 9^(d+1) for every d ≥ 1.
3. With d = 20 and M = K_20, the functions F_m built by the manuscript's
composition satisfy bs(F_m, 0) ≥ s(F_m)^(181/90) and bs(F_m, 0) → ∞.
Part 1 is the manuscript’s Lemma 4.1 with the hypothesis M ≥ 9d+1 replaced by M ≥ Kd. Part 3 makes its Corollary 4.3 explicit.
Why the threshold drops
The manuscript tracks two kinds of sensitivity profile through the levels of its construction, and replaces the two joint profiles by their maximum. We keep them apart. After normalizing by powers of M, they feed each other through the matrix T = [[0, 3], [1, 0]], and T² = 3I. A factor of 3 is paid once every two levels instead of once per level, so the accumulated error term Dd grows like 3d/2 and the threshold (2Dd + 1)² like 3d, not 9d.
The exponent certificate
At depth 20 with M = K₂₀, the seed function f has sensitivity at most A = 44·M²¹ and block sensitivity at zero at least B₀ = 2²⁰·M⁴². The integer comparison ⌊B₀⁹⁰ / A¹⁸¹⌋ = 8374 > 1 gives bs(f, 0) ≥ s(f)181/90, and the manuscript’s composition lemma carries this to every Fm. The check uses integer arithmetic only.
Checks, Lean and limits
A separate derivation eliminates one joint component and recovers the same recurrence. An independent check showed that under the manuscript’s threshold the best exponent any depth certifies is about 2.0065, so 181/90 does depend on the smaller threshold.
The Lean theorem LeanWell.SensitivityThreshold.main proves all three parts.
It uses the manuscript’s recurrences, labelling and composition results as
formalized in OpenAI’s Lean project. An audit of its 64 declarations found only
Lean’s three standard axioms and no sorry.
Kd is a sufficient size, not claimed minimal. 181/90 is what depth 20 certifies, not the limit of the method: depth 21 would give about 2.0114.
Result: node and full write-up · Lean: Threshold.lean · Manuscript: openai/math
An Artin group on 24 generators
OpenAI’s example has 116 generators. Ours has 24.
An Artin group is given by generators and a table that says, for each pair, whether they commute (label 2), satisfy a braid relation (label 3), or have no relation (label ∞). Groups that act geometrically on a CAT(0) space, a space of nonpositive curvature, inherit a lot of structure, so it matters which Artin groups do.
The manuscript An Artin group with no geometric CAT(0) action (23 September 2026) gives an Artin group on 116 generators, with every label 2, 3 or ∞, that has no geometric action on any CAT(0) space. We give one on 24 generators with the same kinds of labels, again in any dimension.
The manuscript’s argument runs three blocks of braid relations through a fixed three-generator group, and it needs a strict inequality between lengths in each block. It gets that inequality from braid groups on 40 strands. We get it from 10 strands, with an exact identity between the centers of nested braid groups. That gives 26 generators. Reusing the last braid generator of two blocks as the two extra generators the argument needs brings it to 24.
The ten-strand identity
Suppose a group acts geometrically and contains s1, …, s9 satisfying the relations of the braid group on ten strands. Write ℓ for stable translation length, Zr for the center of the first r strands, and W = Z₉⁵·Z₁₀⁻⁴. Then
ℓ(W)² + ℓ(Z₁₀)² = 300·ℓ(Z₃)² − 675·ℓ(s₁²)²
If ℓ(Z₁₀) > 0, the right side forces ℓ(Z₃) / (3·ℓ(s₁²)) > ½, the strict ratio the manuscript’s triangle obstruction needs. In our group Z₁₀ is a word of 90 positive letters, so its exponent sum is 90, it has infinite order, and under a geometric action its length is positive.
Why changing the manuscript's parameter is not enough
The manuscript’s own length estimate exceeds the needed ¼ only with at least 28 strands per block, which already means 80 generators. At ten strands it gives 1/36. Going below 80 needs a different length argument, which the identity above supplies.
Checks, Lean and limits
The matrix was rebuilt independently by gluing the presentations of the pieces and agrees on all 576 entries. The identity was derived a second time by a different route. The embedding argument was checked on all 720 placements of three selected strands among ten, and the common centralizer of d and e was proved again with a single element.
The Lean theorem LeanWell.Artin24.main proves the 24-generator theorem with
no remaining hypotheses. It uses the manuscript’s triangle obstruction as
formalized in OpenAI’s Lean project. An audit of its 287 declarations found
only Lean’s three standard axioms and no sorry.
We do not claim that 24 is the minimum. The triangle obstruction is the manuscript’s, used unchanged.
Result: node and full write-up · Lean: Artin24.lean · Manuscript: openai/math
A larger lower bound for two-way automata
The denominator of the exponent drops from 127 to about 54.46, with exact values computed by Limite 1B Violetto.
A two-way nondeterministic finite automaton reads its input with a head that can move in both directions, and may guess. The question here is how many states an automaton needs to recognize the complement of a language that an n-state automaton recognizes.
The manuscript An exponential state lower bound for two-way nondeterministic complementation (25 September 2026) builds, for every n ≥ 4, an n-state automaton whose complement needs at least ½·2⌊(n−4)/127⌋ − 1 states. We prove the same with 127 replaced by a constant d* between 54.46 and 54.47. At n = 600 the bound goes from 7 states to 511.
The manuscript’s induction passes, at each of t² steps, to a smaller instance of one fixed size. Ordering the steps by rows and keeping every row and column not yet used lets step (i, j) keep h − i − j + 1 points instead of h − 2t + 1. Summing these unequal costs gives a weighted recurrence, and d* is its exact growth rate.
This result comes from a separate run. A frontier model, GPT-6.1 Sol, planned the argument and wrote the proof. Along the way it sent short calculation questions to our own model, Limite 1B Violetto, each answered by 24 independent copies. Two of Violetto’s answers are steps of the final proof, and the proof model checked both with exact arithmetic before using them.
| Question to Violetto | Copies that answered | Answer | Role |
|---|---|---|---|
| Largest set of row and column points that keeps the current pair and no earlier pair | 22 of 24 | 2t − i − j + 2 | step of the final proof: the size of the smaller instance |
| Closed form of Σi,j≤t r−(i+j−1) | 24 of 24 | r(1 − r−t)² / (r − 1)² | step of the final proof: its root defines d* |
| Smallest t with the sum ≥ 32t at r = 81/80 | 1 of 24 | 79 | gave the first improved proof, with denominator 63 |
| Two thresholds for a rounded version of the sum | 24 of 24 each | 85 and 76 | confirmed exactly, not used in the final proof |
| Six further questions | 0 of 24 | none | not used |
The statement
Let ρ > 1 solve Σ_{i,j≤99} ρ^−(i+j−1) = 32·99, that is (ρ^99 − 1)² = 3168·ρ^197·(ρ − 1)²,
and put d* = log 2 / log ρ. Then 54.46 < d* < 54.47, and for every n ≥ 4 every
two-way automaton for the complement has at least ½·2^⌊(n−4)/d*⌋ − 1 states.
In particular ½·2^⌊2(n−4)/109⌋ − 1 for every n ≥ 4, and ½·ρ^(n−4) − 1 for n ≥ 69.
The automaton family, the language and all state conventions are the manuscript’s. Its diagram lemmas are used as stated.
Checks and limits
The retained-set formula was checked by exhaustive enumeration for t ≤ 6, and separately for t ≤ 5. ρ was bracketed between 1.012808132687 and 1.012808132688 with exact rational sums, and the bounds on d* follow from integer comparisons. The starting cases of the induction are certified by exact integer rows, and the recurrence was run out to size 600. A separate Claude Opus agent re-derived the proof line by line from the manuscript and wrote its own exact-arithmetic scripts.
The result is not in Lean and has one independent check. d* is the exact limit of this row-order recurrence; we make no claim about other orders of the steps or stronger diagram inequalities.
Manuscript: openai/math · The four results of the Violetto run are not yet in the Flywheel graph.
A projection that loses a decay rate
A proposition says that a standard step keeps decay bounds. Read literally, it does not.
The Navier–Stokes equations describe how a viscous fluid moves under a force. A standard step in their analysis on a torus removes the gradient part of the force, the part that would compress the fluid. What is left is a divergence-free force that drives the same flow.
Proposition 2.4 of the manuscript Prefix Instructions and Incompressible Flows (27 September 2026) says that this step preserves several kinds of bounds on the force, among them “orderwise decay bounds”. Read as a statement about a decay rate at one derivative order, it is false. We give a smooth force on the unit three-dimensional torus whose size is at most a constant times 1/(1+t), with every derivative bounded and decaying, while the projected force is not bounded by any constant times 1/(1+t).
The proof in the manuscript bounds each derivative of the projected force by derivatives of the original force five orders higher. That cannot carry over a rate known only at the original order, and the example uses exactly this gap. None of the paper’s main theorems are affected: the proposition is used in three places, and each use needs only boundedness or periodicity.
The construction
Fₙ(θ) = Σ_{k≤n} sin(kθ)/k bounded by 1 + π for all n
Gₙ(x,y,z) = (0, Fₙ(2πx)·Fₙ(2πy), 0) bounded, smooth, mean zero
Sₙ = Σ_{k,l≤n} 1/(k² + l²) ≥ Hₙ / 2 → ∞ first component of the projection
at the origin
g(t) = Σₙ Tₙ⁻¹ · b(t/Tₙ − 1) · Gₙ, Tₙ = 2ⁿ, b a smooth bump on [−¼, ¼]
The pulses do not overlap, so g is smooth, and ‖g(t)‖ ≤ (7/4)(1+π)²/(1+t), about 30/(1+t), at every time. At time Tₙ the projected force equals Sₙ/Tₙ at the origin, so (1+t) times its size is at least Sₙ, which is unbounded. The potential is unique, so the failure does not depend on a choice of potential.
OpenAI's corrected statement
The same proposition, with the same proof, appeared in the first edition of OpenAI’s Incompressible Box Transport and Finite Computation. Its 6 October revision replaces the clause: qualitative decay passes in general, and a quantitative rate at output order r passes when the input has that rate through order r + 2. Our example agrees with the corrected statement, since its higher derivatives decay only like (1+t)−3/4.
Checks, Lean and limits
The construction was checked with exact symbolic computation, and a verifier
built it a second time through a stream function, without the submitted
potential. The whole construction is in Lean, in four files joined into one;
the statement ¬ SameOrderPreservation is proved, together with the force’s
smoothness, mean zero, uniqueness of the potential, bounds on every derivative
and computability at rational points. An audit of the 277 declarations found
only Lean’s three standard axioms and no sorry.
The manuscript does not define “orderwise decay bounds”. A reading that allows its five-derivative loss is not refuted, and qualitative decay survives. The example lives on the unit torus. The full meaning of “effective” is only partly formalized.
Result: node and full write-up · Lean: Effective.lean · Manuscripts: Prefix, Box, 6 October
How the results were produced
In the Flywheel graph each manuscript is split into linked nodes for its theorems, lemmas and corollaries. Agents can then be handed one statement and its neighbours instead of a folder of PDFs, and what they find is written back next to the statement it improves, with its proof and checks attached.
Results 01, 02 and 04 come from runs of gpt-6-astra agents inside our
meta-harness on 7 November 2026, on revision fd4aeeb2 of the corpus. Results
01 and 04 came from a swarm of independent scouts; result 02 came from a
hierarchy of a director, area leads, hunters and verifiers. Result 03 comes
from the separate run described in section 03. A result from these runs was
accepted only with all of the following.
- A1. A written proof of the claimed improvement or failure.
- A2. Check scripts in exact arithmetic or exact symbolic computation.
- A3. An independent re-derivation by a separate verifier, and a second read by Claude Opus.
- A4. Afterwards, for 01, 02 and 04, a Lean proof written by Claude Opus agents and compiled by a separate checker against the Lean project that ships with the corpus.
The runs on 7 November recorded 46 positive results, 19 minor ones and one negative result. All of them are in the Flywheel graph, tagged with the agent roles that worked on them.
Each result is compared only with the statement in the OpenAI manuscript it starts from. Full write-ups, check scripts and Lean files are attached to the result nodes.
References
- OpenAI (2026). A superquadratic separation between sensitivity and block sensitivity. 25 September. openai/math.
- OpenAI (2026). An Artin group with no geometric CAT(0) action. 23 September. openai/math.
- OpenAI (2026). An exponential state lower bound for two-way nondeterministic complementation. 25 September. openai/math.
- OpenAI (2026). Prefix Instructions and Incompressible Flows. 27 September. openai/math.
- OpenAI (2026). Incompressible Box Transport and Finite Computation. Revision of 6 October. openai/math.
Citation
The post:
@misc{paradigma2026fieldscale,
title = {{Building a Field-scale Flywheel graph for mathematics}},
author = {Baslak, Muhammed Emin and
Starace, Giulio and Pappone, Francesco},
year = {2026},
howpublished =
{\url{https://paradigma.inc/blog/field-scale-research/}}
}
An explicit exponent for sensitivity:
@misc{paradigma2026sensitivity,
title = {{An explicit exponent for sensitivity}},
author = {{Paradigma}},
year = {2026},
howpublished =
{\url{https://paradigma.inc/blog/field-scale-research/#write-up-01}}
}
An Artin group on 24 generators:
@misc{paradigma2026artin24,
title = {{An Artin group on 24 generators}},
author = {{Paradigma}},
year = {2026},
howpublished =
{\url{https://paradigma.inc/blog/field-scale-research/#write-up-02}}
}
A larger lower bound for two-way automata:
@misc{paradigma2026automata,
title = {{A larger lower bound for two-way automata}},
author = {{Paradigma}},
year = {2026},
howpublished =
{\url{https://paradigma.inc/blog/field-scale-research/#write-up-03}}
}
A projection that loses a decay rate:
@misc{paradigma2026projection,
title = {{A projection that loses a decay rate}},
author = {{Paradigma}},
year = {2026},
howpublished =
{\url{https://paradigma.inc/blog/field-scale-research/#write-up-04}}
}