Comment by eru 2 months ago For mathematical research, you can just run until you have a computer checkable Lean proof. 2 comments eru Reply gf000 2 months ago Given 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 2 months ago Agreed. 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.
gf000 2 months ago Given 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 2 months ago Agreed. 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.
eru 2 months ago Agreed. 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.
Given 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)
Agreed. 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.