The Cost of the Project

This page accounts for what the project consumed: first in tokens, then in dollars. The token figures follow the definitions of the published token audit: processed tokens count all logged fresh input, cache creation, cache reads, and output, while the non-cache subtotal excludes cache reads. Cache reads dominate every agentic total below, so the two numbers differ by more than an order of magnitude; neither measures unique semantic content. Measured figures come from session logs; where a provider hides usage (ChatGPT Pro in the browser), the audit estimates it from recorded thinking time and states the range.

Cost in tokens

The work divides into six categories: David Turturean’s conversations finding the presentation, his Lean formalization, David Roe’s separately developed Lean formalization, Roe’s cleanup of the finished Lean repository, Roe’s follow-up campaign formalizing the square-commutator presentation, and Roe’s work on this website and PaperForge.

1. Finding the presentation. The successful candidate and natural-language proof campaign ran June 18–26 on ChatGPT Pro in the browser, with a small Codex lane and an Opus 4.8 controller. Because OpenAI does not expose historical hidden-reasoning usage for ChatGPT Pro, the audit reconstructs it from 41.9 recorded hours of thinking time at 100–500 hidden tokens per second: about 327 million processed tokens, with an estimated range of 305–365 million. A non-cache subtotal is not meaningful here, since the browser interface exposes no cache accounting.

2. Turturean’s formalization. Turturean’s continuous Codex/GPT workflow, ChatGPT Pro consultations, and later Claude work measured 9.57 billion processed tokens (324.0 million excluding cache reads) in session logs. Adding the estimated hidden reasoning behind his ChatGPT Pro formalization consultations (24–121 million tokens, central estimate 61 million) gives roughly 9.63 billion processed and 348–445 million excluding cache reads.

3. Roe’s formalization. The twenty archived Claude Code sessions of Roe’s one-week formalization measured 9.23 billion processed tokens and 237.7 million excluding cache reads (6,918 Fable 5 and 12,762 Opus 4.8 API calls), the figures pinned in the published token audit. A fuller recount for this page, which also sweeps every background subagent transcript and the Haiku 4.5 housekeeping calls the audit omitted, reaches 9.44 billion processed and 256.7 million non-cache; the same fuller method produces the totals for categories 4 and 5.

4. Lean cleanup. After the proof was complete, Roe ran a cleanup effort on the repository July 11–26: style and documentation passes over every file, splitting the six largest files, relicensing, axiom reduction, and responses to external review. The 7 sessions, published as records in the cleanup corpus, measured 1,049,991,865 processed tokens (78,528,519 excluding cache reads). Most of the work ran in swarms of parallel subagents, which the ledger includes.

5. Square-commutator formalization. When GPT 5.6 produced a proof note for the square-commutator candidate (the presentation Fable 5 had proposed in early June), Roe ran a second, smaller formalization campaign July 24–26 to verify it in Lean: the replacement theorem over the new source, the agreement of the two admissible-marking semantics, and the in-repo proof of the required Labute-classification instance, ending with the unconditional GQ2.main_presentation_literal_roe_unconditional now cited in the paper’s Appendix C. Its 6 sessions measured 1,258,420,413 processed tokens (53,183,297 excluding cache reads), again mostly in parallel-subagent swarms.

6. Website and PaperForge. Roe’s work on this site and on PaperForge (the paper pipeline, the development record, the interactive pages, and this cost accounting itself) spans 20 sessions from July 8 onward and measured 1,672,989,483 processed tokens (49,758,838 excluding cache reads). This category is a moving snapshot: sessions were still active when the ledger was generated at 2026-07-27T06:56:43Z, and the numbers grow as the site does, including by the act of writing this page.

One conversation predates all six categories: Roe’s own exchange with Fable 5 (June 9–July 2), which produced a first candidate presentation that passed his finite-quotient verifier along with a partial proof, and which was set aside when Fable was withdrawn on June 12. It measured 109 million processed tokens and is counted in no category above.

Downloads

• Token audit (CSV): the published accounting for categories 1–3; its definitions, exclusions, and estimation method are recorded inside the JSON.
• Research conversation records: every published record outside the three session corpora (445 records: the search, the June campaign behind category 1, and the separate manual conversations), bundled byte-identical from the site’s per-record files.
• Per-session ledger (CSV): deduplicated per-session token totals for categories 3–5, generated for this page: dates, models, API calls, and token sums per session, subagent transcripts included.
• Turturean’s formalization archive: the published record corpus behind category 2.
• Roe’s formalization archive: the twenty full session logs behind category 3, lightly redacted, hosted on MIT.
• Roe’s cleanup archive: the sanitized assistant-message extraction behind category 4.

Cost in dollars

It is difficult to translate the token usage above into a dollar figure, for several reasons. Both authors had subscription accounts, and David Turturean also had support from Fulcrum for providing API credits. If you just directly translate the token usage into API credits, the presentation and informal proof would have cost roughly $7,000 and the formalizations would have cost roughly $30,000 (both of these numbers have quite a bit of variance; the largest single uncertainty is the rate attributed to ChatGPT Pro’s hidden reasoning, which is not billed or metered per token in the browser). The two later categories are smaller: at current Claude list prices the cleanup sessions translate to roughly $1,800 of API usage and the website and PaperForge work to roughly $2,300 more.

However, the authors did not spend nearly this much, for two reasons. First, fully utilizing a subscription provides vast leverage: you can run several parallel lanes using GPT Pro in the browser without being rate limited, and there is no overall usage cap. Indeed, you can run 2–3 parallel sessions on GPT 5.5 Pro and roughly 6 parallel sessions on GPT 5.6 Pro. The coding agents (Codex and Claude Code) do have overall usage limits, but if you use them to the maximum extent, the number of tokens available in a Pro/Max20 subscription is far more than the API credits you could buy with the cost of the subscription.

The other reason that it is difficult to translate token usage into dollars is that the authors prioritized finding results in a short overall time (partly due to the lack of clarity on the availability of Fable 5), and would have needed fewer subscriptions if they had drawn out the project over months rather than weeks.

With optimal usage drawn out over more time, this work could have been accomplished by one month of a GPT Pro subscription and one month of a Claude Max20 subscription, for a total cost of $400. The actual amount spent by the authors was roughly $6,000: one GPT Pro subscription for $200, three Claude Max20 subscriptions for $600, and roughly $5,000 of Fable API tokens. All of these costs were covered by David Roe’s SSRFA grant from the Simons Foundation and David Turturean’s support from Fulcrum.

Efficiency in retrospect

This analysis was prepared by Claude Fable 5 from the per-session ledger above and the project’s session transcripts; call counts refer to the July 24 snapshot.

Where the tokens actually went. In every agentic category, model output is 0.5–1% of the processed total and cache reads are 92–97%. The bill was not for writing proofs; it was for holding long-lived contexts warm. Roe’s formalization made 21,852 API calls averaging roughly 430,000 processed tokens each, nearly all of it the same repository context, ticket boards, and conversation history re-read from cache on every call. Turturean’s Codex lanes have the same shape (about 98% of GPT-5.6 input was served from cache). Efficiency here means context discipline, not terser answers.

Small fresh contexts beat large persistent ones. The cleanup phase ran as an orchestrator dispatching per-file workers that started fresh, did one job against a tight brief, and reported back; its average call carried about 160,000 processed tokens, versus 430,000 in the formalization’s long-lived lanes, a 2.7× lighter context per call. The formalization’s hardest design work genuinely needed shared context, but a larger share of its well-specified tickets could have run worker-style from the start, and that is the single largest token saving we can identify in hindsight.

Parallelism paid twice for coordination failures. Six simultaneous lanes each carried a copy of essentially the same repository context, and when the shared ticket board went stale the lanes did overlapping work: on July 7 the tree was compiling with two sorry placeholders left while the board still listed open tickets, and two lanes raced to fill neighboring fields of the same structure. Cheap, frequent, automated status sweeps computed from the compiler’s ground truth, rather than from anyone’s bookkeeping, would have kept the lanes from re-deriving each other’s state. Related version-control losses (a harness reset that discarded uncommitted edits, an over-broad git add) turned hours of work into re-spend; commit-immediately-after-green and one-new-file-per-lane conventions cost nothing and would have prevented all of it.

Unattended runs must be unattended-safe. One overnight cleanup run stalled for five hours on a permission prompt no one was awake to answer. Under subscription pricing the scarce resource is wall-clock, not tokens, so every idle hour of a paid-for lane is pure loss; pre-approving the expected command surface before leaving a run alone is the fix.

Route work down-tier by default. The project already routed by difficulty: design-heavy tickets to Fable 5, well-specified ones to Opus 4.8 (13,103 and 7,716 calls respectively in the formalization recount), housekeeping to Haiku 4.5 (1,033 calls). The cleanup phase showed the mechanical end of the spectrum runs fine on delegated workers. Pushing lint fixes, file splits, and documentation passes further down-tier, with escalation only on failure, is cheap to try and easy to reverse.

Define what “done” means before opening a long lane. The one lane that consumed serious tokens without a durable result was the 161-response attempt to compare the two presentations, which ended only when a checker asked for calculation records produced independently of the proof narrative and none could be supplied. Stating that acceptance test in the first message, not the last, would have either produced the records or ended the lane a hundred responses sooner.

What we would not economize. The redundancy that looks most expensive on this page (two separately initiated formalizations, fresh-context adversarial reviews, exhaustive finite-quotient testing) is what made the result trustworthy, and the reviews in particular were among the cheapest line items per unit of value: A2’s fatal flaw and the manuscript’s false proposition were both found by short review threads, not by the long lanes that built them. Between finding the presentation (≈327 million tokens) and certifying it (≈19 billion), certification dominated by a factor of nearly sixty; if anything, the efficient move is to spend more of the budget on early, cheap refutation so that expensive certification only ever runs on statements that survive it.