Prove a theorem. Write a function.

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…

Advertisement