Comment by fsniper
11 hours ago
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.
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.