This is a talk by Prof Kevin Buzzard given at Microsoft Research recently. In it, he proposes a program for formalizing the undergraduate mathematics curriculum in Lean. I personally found it fascinating, partly because this goal resonates strongly with me, but also because of the cultural and sociological observations. The overlap between “real mathematicians” and the the theorem proving space is incredibly tiny, so Prof Buzzard has been able to make a significant impact, working with undergraduates, largely because very few other people are doing that kind of work.
This was great. It has a bit of the excitement associated with Hilbert’s program, but the application is not proving/solving all of math (which had didn’t turn out the way Hilbert wanted), but rather shoring up the foundational knowledge that is used in modern math.
Great talk, thanks for sharing.
I like his pragmatic approach, i.e. having clear goal of doing modern math, rather than playing with fancy type theories.
Also interesting bit where he mentions that for math students, often one of the main barriers of entry into proof assistants is installing and running in the first place (they are often using Windows laptops). E.g. ‘what the fuck is git clone’, or even ‘command line? eh?’
Wonder if it’s something worth solving on a larger scale: e.g. something cloud based. Once students find it useful, there would be at least motivation to overcome the technical difficulties and install locally.
Prof Buzzard is also running a cool blog, Xena.
Wait… ‘a significant impact’ on who, exactly?
(I’m not going to watch the video, because I don’t have patience for videos. I’d read a transcript, though.)
They’re the first ones out of the gate to formalize a bit of mathematics of actual interest to working mathematicians today. Almost all of the existing formalization efforts (he picked on the odd-order theorem) cover old and stale areas.
Here’s the PDF of the presentation, but IMHO you’d be missing out on a lot of the good stuff, including the Q&A.
Right, he was able to pick up some of the current buzz around perfectoid spaces by formalizing some of the relevant definitions in Lean. But in the slides he sort of admits it’s just a PR gimmick – no new results were obtained thereby. Now, if some working research mathematicians picked up that formalization and did something of mathematical interest with it, that would be news. Maybe some of his current crop of undergrads will grow into that?
Doing new “real mathematics” in a formal system is an incredibly high bar; I don’t think anyone is plausibly suggesting they can do that any time soon. It seems to me Prof Buzzard is proposing a “walk before you can run” approach where the goal is indeed about formalizing definitions and statements of results. This alone can give significant benefit, including making this space searchable.
I think “just a PR gimmick” is disrespectful. Prof Buzzard is embracing the importance of doing good marketing, which is something people (especially academics who might feel they’re above it) ignore at their peril.
No disrespect intended. I’m using his own words: see Slide 13: “Serious piece of research, or elaborate PR stunt? Maybe both.”
The four-color map theorem proof was “real mathematics”, and that was decades ago. I don’t think the bar is that high, I just think that the community of mathematicians haven’t found these tools to be useful in their work. The slides talk a lot about why, but he doesn’t even refer to Lakatos’ Proofs and Refutations, or any other serious investigation, he just rolls it all up into “belief systems”. I would hope he’s at least aware of the history!
But my question was about the “impact” you had claimed. As far as I can tell, there has been no significant adoption of Lean by working mathematicians. Maybe you meant it’s having an impact on undergraduate mathematics education? Is there anywhere besides Imperial that has adopted this curriculum?
Maybe “impact” wasn’t the right word, I meant in terms of doing interesting things that move understanding in the world forward, not in terms of how it’s measured in academic circles. The discrepancy between the two is interesting from a sociology perspective :)
There shouldn’t be significant adoption of lean by working mathematicians, by their documentation it isn’t ready for prime time yet.
“If you are looking for stability, it may not be the system for you”. Mathematicians probably should not use this for their day job.
That’s a software concern. Compatibility of the artifacts generated by use of today’s version of Lean in tomorrow’s versions is another familiar concern to us software folks. That’s important, but there’s a much deeper issue here. Working mathematicians generally don’t use any proof assistant or automated theorem prover technologies at their day jobs, despite these being a long-standing topic in computer science, and quite useful in some specialized sub-fields thereof. It’s not (just) because they are cumbersome and finicky to work with; LaTeX has some pretty awful UX but is ubiquitous among working mathematicians, it’s basically a job requirement, and nobody complains much. The real issue (I think) is that “machine understanding” of a proof is generally a very poor substitute for human understanding. Still, I can see the value in a machine-assisted undergrad course. Sounds like a good idea, just shouldn’t be oversold.
You’ll hear mathematicians talk about how they should be using a proof assistant like how I talk about how I should be exercising. I suspect the hurdles are similar.
Part of the scientific process is replication and peer review. So, it might be worthwhile to analyze old mathematics if trying to catch flaws in it now or in new work later on that builds on it.