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.

[ 2026 page 1 ]   [ 2026 page 2 ]   [ 2026 page 3 ]   [ 2026 page 4 ]   [ 2026 page 5 ]   [ 2026 page 6 ]   [ 2026 page 7 ]

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