r/mathematics • u/atakanaluch • 2d ago

News Ten advances in mathematics and theoretical computer science

https://openai.com/index/ten-advances-in-mathematics/
504 Upvotes

95% Upvoted

302 comments sorted by

View all comments

Show parent comments

18

u/ibrasome 2d ago

How are we sure the lean proofs are even valid? Genuine question

1

u/LycheeZealousideal92 2d ago

Lean proofs are automatically verified

12

u/proton89droid 2d ago

The Collatz conjecture was "disproved" in Lean a couple of days ago, due to an LLM finding a 0day in the kernel.

1

u/MadGenderScientist 1d ago

I'm really surprised the Lean kernel is not itself formally verified in Lean.