Dots agent swarm improved a 47-year-old math bound (Lean-verified)

added Oct 6, 2026

I Used OpenAI Dots as an agent swarm to break a 47 year old math record, for free (with Lean verification of the proof)

First-hand experiment by Redditor u/jaxchang (Substack: unexcitedneurons, Oct 5 2026): ran a 7-agent swarm on their Dot's VM (9-core AMD Epyc, 10GB RAM) at $0 cost over Oct 1-3 to attack a covering-number problem. The swarm proved a contradiction showing 19 blocks of size 14 can never cover every 4-element subset of 24 points, raising the lower bound from C(24,14,4) >= 19 (Schonheim 1964 / Mills 1979) to C(24,14,4) >= 20, with the proof verified in Lean. The same argument also raised C(25,15,5) from 32 to 34. Link post to the author's own detailed writeup.