MATH HARNESS · EVIDENCE NOTE · OCTOBER 2026

AI math, with proofs a computer can check.

A 12-day experiment produced a general theorem verified in Lean, along with other proofs and reproducible graph searches. Inspired by frontier labs’ progress in mathematics, I started directing AI agents at open problems myself.

The math harness is the system I’m building to coordinate those agents and check their work. Erdős 585 is one worked example, and remains open.

A general theorem, verified in Lean.

The theorem gives conditions under which a bipartite graph contains a regular subgraph. In plain English: under the stated size, density, and degree conditions, a network with two groups and connections only between them contains a nonempty subnetwork where every vertex has the same number of connections.

The result covers an infinite family of graphs, rather than a finite list of examples. Lean checks the proof. The exact theorem, hypotheses, and verification instructions are in the public v0.4 release.

This does not settle Erdős 585. The theorem’s novelty relative to earlier mathematical work still needs expert assessment.

A roughly 20× faster replay

Two initial unsteered runs re-proved the same theorem, QB(4), in 30.8 and 36.6 minutes. My earlier steered run took about 12 hours elapsed, including an overnight interruption, or about 5 hours of active work. Both replay proofs passed Lean checks and a separate AI review.

That is about 21× faster by elapsed time for the initial two-run comparison, and about 9× against active time. Across all six runs, every proof passed in under an hour: 31–59 minutes, with a median of about 44 minutes.

QB(4) timing comparison: original steered run 12 hours elapsed and 5 hours active; six unsteered harness runs ranged from 31 to 59 minutes, median 44 minutes. — The six-run chart from my retrospective. Its median comparison is about 16.5× against the original elapsed time.

What the comparison measures

This was a replay of a supplied theorem statement, using different models from the original run. It measures time to a checked proof in this experiment. It does not establish a general speedup in discovering new mathematics or isolate the harness’s contribution from the model’s.

Erdős 585 remains open. The public results and verification instructions distinguish Lean-checked statements, reproducible searches, and arguments without human mathematical review.