Wu's method: geometry as algebra
In 1977 the mathematician Wu Wen-Tsun of the Chinese Academy of Sciences implemented, on a Great Wall 203 computer with 4K of memory, a method that turns a theorem of elementary geometry into a system of polynomials and checks it algebraically, and proved the Simson line theorem. The paper on the method was published in Scientia Sinica in 1978.
Why it matters
According to the Herbrand Award citation, after almost twenty years in which machine proof of geometry theorems had barely moved, it became one of the most successful areas of automated proof. Forty-six years later the AlphaGeometry paper takes Wu's method as the level to beat.
According to the 1997 Herbrand Award citation, the method rests on Ritt's principle and a zero structure theorem, and can discover theorems and find degenerate cases as well as prove; in 1979, on an HP9835A, Wu proved harder problems such as Morley's theorem, and S. C. Chou carried the method to the West at the University of Texas in the early 1980s. The AlphaGeometry paper (Nature, January 2024) ran the method on the same problems: 10 of the 30 olympiad problems of IMO-AG-30, and 75% of a wider set of 231, counting a problem as solved if it can be decided within 48 hours. What the record does not claim: anything from the 1978 paper itself, which could not be read; the record rests on the 1997 award citation and the 2024 paper.