[measurablefunc]

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.

[fsniper]

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.

[measurablefunc]

Like I said, you want to believe in magic & will find any excuse to do so b/c you don't really understand how computers actually work. Good luck.

[fsniper]

Chemistry is magic to uninitiated. Perhaps LLMs are to you because you are not initiated yet? I never said LLMs are AGI or will ever be AGI. I also never suggested LLMs are perfect and can prove math problems. But having incidents suggesting there are instances that does excites me. Because it was never in my expectation levels.

[johnfn]

You are calling something “magic” that actually happened in real life.

[measurablefunc]

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.

[housecarpenter]

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.