Hacker News new | ask | show | jobs
by fsniper 53 days 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.
1 comments

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.
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.