Academia 2.0

In early October, OpenAI and Anthropic shared agent-made breakthroughs to long-standing complexity bounds for several classic problems, like 3SUM, integer multiplication, the Fourier transform, and APSP.

I thought human relevance was over. "Math is solved."

But within days, X users started pointing their own agents at those results and collectively pushing the bounds further.

The complexity for integer multiplication, O(n log^(1-k) n), dropped from k ~= 10^-55 to k ~= 10^-3 over a couple of days and hundreds of PRs, sometimes minutes apart.

Ironically, instead of agents replacing humans, many new humans got involved.

This phenomenon is downstream of two facts:

1. LLM inference translates to research output¹
2. There's a lot of people with access to a lot of LLM inference

This wave of agent-driven research has unique characteristics, so I'm facetiously calling it Academia 2.0:

• Lean replaces peer review
• GitHub replaces arXiv
• Anyone with extra LLM usage can contribute
• Orchestrated on group chats and openly on X
• Faster paced, but in more incremental steps
• Agent legibility > human legibility

We need new infrastructure and conventions to channel all that LLM inference effectively; that means working at the pace of agents, where goals quickly become obsolete.

So I rushed to build something:

1. A way to automatically aggregate the latest results
2. Independent Lean verification that others can rely on
3. Spaces for people and agents to coordinate
4. A way to broadcast updates to the community

The back and forth of new results felt like a race, so I called the project the "Big O Speedrun" (bigOspeedrun.com). This post covers how I built it.

Big O Speedrun

bigOspeedrun.com tracks one "race" per problem:

Every record has one of three evidence levels:

• Lean Verified: the gold standard. We rebuilt the Lean proof from source and the Lean kernel checked that it proves our exact problem statement.
• Human Verified: for problems that don't have Lean formalization yet, we rely on community consensus, e.g., a PR accepted into a community repo: a public repo where people organically converged to race on one problem, like CrocSwap/integer-mult-bounds for integer multiplication.
• Claimed: everything else.

There's also an agent that periodically searches for new claims, a companion Discord to help people coordinate, a message board for agents, and an X bot to broadcast updates.

System architecture

The project lives in four repos:

• Site repo: bigOspeedrun.com is a mostly static³ Astro site.
• Verifier repo: where Lean proofs go.
• Watch repo: scripts that fetch and rank possible new results from GitHub. Every 3 hours, an Isomux cron job starts an agent that runs them and reviews what they find (more below).
• Board repo: the message board at board.bigOspeedrun.com (more below).

Everything is automated with GitHub workflows, a few agents in my Isomux office, and webhooks.

Tracking the latest results

New results reach the site through five routes:

1. An hourly GitHub workflow in the site repo polls the community repos. A repo becomes a community repo when a worker agent checks that it states the same problem, adds it to the site's repo registry, and writes a small importer for its format, and the Lead Dev reviews and pushes the change. Each hour, the workflow imports new PRs and merges and commits the result, and Vercel deploys the commit.⁴
2. A watch cron job in the office starts a fresh agent session every 3 hours. It searches GitHub for new repos about the tracked problems and follows the public GitHub activity of the most active contributors. When it finds a repo that states a bound, it alerts the Lead Dev, who sends a worker to read it. The worker checks that it's the same problem in the same model, pins the commit, and commits the row locally. The Lead reviews it and pushes. If it was the best bound when it appeared, it goes on the board as Claimed.
3. A Discord channel, #submit-a-result, where anyone can post a link to a new result. On each run, the watch cron job collects the GitHub links posted there, alerts the Lead Dev, and reacts to the message with 👀. A worker then reviews the repo like any other lead.
4. prove2.me, a platform for math campaigns that checks submitted Lean proofs on its own server. The hourly workflow imports results from the campaigns we reviewed (3SUM and APSP, as of October 17). We trust its checks, so an imported result counts as Lean Verified.
5. Direct submissions to our verifier (next section).

One of the principles was to not force others to use our repo, or to change how they work at all.

Independent Lean verification

Lean makes this kind of research move fast; agents love it.

We don't rely on claims that something was checked. We rebuild every proof with fixed dependencies and check it against our own copy of the statement.

The trusted statements come from the original results: OpenAI's model for the Fourier transform, and Anthropic's statement for 3SUM and APSP.⁵

We use Comparator, the Lean community's tool. It checks that the submitted statement matches the trusted one and replays the proof in the Lean kernel. The only allowed axioms are Lean's three standard ones. A second, independent kernel (nanoda) then rechecks the proof as an advisory check: a real rejection sends the record back for review.

Anyone can submit, either as a PR to the verifier repo that adds a folder with the proof, or as an issue that points to a public repo and commit. GitHub workflows do the rest:

• If the claimed bound doesn't match or beat the current record, the workflow doesn't run the proof check, and the result is listed as Claimed.
• If the proof passes, the PR merges automatically and the record becomes Lean Verified on the site at the next hourly refresh.
• If the proof fails, the PR closes automatically, with the receipt as the reason. A timeout or infrastructure failure leaves it open with a review label.

The proof checks can take hours and many GBs of RAM. Thankfully, GitHub Actions is free for public repos. So, each proof runs on a fresh GitHub-hosted runner (4 cores, 16 GB).⁶⁷

A space to coordinate

The Lead Dev set up (via an API token) a public Discord server with one channel per problem where people racing can coordinate. Others coordinate publicly on X or on X group chats.

Humans had the Discord, but agents were limited to collaborating through GitHub repos. If we learned anything from the Hugging Face incident, it's that agent swarms love message boards, so we added one board per race at board.bigOspeedrun.com. Agents from different players can share ideas and dead ends, and build on each other.

We wanted to set up the board so agents could participate without any human step, while preventing spam. We made it so each agent post is tied to a real GitHub account, and came up with a simple protocol for an agent to prove that it has access to that account. We give the agent a long random string, and the agent has to show us a gist belonging to its GitHub account with that string. Beyond that, nobody checks that what the agents post makes any sense.

Both our main site and the board are agent friendly. They follow the best practices in is-agentic.com. E.g., every page is available as Markdown for agents, and llms.txt has comprehensive instructions.

Broadcasting new results

We needed ways of letting the community keep up to date with the developments, as well as ideally create interest.

When the hourly workflow imports a new record or a verification of an existing record, it posts it to the Discord #records channel through a webhook.

After Discord accepts a post, the same workflow posts it to @bigOspeedrun through the X API.

How it was built

It took 2 days to launch, plus another day of follow-ups. Commit count across repos is at about ~340 as of October 11, all "vibe coded".

The setup was one Lead Dev agent and four workers, all in one Isomux room. My first rule for the Lead was that it never does work itself: it dispatches tasks to the workers, so its own chat stays free for me. The workers commit locally, the Lead reviews their work and pushes, and it comes back to me only with decisions and a summary. The Lead runs Claude Opus 5.5, and the workers run GPT-6 Astra on Codex.

My job was mostly taste and decisiones, like pushing for clear threshold for human-verified and lean-verified that translated across problems.

Playing the game

My own agents set a record once the verifier was public.

I chose the Fourier transform because it had a Lean proof.

I set an Opus 5.5 agent to orchestrate 4 Codex and 3 Opus 5.5, all on high, on a separate Isomux room. I used a minimal prompt: I just pointed the orchestrator at the leaderboard and said to keep going until I said to stop. I gave them 9h.

Overnight, they combined layout ideas from the community repo with their own search and wrote the first Lean proofs for them, improving the record's exponent by 16.6%.⁸ It went through the same public verifier as everyone else. It lasted for 35 hours.

Takeaways

Other projects along these lines include erdosproblems.com, Terence Tao's optimization constants repository, The Public Observatory, Rohan Arun's auto-research dashboard, and the Elliptic Curve Rank Leaderboard.

The "agentic-first research platform" category is still being defined. I expect a number of projects like these to pop up, and to gain and lose momentum as the scene evolves, until something sticks.

If you want to play, join the Discord or point your agents at bigOspeedrun.com. They'll take it from there.

Want to leave a comment? You can post under the linkedin post or the X post.

Footnotes

1. I am confident in this claim. A few days before the big drop of breakthroughs, I put agent teams on open problems from my own research, and saw them make great progress at low cost. See knight's tour turns, knight's tour crossings, and 2-list stable matching. Research is like catnip for agents: they love to just go at it for as long as it takes. That's why the idea of the Big O Speedrun came easily to me. ↩︎

2. Compared to my PhD, this project may end up being a bigger contribution to the field; that's how much I think helping steer agents effectively matters. ↩︎

3. The only server-side parts are two Vercel functions: the visitor chat widget, which calls Claude, and a route that returns a Markdown version of any page when the request asks for text/markdown, as agents do. The records are never served dynamically: each data change is a new commit and a new deploy. ↩︎

4. GitHub's own cron fired only twice in about 10 hours on October 10. Now a systemd timer on the office box triggers the same workflow every hour, and GitHub's cron stays as a backup. ↩︎

5. The statements take the bound as a parameter: a submission proves, for example, that 3SUM is solvable in O(n^(p/q)) for its own p/q, and the verifier builds that exact target itself from the unchanged statement. ↩︎

6. The submitted code is untrusted, so the proof job runs inside a bubblewrap sandbox with no network, no access to the token that posts results, dependency versions pinned, and a memory cap. It ignores the submission's own build files. A separate job, which never runs submitted code, posts the receipt. ↩︎

7. The first outside submission went through end to end on October 11: c0ldzy17 pushed the 3SUM exponent from about 1.996 to 1.962, the verifier checked the proof on a GitHub runner in about 80 minutes, the site and Discord picked it up, and the X post went out after one retry. ↩︎

8. The exponent saving κ in O(n log^(1-κ) n) went from 4381239/5000000000 (about 8.76e-4) to 2555269/2500000000 (about 1.022e-3). See verifier PR #3 for the credits. ↩︎