Flywheel: a claim graph for agent swarms doing mathematics

Paradigma has turned a corpus of 721 mathematics papers from OpenAI into a public Flywheel graph, and reports that its AI agents working on that graph have already improved results in some of the papers and found one claim that is false as written (Paradigma's post). Flywheel records research as claims and the evidence behind them rather than as finished papers. Each claim is a node in a directed acyclic graph, meaning every statement points to the statements it relies on and no chain of dependencies loops back on itself, so any result can be traced back to its supports. Paradigma first argued for this format with a single worked example, covered in its earlier Flywheel proposal. This release is its first graph covering part of a field instead of one problem.

The graph has 7,095 nodes. Each statement links to what it depends on, to its source lines in the paper and to its file in Lean, a proof assistant that checks every step of a formal proof by machine. Paradigma says more than half of the papers cite another paper in the corpus, and in the graph those citations become links, so a reader can follow a lemma straight to the companion paper that proves it. A reviewer can check one claim, and see whether it has been formalized, without reading the whole paper. Anyone, person or agent, can branch from a node to extend or challenge it, and that work sits next to the original rather than in a separate PDF.

To test the idea that a graph makes research easier to delegate, Paradigma ran Simplex, its internal meta-harness, on the graph in three arrangements, using combinations of Claude Opus 5.5, GPT 6 Astra, GPT 6.1 Sol and its own small math model, Limite 1B Violetto. It reports 46 improved results and one negative result so far, each checked for a written proof, exact arithmetic and an independent re-derivation. In one example, an OpenAI paper proved that one measure of how a Boolean function reacts to flipped input bits can grow like another measure raised to some power above 2, without saying which power; Paradigma gives an explicit exponent, 181/90, higher than the paper's own argument reaches. In another, a paper's example of an Artin group, a kind of algebraic group, that cannot act nicely on the curved spaces geometers usually use needed 116 generators, and Paradigma's needs 24. The negative result concerns a Navier–Stokes paper on fluid flow. The paper says a standard step, stripping out the part of a force that would compress the fluid, leaves unchanged how quickly the force fades; Paradigma says that is false when read literally, and it found a force for which that rate is lost. Paradigma says all three examples are also checked in Lean on top of OpenAI's own Lean project, with no gaps or extra assumptions. In a separate run, a larger model wrote proofs while Limite 1B Violetto computed the exact values they used, improving bounds in four more papers.

These are Paradigma's own reports, and the post describes only those three examples in any detail, pointing to its blog for more on individual results. The post also gives a total of 66 follow-up results in the public graph without explaining how that figure relates to the 46 improvements, one negative result and four further papers it describes. The Navier–Stokes finding is framed as a problem with the claim as literally stated, which leaves open whether the paper's intended argument holds. Paradigma says it is still running agents on the graph and invites others to point their own agents at it.