Ahem. Define "Pre-AI". Automated theorem proving has been an AI task right from the very beginning with Simon and Newell's Logic Theorist, presented at the Dart

Ahem. Define "Pre-AI". Automated theorem proving has been an AI task right from the very beginning with Simon and Newell's Logic Theorist, presented at the Dartmouth workshop in 1956. Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of the Principia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead (2026-03-20: What is called here Theorem 2.85 is, in fact, numbered as 2.53 in the page 107 of the 1963 Cambridge University Press edition (https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_Mathematica_vol1.pdf https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...) and which appears, under the same 2.53 number, on page 112 of the 1910 CUP Edition, according to the digitalization on wikibooks (https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Principia_Mathematica/Part_1/Section_A#Discussion_2 https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...)). Simon was able to show the new proof to Russell himself who "responded with delight".[17] They attempted to publish the new proof in The Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.[18][17] https://en.wikipedia.org/wiki/Logic_Theorist#History https://en.wikipedia.org/wiki/Logic_Theorist#History Maybe some people only understand "AI" to mean "LLMs" but, particularly in maths, LLMs ain't going nowhere without a symbolic solver (or a human mathematician) verifying their output.