The question.
Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?
Examples.
In the current stable version of the Lean Theorem Prover, topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably not going to be too difficult, if anyone is interested in trying), but complex manifolds have not yet been done. In fact I think we are nearer to perfectoid spaces than complex manifolds — maybe because algebra is closer to the axioms than analysis. But actually we also have Lebesgue measure (it's differentiability we're not too strong at), and today we got modular forms. There is a sort of an indication of where we are.
What else should we be doing? What should we work on next?
Some background.
The Lean theorem prover is a computer program which can check mathematical proofs which are written in a sufficiently formal mathematical language. You can read my personal thoughts on why I believe this sort of thing is timely and important for the pure mathematics community. Other formal proof verification software exists (Coq, Isabelle, Mizar…). I am very ignorant when it comes to other theorem provers and feel like I would like to see a comparison of where they all are.
Over the last year I have become increasingly interested in Lean's mathematics library, because it contains a bunch of what I as a number theorist regard as "normal mathematics". No issues with constructivism, the axiom of choice, quotients by equivalence relations, the law of the excluded middle or anything. My impression that most mathematicians are not particularly knowledgeable about what can actually be done now with computer proof checkers, and perhaps many have no interest. These paragraphs are an attempt to give an update to the community.
Let's start by getting one thing straight — formalising deep mathematical proofs is extremely hard. For example, it would cost tens of millions of dollars at least, i.e. many many person-years, to formalize and maintain (a proof is a computer program, and computer programs needs maintaining!) a complete proof of Fermat's Last Theorem in a theorem prover. It would certainly be theoretically possible, but it is not currently clear to me whether any funding bodies are interested in that sort of project.
But formalising deep mathematical objects is really possible nowadays. I formalised the definition of a scheme earlier this year. But here's the funny thing. 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales' talk in Cambridge, and in particular I saw his answer to Tobias Nipkow's question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow's theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It's all open source, we are writing the new Bourbaki in our spare time and I cannot see it stopping. I know many people don't care about Bourbaki, and I know it's not a perfect analogy, but I do care about Bourbaki. I want to know which chapters should get written next, because writing them is something I find really good fun.
But why write Bourbaki in a computer language? Well whether you care or not, I think it's going to happen. Because it's there. Whether it happens in Lean or one of the other systems — time will tell. Tom Hales' formal abstracts project plans to formalise the statements of new theorems (in Lean) as they come out — look at his blog to read more about his project. But to formalise the statements of hard theorems you have to formalise the definitions first. Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn't ever realise or care that it was happening. If you're a mathematician, I challenge you to formalise your best theorem in a theorem prover and send it to Tom Hales! If you need hints about how to do that in Lean, come and ask us at the Lean Zulip chat. And if if it turns out that you can't do it because you are missing some definitions, you can put them down here as answers to this big list question.
We are a small but growing community at the Lean prover Zulip chat and I am asking for direction.
Best Answer
I would like to see that Statement of the Classification of Finite Simple Groups formalized. And then I would like to see the proof formalized. Many people use the theorem as a black box. The first generation human proof is too big for people who are not working on the second generation and third generation proofs to completely understand and it would be a huge service to the mathematical community to formalize this, as was done for the Odd Order Theorem.