Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I don't think Lean is as rigorous as you implied here.

https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o...

> In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.



Consider applying for YC's Winter 2027 batch! Applications are open till November 2.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: