4 ms·
They're def gonna go after the Riemann hypothesis with this, hehe.
by Ericson2314 2y ago
They're def gonna go after the Riemann hypothesis with this, hehe.
- nwoli 2y agoGuessing 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.