undefined | Better HN

0 pointsSmaug1231y ago0 comments

I think you might be thinking of the recent project to start Fermat's Last Theorem? The Riemann hypothesis has been easy to state (given what's in Mathlib) for years.

0 comments

Davidzheng1y ago

Yeah lol i don't think either is hard to formalize in lean

raincole1y ago

They're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.

j / k navigate · click thread line to collapse

0 comments

Davidzheng1y ago

Yeah lol i don't think either is hard to formalize in lean

raincole1y ago

They're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.

j / k navigate · click thread line to collapse