3 ms·
Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that
by nwoli 2y ago
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 2y agoI 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 2y agoYeah lol i don't think either is hard to formalize in lean
- raincole 2y agoThey're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.