Post #2522106

@screwlisp@gamerplus.org You may well be right about ACL2. Off off topic, here is my small background in this subject. I followed this field a little, roughly some 15 years ago. (I went to meetings of a small community of people who were into that. I even went once to a public lecture by Voevodsky.) As one thing, I was left with the understanding that full-fledged theorem _provers_ were quite some time into the future yet. Proof _assistants_, on the other hand, were more than promising and even (seemed) "ready for prime time". However, one large piece of work to be done was obviously to represent a huge body of mathematical knowledge in the language of a given proof assistant, so it can be useful for new work. I don't know how far those efforts have reached. By the way, I came across two other promising claims at the time: One, that proofs written in those languages were _acceptably_ longer than proofs written in the traditional way. Just two or three or so times longer, not dozens of times longer (compare to _Principia Mathematica_). Two, that one of those proof assistants found a missing step in a proof Hilbert produced when he formalized elementary classical geometry. The significance of this is that Hilbert had gone to great trouble to make those proofs _full_. His proof was quite correct: it was merely that even he, working with that goal in mind, had inadvertently considered something "too obvious". @kentpitman@climatejustice.social @bagder@mastodon.social