THE FUTURE PAGE

[ Front page ] [ The edge ] [ Finished ] [ About ] [ Links ]

The latest reading, written down 2026-10-24.

Theorems a computer has checked

291,178 theorems

Held by Mathlib, the Lean 4 mathematical library. Set 2026-10-23, and has stood for 4 days.

Every other number here that touches mathematics measures a machine trying to find an answer. This one measures a machine refusing to take one on trust. A formal proof is mathematics rewritten so that a program can check every step down to the axioms, with nothing left to a reader's judgement about which lemma is obvious, and the checking is the whole point: the program that does it is small enough to audit and knows nothing whatever about the subject. The cost used to be the entire objection. A page of a textbook could take a week, and for fifty years, from Automath in the sixties through Mizar and the theorem provers of the eighties, the method was plainly sound and plainly useless at scale. What changed is not the checkers but the library. Every theorem formalised stays available to the next one, so the work compounds instead of being redone, and arguments that once needed building from the ground up now rest on lemmas already present. That is what this count really measures: not how clever anyone has been, but how far the usable floor has risen. In 1993 the field's achievements were single theorems, announced one at a time, each one a project. Two things are worth knowing about the figure. It is one library in one language, and the rival systems are not in it. And unlike every other record on this page it is not held by a machine or bought by a laboratory - it is ordinary work, done largely by volunteers, visible commit by commit, and the thing being counted is the part a computer agreed to.

That description was written when this frontier was opened, on 2026-10-07, and is never rewritten. Where it and the number above it disagree, the number is the reading and the description is history.

[ The whole history of this number ]

The edge today

• The longest task an AI can finish on its own — 1,045 minutes
• Open problems in mathematics solved — 4.4 per cent
• Unsolved integer sequences worked out — 29.9 per cent
• Real software issues resolved — 83.5 per cent
• Questions answered without inventing an answer — 76.0 per cent
• Chess puzzles solved — 76.0 per cent
• The largest training run ever disclosed — 9 x 10^26 operations
• The largest training cluster ever disclosed — 200,000 chips
• The fastest computer on earth — 2,198 petaflops
• The most arithmetic per watt — 73.282 gigaflops per watt
• The largest prime number ever found — 41,024,320 digits
• The largest quantum volume — 8,388,608 quantum volume
• The smallest a gigabyte of Wikipedia has ever been made — 91,778,237 bytes
• The most data ever read and written in a second — 26,888 gibibytes a second
• The most connections ever followed in a second — 410,266 billion edges a second
• The most digits of pi ever computed — 314,000,000,000,000 digits
• The highest rating any chess program holds — 3,650 Elo
• The most transactions a database has ever run in a minute — 2,055,076,649 transactions a minute
• The most storage operations ever done in a second — 30,002,765 operations a second
• Assembly mistakes spotted in a photograph — 83.3 per cent
• Programs rebuilt without seeing the code — 77.4 per cent
• The most ordinary work one computer can do — 1,660 times the reference machine
• The most questions ever answered against a hundred terabytes of data — 653,611,141 queries an hour
• The least time ever taken to train a four-hundred-billion-parameter model — 7.07 minutes
• The most tokens a seventy-billion-parameter model can produce in a second — 1,136,100 tokens a second
• Theorems a computer has checked — 291,178 theorems
• The most arithmetic ever sustained on scattered data — 22.0 petaflops
• The fewest mistakes a machine makes transcribing a meeting — 6.08 per cent of words wrong

Watching 28 frontiers. 6 others have finished.   [ The full table, with dates ]

The rules

• Every number here carries a date and a place anyone can check it.
• When a number moves, the old one is kept. Nothing is edited or deleted. A script enforces this.
• A number nobody can check is not published.
• Every page on this site is a single document smaller than 14,336 bytes.

Written down in:   2026

When a number moves it appears in the feed. Nothing else on this page can reach you again.

[ Front page ] [ The edge ] [ Finished ] [ About ] [ Links ]