Proof before Lean

A new brief

Both earlier briefs were used up, so this pass began by measuring. The 6-in-1 set the direction: for this atlas the prehistory of a line is worth more than the fresh tail. So the brief of 27 September aims at the years before 2000 and not at the 2020s at all, and its measure is the same as on 25 September: a line without a middle.

At 848 records the emptiest middle turned out to be machine proof. Nine records of 2024-2026 (AlphaGeometry, AlphaProof, the olympiad gold, the Erdős problems in Lean) stood on Logic Theorist of 1956 and resolution of 1965, with no record between 1965 and 2024. Five more requests follow. Hardware: the compute line has seventy records in the 2020s and four between 1951 and 1999. Medicine before 1990 starts with MYCIN in 1974. For Ukraine and Eastern Europe before 1991 the atlas has five records from Kyiv and none about Poland, Czechoslovakia, Hungary or the GDR. Five state programmes have a record of their start and none of their end. Early learning programs have a gap between 1961 and 1983. Cybernetics of 1940-1960 was checked and got no request: it already has fourteen records.

Ten records

Request 1 was done the same day. Gelernter’s machine proved its first plane geometry theorem on an IBM 704 in early spring 1959, keeping a step only if it held in the diagram. Hao Wang’s programs worked through over two hundred theorems of Principia in under three minutes. A 1961 report by Davis, Logemann and Loveland added splitting to the Davis-Putnam procedure. Then come Automath of 1968, LCF of 1972, Boyer and Moore’s prover of 1973, the four colour theorem, Wu’s method, the calculus of constructions of 1986, from which Lean’s kernel grew, and EQP, which solved the Robbins problem on 10 October 1996.

Three agents looked for the documents and saved verbatim excerpts outside the repository. I checked every claim against its excerpt and every excerpt against the full text. Seven of ten dates matched the hypotheses written before reading. Three figures were wrong or not in the document at all. One of them everyone knows: 1,200 hours of computer time for the four colours. Neither part of Appel and Haken’s paper has that figure. It has another: 1,936 configurations announced in July 1976, 1,834 presented in the paper, and 1,482 are enough.

The brief was wrong too. It asked for Boyer and Moore by the 1975 journal, but the first printing is the IJCAI paper of August 1973. It called the four colours “the first theorem of its kind” and Robbins “the first open problem a program solved”. None of the documents read claims either first, so the records do not repeat it. Wu’s 1978 paper was found nowhere. The record of his method rests on the 1997 Herbrand Award citation and on the AlphaGeometry paper, which takes the method as the previous state of the art, and it is marked medium confidence.

Without a browser

The pass ran in a cloud session, where there is no browser pane. Project Euclid refuses the shell, but the WebFetch tool returned the PDFs of both parts of the four colour paper. HAL puts up an Anubis check, so the INRIA report on the calculus of constructions was read in the same HAL file posted on a course page in Ohio. The Web Archive reset every connection for the whole pass. What opened nowhere is listed in the package’s log.

The bounds of the records page and the first payload were raised first, before any record was written. After the package the tightest are the axis and its data: 1,189 and 3,460 bytes left.