Wu's method: geometry as algebra
In 1977 the mathematician Wu Wen-Tsun of the Chinese Academy of Sciences devised a method that turns a theorem of elementary geometry into a system of polynomials and checks it algebraically. The paper on the method, received by the journal on 14 May 1977, was printed in Chinese in November 1977 and in English in Scientia Sinica for March-April 1978; it works the Simson line theorem as an example by hand.
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, Wu implemented the method in 1977 on a Great Wall 203 computer with 4K of memory and proved the Simson line theorem on it; 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. Wu himself names the Great Wall 203 twice, but with no year and no memory size. In the preface to his 1984 book he gives thanks for the chance to experiment on a desktop computer, the Great Wall 203: a few months of such experiments convinced him to buy a more modern machine. In his oral autobiography he says that at the Spring Festival of 1977 he first verified the method by hand calculation, and that on the Great Wall 203, which took only punched paper tape, he proved the Simson line theorem. The paper, received by the journal on 14 May 1977, says that programming the method on a computer "has not yet been done" and proves that theorem by hand in its Example 3; the note added in proof, dated December 1977, says nothing of a machine either. What the record does not claim: the year of the Great Wall 203 run and the 4K of memory, which only the award citation gives, while by the paper no program existed in May 1977. Wu's later texts say only that in the past years he programmed the method on small computers such as the HP9835A, and date the Pascal-conic theorem to 1980.