Hacker News Reader

When you can formalize it in Lean or some such, why would this be? I can understand the desire to separate out other forms of research from the human corpus. But theoretical math that is decidable/provable, I’m not sure I see the risks.

View on HN

I just want to state that having "lean proofs" that build does not mean the actual real theorems we care about hold. Ultimately a human has to verify the lean encoded theorem statements that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal.

Agreed that confirming “This proposition has been faithfully translated to Lean” matters. As a side note, though, this is an area where LLMs used interactively can be helpful.

Also in the case of these recent counterexamples turning up, we have good qualitative evidence that this pathway is effective.

Reply on news.ycombinator.com