4 ms·
The lede is a bit buried: they're using Lean! This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid
by Ericson2314 2y ago
The lede is a bit buried: they're using Lean!
This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general.
Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.
- Ericson2314 2y agoThey'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.
- Smaug123 2y agoAnd while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.
- Ericson2314 2y agoHehe, well, we'll need to have a tool-assited international math Olympiad then.
- ComplexSystems 2y agoThis is the greatest idea ever. Why doesn't this exist?
- panagathon 2y agoThis does sound like a lot of fun. Since this AI only reaches silver level, presumably such a contest could be quite competitive, with it not yet being clear cut whether a human or a tool-assisted human would come out on top, for any particular problem.
- sebzim4500 2y agoIf the tools are the same as the ones AlphaProof gets (i.e. a lean compiler) then no one would use them.
- Ericson2314 2y agoWell, hopefully that changes soon :)
- Davidzheng 2y agoGood. I want my AI to use all the advantages it has to reinvent the landscape of mathematics
- YeGoblynQueenne 2y agoSure but note that's not "your AI". It's a closed-source, proprietary system by DeepMind who typically publish a result to reap the hype and then bury the system forever (see AlphaGo).
- queuebert 2y agoThat's amazing. I was just about to comment that hooking this up to Lean [1] would be killer. This must be the way forward for higher math, as proofs are getting so complicated that almost no one understands all pieces of major proofs. 1. https://lean-lang.org/ https://lean-lang.org/