[nwoli]

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

[Smaug123]

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.

[Davidzheng]

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

[raincole]

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