3 ms·
For mathematical research, you can just run until you have a computer checkable Lean proof.
by eru 3mo ago
For mathematical research, you can just run until you have a computer checkable Lean proof.
- gf000 3mo agoGiven that it was formalized correctly, which is far from trivial in many cases (Of course LLMs can help there, get it right etc, just a caveat that people have to keep in mind)
- eru 3mo agoAgreed. But also formalising the statement of a theorem, or rather understanding the formalisation that the LLM suggested to you, is often a lot easier than understand the whole proof, especially if it's a formal proof.