History of ITPs and ATP?

Stream: general

[Luigi Massacci]

Are there any community recommended books about the history of proof assistants? Or indeed, any books at all.
I have vague notions of things like the Logic Theorist and Automath, the controversies surrounding the Four Color Theorem and Hale's work on Euler's Conjecture, but never really read something more comprehensive, so I'm looking for book /article recommendations!

[Alex Nelson]

This is a great question.

There's a wonderful book, "Handbook of Practical Logic and Automated Reasoning", by John Harrison. It's a "literate program", in some sense, of the various algorithms useful for proof assistants based on first-order logic, but generalizes to higher-order logic in the obvious ways. Each chapter ends with a review of the literature, for you to look further in whatever topics interest you.

As far as a more direct history of proof assistants, there are a couple of good papers. Hermann Geuvers' "Proof assistants: History, ideas and future" (https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025) is a good read.

The only other paper which discusses the history of interactive theorem proving is John Harrison, Josef Urban and Freek Wiedijk's "History of interactive theorem proving" (https://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf)

[Luigi Massacci]

The Handbook was thrown at me (not literally fortunately) by one of the logic professors in our CS department, but that is really a reference textbook, I was looking for something like the other two papers, thank you!

[Tyler Josephson ⚛️]

For a short read, Formal Proof by Thomas Hales is nice: https://cmartinez.web.wesleyan.edu/documents/FP.pdf