undefined | Better HN

0 pointsnwoli1y ago0 comments

Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that

0 comments

Smaug1231y ago

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.

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