hello! + how to get started on math?

Stream: new members

[Matt DeLand]

Hi!
My name is Matt! I was a student of Johan DeJong's, have left academia to work in the tech industry, but have always been interested in formalizing math! I heard about this project on Twitter and watched the seminar @Kevin Buzzard gave at Microsoft. I have been working my way through "Theorem Proving in Lean" to get familiar with the language/approach. Is there a list of topics/issues in mathlib that I could think about in order to get started contributing to the (ambitious!) project of formalizing the undergraduate/graduate curriculum? In other words - what's the best way to help with something that could possibly be useful? I could randomly pick something, but I'm wondering if there's a more impactful path.

[Bryan Gin-ge Chen]

@Kevin Buzzard shared this wish list last week. You might also browse the mathlib issues page.

[Kevin Buzzard]

We were thinking of formalising the stacks project and integrating it into the website. Seriously!

[Matt DeLand]

Interesting! Is it a reasonable way to get started (for me I mean) to start trying to write lemmas from there in Lean?

[Kevin Buzzard]

Yeah, interesting question. My personal route to the stacks project (I'm a number theory lecturer) was that first I did a bunch of questions from our first year (maths) undergrad problem sheets, and then I just started on the stacks project with the aim of defining schemes here and did about 20 tags and then realised that probably one could just do all of them, although it will take time. I've talked to Johan and also Pieter Belmans, and they are broadly positive, although neither of them knows anything about Lean. Belmans basically challenged me to do 100 tags, so I promptly added this to the gigantic pile of things I desperately want to get done in Lean.

Here are four problem sheets from the course this year: https://github.com/ImperialCollegeLondon/M40001_lean . They are not the place to start, but if you read Theorem Proving In Lean and ask questions here you should be able to do some of them. Theorem Proving In Lean is an introduction to Lean written mainly with computer scientists in mind. The natural number game was written by me and Mohammad Pedramfar (I wrote the Lean, he did the web stuff) and this is a more mathematical introduction to Lean. On the other hand you might just want to pick a tag and get going, and ask here if you get stuck.

The Lean stacks project repo needs a huge reorganisation. That code was written over 18 months ago when I knew very little about Lean, and some of the stuff in it will no doubt be appalling. It was only once I'd got up to the definition of scheme (with help from Kenny Lau and Chris Hughes, two undergrads at my university) that I realised what I should have been doing. This MSc project does schemes in a far more respectable way; no doubt you're familiar with the mathematics so it might make interesting reading. There are also the Lean maths challenges which I'm slowly adding to; currently these should be accessible to anyone who has worked through the levels of the natural number game.

[Matt DeLand]

Thanks Kevin!

I will digest some of these resources and start to learn about how more "real" math is expressed in Lean. The natural number game is how I found your project! The schemes start looks interesting - is there a reason it's not in mathlib (sorry, still learning how things are spread across these different resources). I'll be back with questions, I'm sure!

[Johan Commelin]

@Matt DeLand The biggest reason that it's not in mathlib is because it's not polished yet. Lots of rough edges, or stuff that isn't in the correct form of generality, etc... And there aren't many hands working on it.

[Kevin Buzzard]

Ramon's MSc project could probably be in mathlib in some form but Ramon is doing an MSc in Amsterdam and working part time so is busy. You could ask the same about the perfectoid project. All this stuff is just a hobby for some of us so it can be difficult to find the time to do what should be done

[Matt DeLand]

Makes sense, thanks!