Hubert: Automated Formal Proof Checkers Enable Mass Crowdsourced Mathematics
Thomas Hubert · No Priors Ep. 90 | With Google's DeepMind's AlphaProof Team · Nov 14, 2024 · at 29:24
Thomas Hubert of Google DeepMind discusses how formal verification systems like Lean alter collaborative dynamics in mathematics.
0:00 / 0:27exact quote · 27.3s
▶ Watch the full episode on YouTube → 720p mp4 · rendered on demand · StarZero watermark
“But if you instead relied on a formal system to check everyone else's work, then You could do a little bit like in astronomy where you could have an amateur kind of living in the middle of maybe nowhere and you, you've never met. And then you wouldn't have to trust him. Like you could trust in some sense the machine to check the work. And if he's, the machine says it's a correct proof, then it's a correct proof. And then you can kind of start to work with many, many more people”
quote is from the automated transcript, cleaned for reading: filler sounds and stutters are removed, nothing is rephrased. names can be misheard (the analysis reads context, assessments check outside sources). how →
More from Thomas Hubert
Hubert: Formal math proofs enable self-improving reinforcement learning loops
“The advantage of that is that once kind of the proof is complete then you know, the machine would give you a signal back to say, yes, your proof is correct or not. And so we could search for kind of correct proofs. Once we find a correct proof, we can learn fr…”
Hubert: AlphaProof reached high school level but cannot rival Terence Tao
“And to be honest with you know, like kind of we, at the moment we can't rival at all with someone like Terry Tao. We, I think we demonstrated that what we've demonstrated is that we can learn general mathematics almost from scratch and arrive at kind of an imp…”
DeepMind's Hubert: Solving Harder Math Requires Introducing New Mathematical Objects
“To prove harder problems, you start to need to be able to introduce these new kind of mathematical objects to decompose the problems or problems. And we see that already happening for the IMO at a, you know, small scale.”