New maths PhD students Lambert A’Campo and Ashvni Narayanan have proved that a normed real vector space with compact unit ball is finite-dimensional in Lean! [update added a few days later: ROFL Sébastien Gouëzel on the Lean chat complained that they had proved the “wrong” theorem and now I see that they have observed that exactly the same proof works for vector spaces over an arbitrary complete non-discrete normed field 🙂 ]
For me this is a milestone, because Lambert and Ashvni heard about Lean through me, Ashvni has chatted to me about Lean in person, and Lambert both in person and online, but they don’t really come to the Xena project. Lambert just asked me if this theorem was provable in Lean, I said “sure”, and he’s just gone away and worked on it with Ashvni and they’ve figured out how to prove it in Lean.
Here’s s brief history of how they got there. Lambert talked to me on the Lean chat. He played the natural number game. He installed Lean, created a new Lean project on his computer called compact_unit_ball, and just got going. He pushed it onto github so Ashvni could access it too. When they got stuck, Lambert asked questions in the #new members stream in the Lean chat, and experts helped him out. We understand mathematicians in that chat, as long as they are speaking rigorously. At the end of the day, these new PhD students have written a computer program containing the definition of a function which, when run, spits out a term of a type. A mathematician would call the type “the statement of the compact unit ball theorem”, and they would call the term “the proof of the compact unit ball theorem”.
Lambert and Ashvni are on my CDT, the London School of Geometry and Number Theory (applications for 2020 open now and close Dec 31st 2019!) I honestly think that teaching young mathematicians how to prove theorems in Lean is every bit as important as teaching them how to write computer programs in Python. Doing maths this way is making sure that you don’t make any mistakes along the way. Lambert and Ashvni proved a theorem by writing a function and I am proud that our CDT (Centre for Doctoral Training, a maths PhD student program) will accept such work as a submission for a computer project.
Lambert and me have been talking about etale cohomology. It’s going to be a tall order. A second year undergraduate at Imperial College, Calle Sönne, is working on sites and sheaves. We have found some of the literature a bit imprecise. What is a Grothendieck topology? Look at the definition on Wikipedia! It says that a Grothendieck topology is a “collection” of distinguished sieves blah blah blah. What is a collection? Can some mathematician tell us a more precise reference which deals with these issues properly? Is it a set or a class? Or is there more than one definition here?
Lambert did come to Xena last Thursday, and Johannes Girsch was also there (he’s another PhD student on the CDT). Calle was there too. We’ve been reading about condensed mathematics. That’s Clausen and Scholze’s new theory. Scholze talks about sites and Grothendieck topologies in there, and on the first page of chapter 11 he says the word “canonical” four times. If there are any other mathematicians in London interested in trying to figure out etale cohomology or condensed mathematics within the context of the Lean theorem prover (or even not within that context), any mathematician who thinks they know a definition of canonical, or any mathematician interested in learning about how to prove a theorem by writing a function, they can always find me in the computer room in Imperial’s maths department on Thursday evenings during Imperial’s term time. If London is not convenient, I’m often available on the Lean chat.
PS There are lots of <= worlds in the natural number game now, but hardly any < worlds beyond the definition. If people want to help out, feel free! There’s also the fledgeling real number game…
I’ll change it. Scholze is giving the course but the theory is joint with Clausen.
LikeLiked by 1 person
Pingback: [computer-assisted proof] PhD students have used Lean to prove that a normed real vector space with compact unit ball is finite-dimensional - Nevin Manimala's Blog
could you blog on the economic aspects of these Lean activities? For example, these graduate students (congratulations to them!) seem to be graduate students in a professional pure math grad school. I think NSF and whatever funding bodies they have in EU and UK do not believe that Lean formalization is pure math (but correct me if I am wrong). There do not seem to be any tenured positions for Lean formalizers. So the only way a pure math grad student could work full time on these things is if they intend to go to hedge funds or industry. Could you explain to me if my understanding is correct? Do you intend to do anything about it (so that in future a pure math graduate student could have at least a distant hope of finding a tenured position in academia if they go full formal)?
I am applying for money for post-docs. I totally agree that it’s a risky route for graduate students. That’s why I’m spending a lot of time working with undergraduates, who will be able to write on their CV’s that they have been doing extra-curricular stuff.
Once I worked in number theory. There is too much number theory. What is the point of having an average student who proves a fairly standard theorem, never publishes it, and then goes off to work in industry? Now I work in formal proof verification, and in my mind any student who formalises some stuff, gets it working, and then just leaves it to bitrot has taught us something about Lean and added to the general collection of Lean code which mathematicians might be able to look at and learn from. So even lousy formalisations are really helpful to me — and to society — right now.
ROFL Sébastien Gouëzel on the Lean chat complained that they had proved the “wrong” theorem and now I see that they have observed that exactly the same proof works for vector spaces over an arbitrary complete non-discrete normed field
Just curious, why was it a “wrong” theorem? Was it not general enough?
Yes, the proof was fine, but the same proof generalised to give a more powerful result.