Comment by measurablefunc
20 hours ago
People want to believe in magic so they will find excuses to do so. Computers have been proving theorems for a long time now but Isabelle/HOL didn't have the marketing budget of OpenAI so people didn't care. Now that Sam Altman is doing the marketing people all of a sudden care about proving theorems.
You are calling something “magic” that actually happened in real life.
You were misrepresenting what actually happened b/c you want to believe in magic. I'm not calling it magic, I'm saying your interpretation of events is magical b/c you don't actually understand how computers work. There is nothing magical about theorem proving, Isabelle/HOL has been doing it for decades.
Isabelle/HOL haven't been solving open problems, as far as I'm aware. They've been used for making fully-formal proofs of problems that were already considered proved to a satisfactory level by the mathematical community. I believe mathematicians generally consider proving something to the mathematical community the "hard part", while making it fully formal is just a kind of tedious bookkeeping thing.
Isabelle/HOL (a specialized software to do math proofs) doing proofs is not the analogue to LLMs (with the common accepted degeratory description: automated plagiarism machine) being capable of doing proofs. It's not the marketing, it's what the intention and the capability matrix is coming up to. I would be excited the same when Isabelle/HOL writes poetry.
[dead]