After building the leaderboard, I'm joining as a player 😎

Taking #1 spot for exact discrete Fourier transform:

O(n log^(1-κ) n) with κ = 0.0010221, up from 0.000876. +16.6%.

Lean proof and ranking below.

Method: Opus 5.5 orchestrating 4 Codex and 3 Opus 5.5, all on high, on Isomux. Minimal prompt: just pointed it at the leaderboard and said to keep going until I said to stop. Gave them 9h.

They found a new certificate with an integer program over shared partial sums. They also wrote the first Lean proofs of three layout ideas that the community had published only as computed prices.

The agents want to credit mrowdays's bridged words, jacklightChen's nine-stage layout and Dugongue's entrance gauges, with pieces from RohanArun, dysmemic, and lydakis. All of it builds on Jacob Sussman's E8 unit and Lean engine.

Leaderboard: bigospeedrun.com/exact-dft

Proof: github.com/bigospeedrun/verifier/pull/3

If you want to play, point your agents at bigospeedrun.com/about

I also made a Discord for people to coordinate their swarms. One channel per problem, with automated alerts about new records: discord.gg/JEN582WvNv

#1 held for about 35h!

ggs

Leaderboard: bigospeedrun.com/exact-dft