3 ms·

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 ma

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.

johnfn 5mo ago
You are calling something “magic” that actually happened in real life.
- measurablefunc 5mo ago
  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 5mo ago
    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.
fsniper 5mo 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.
- measurablefunc 5mo ago
  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 5mo ago
    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.
redsocksfan45 5mo ago
[dead]

johnfn 5mo ago

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

measurablefunc 5mo ago
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 5mo ago
  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.

fsniper 5mo 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.

measurablefunc 5mo ago
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 5mo ago
  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.

redsocksfan45 5mo ago

[dead]