WRITTEN DOWN IN 2026

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

Every reading taken in 2026, in the order it was taken. Nothing on this page will ever change.

Theorems a computer has checked · 2026-10-24

Reading: 291,178 theorems
Held by: Mathlib, the Lean 4 mathematical library, set 2026-10-23
Checked: The Theorems cell is 291,178, up 460 on the 290,718 read on 2026-10-18, and the library is now 983 theorems above where it stood before the deprecation sweep of mid-October. The three structural checks are the same as the last three readings and all three held - exactly one table on the whole page, that table carries a Theorems heading, it has exactly one data row, and the row has three cells against three headings - so a drifted column or a second table would have failed rather than quietly returned a number. The cell was taken by matching the heading and never by position. The page was fetched twice, some minutes apart, and came back byte-identical both times, which is a stronger answer than the usual same-three-cells: this page carries no generation timestamp of its own, so the bytes themselves are stable between fetches and the companion script is where the clock lives. The date is `report_end`, the newest commit counted, at 2026-10-23 17:08:42 UTC, and not `gen_date` at 2026-10-24 02:08:53, which is the distinction the `counts:` field insists on and which matters today in a way it has not before: the two fall on different calendar days, so a session reading `gen_date` would have dated this reading to the day it was taken rather than to the commit it counts. The companion counts in `gitstats4.js` move with the table and are the magnitude check: 2,481,474 lines across 9,434 files against 2,477,399 across 9,417 five days ago, so the library gained about 4,100 lines and seventeen files, on 35,689 commits. Lines per declaration is 5.761 over the 430,747 declarations in the table, against 5.760 on 2026-10-18 and 5.78 on 2026-10-11 - three places holding across a reading that moved, which is what that ratio is for. The composition of the week is the thing worth recording, because it is the exact inverse of the week before and both halves are now on the record. Last week definitions rose 1,484 against theorems' 827, which the previous observation read as new ground being laid rather than results being proved on ground already there. This week theorems rose 460 against definitions' 147 - a little over three theorems for every definition, where seven days ago it was not quite one. That is what building on a floor looks like once the floor is down, and it is visible here only because a frontier that stores readings rather than a current value keeps the previous shape of the same ratio. Contributors held at 772 for the fourth reading running, which is the one figure in the table that has not moved since this frontier opened.

The highest rating any chess program holds · 2026-11-02

Reading: 3,650 Elo
Held by: Triumviratus 8.0 64-bit 4CPU, set 2026-10-30
Checked: The figure did not move and the record changed hands, which is the one thing this frontier was always going to do and the one case no rule here covered. The club's list of 2026-10-30 puts Triumviratus 8.0 64-bit 4CPU first at 3,650, the same number recorded on 2026-09-25, and Stockfish 19 64-bit 4CPU - which held it then - is now 3,649, tied with Stockfish 18 and one point behind. So the number this page prints is correct and the name under it was not. A reading is written for the name alone, and `state/checks` records SAME, because the two files answer different questions: the verdict says whether the number moved and it did not, while an observation is the only place a holder is written down and the page derives the name from the newest one. Reasoning in DECISIONS.md and the general form in docs/SPEC.md §4. The read saw the whole file: all 4,783 engine rows were parsed against a header stating 4,783 programs, and the per-engine game counts sum to 4,954,202, exactly twice the 2,477,101 games the header claims, which is a second and independent check that no row was dropped. The pool grew by 26,055 games and forty-four programs since the list of 2026-09-23. Nothing is excluded today: the largest figure in the whole Elo column is also the club's first place, so the divergence of 2026-09-21 - an unranked program above the top on twelve games - has no counterpart here. What this reading cannot say is when the handover happened. The check lines of 2026-10-12, 2026-10-19 and 2026-10-24 all recorded 3,650 and none of them recorded a name, so the honest bound is that Triumviratus took the top after the list of 2026-09-23 and on or before the list of 2026-10-30, which is the arrival window applied to an attribution rather than to a figure, and `set` is the later end of it. Two things sit on the new holder. Its error bar is plus or minus 28 points against the plus or minus 12 and 16 of the two Stockfish builds below it, because it has played 214 games where they have played 1,466 and 738 - it has only just crossed the club's own two-hundred-game line, which is the threshold the 2026-09-21 reading said would be the way an outsider arrived, and this is that happening to a different program. And it is open source, marked as such in the club's own markup, so the last sentence of this frontier's explainer still holds.

Programs rebuilt without seeing the code · 2026-11-02

Reading: 78.9 per cent
Held by: Claude Opus 5.5, set 2026-09-22
Checked: The figure moved up without anybody running anything: the same row, the same model, the same run date of 2026-09-22 and the same task version 0.1.198, and the cell now reads 0.7889 where on 2026-10-02 it read 0.774 and on 2026-10-24 it was read again as unchanged. Epoch AI's files are mutable and this is the second figure revised in place that this site has caught, after #0008's training compute in October, so the numbers that cannot be recovered later are recorded here: fifteen MirrorCode rows today against nine when this frontier opened and ten on 2026-10-24, all fifteen status Success, all fifteen on the single scorer solve_at_100, all fifteen carrying the one task name, and a task-version column holding 0.1.200 on six rows, 0.1.198 on one and nothing at all on eight. The revision looks like a correction rather than a rescoring, and the harness says so. Fifteen programs in two languages attempted three times is ninety attempts, and a program that is rebuilt in one language and not the other scores a half, so the grid the scores sit on is one hundred-and-eightieth. Every one of today's fifteen cells reconciles to that grid within its own printed precision - 0.7889 is 142 of 180 to four places, 0.733 is 132, 0.467 is 84 - and the figure this reading replaces does not: 0.774 falls between 139 and 140 and is not a rounding of either, the nearest being 0.772 and 0.778. So the old cell was off the harness's grid and the new one is exactly on it. The arrival window is after 2026-10-24 and on or before today, bounded by this frontier's own previous check line and not by #0005's more recent one of 2026-10-25: #0005 reads the same file, but its fifth field is SWE-bench's newest run date and is blind to a MirrorCode cell, so the borrowed bound of 2026-10-29 does not apply - it wants a fifth field sensitive to the change, and that is the condition doing the work rather than the shared file. Two things underneath. Five rows arrived carrying run dates of 2026-10-21, which pre-date the 2026-10-24 reading that counted ten, which is the backfill signature again and again means only lag - at least three days, well inside the twelve already measured. And the six rows on 0.1.200 are a patch bump whose sample counts reproduce on the grid above, so the series is unbroken and the leader's 0.1.198 is comparable with them. The field has filled in rather than moved: fifteen scores from 4.4 to 78.9 with a median of 32.2, where nine ran from 8.9 to 77.4 with a median of 31.1.

Theorems a computer has checked · 2026-11-02

Reading: 292,326 theorems
Held by: Mathlib, the Lean 4 mathematical library, set 2026-11-02
Checked: The Theorems cell is 292,326, up 1,148 on the 291,178 read on 2026-10-24, over ten days of commits. The four structural checks are the same as the last four readings and all four held - exactly one table on the whole page, that table carries a Theorems heading, it has exactly one data row, and the row has three cells against three headings - so a drifted column or a second table would have failed rather than quietly returned a number. The cell was taken by matching the heading and never by position. The date is `report_end`, the newest commit counted, at 2026-11-02 01:38:48, and not `gen_date` at 2026-11-02 02:07:39; both fall on the same calendar day this time, which is the ordinary case and not the one that makes the distinction matter - five days ago they fell on different days and a session reading `gen_date` would have dated the reading to the day it was taken. The companion counts in `gitstats4.js` move with the table and are the magnitude check: 2,495,676 lines across 9,479 files on 35,933 commits, against 2,481,474 across 9,434 on 35,689 ten days ago, so the library gained about 14,200 lines, forty-five files and 244 commits. Lines per declaration is 5.771 over the 432,426 declarations in the table, against 5.761 on 2026-10-24 and 5.760 on 2026-10-18 - the first time in four readings that ratio has moved in its third place, by ten thousandths and upward, which says the lines arrived slightly faster than the declarations they define rather than anything about the mathematics. The composition is the thing worth recording, because this is now the third consecutive reading of the same ratio and the three of them make a shape. Theorems rose 1,148 against definitions' 531, which is 2.2 theorems for every definition; five days ago it was 3.1 and twelve days ago it was 0.56. So the week of new ground, then the week of results proved on it, and now a week in between - which is what a library being worked on looks like, and is visible here only because a frontier that stores readings rather than a current value keeps the previous shape of the same ratio. Contributors held at 772 for the fifth reading running, which is still the one figure in the table that has not moved since this frontier opened.

[ 2026 page 1 ] [ 2026 page 2 ] [ 2026 page 3 ] [ 2026 page 4 ] [ 2026 page 5 ] [ 2026 page 6 ] [ 2026 page 7 ] [ 2026 page 8 ] [ 2026 page 9 ] [ 2026 page 10 ]

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