Analysis Lean Game

Stream: Lean for teaching

[Gridiron Player]

https://github.com/ImperialCollegeLondon/real-number-game

Does anybody know if there is a full or partial translation to lean4 of the game above?
Or maybe a different real number related one that I could set up with this server: https://github.com/leanprover-community/lean4game ?

Would really like to learn some analysis with lean :)

[Kevin Buzzard]

That game never really got off the ground. It was going to be a project but then COVID happened and it got very disrupted. What I could never figure out back then was how to teach Lean and analysis at the same time. With NNG you only need to learn rw and induction and rfl, and all the mathematics is very low level, so you have a recipe which works. To teach analysis you need a lot more tactics and the maths is harder. I'm not sure that learning lean and analysis at the same time is a good idea. My most recent thoughts on how to do analysis in lean are in the formalising mathematics 2024 repo which is in lean 4.

[Gridiron Player]

Kevin Buzzard said:

That game never really got off the ground. It was going to be a project but then COVID happened and it got very disrupted. What I could never figure out back then was how to teach Lean and analysis at the same time. With NNG you only need to learn rw and induction and rfl, and all the mathematics is very low level, so you have a recipe which works. To teach analysis you need a lot more tactics and the maths is harder. I'm not sure that learning lean and analysis at the same time is a good idea. My most recent thoughts on how to do analysis in lean are in the formalising mathematics 2024 repo which is in lean 4.

The man himself answered!

https://github.com/ImperialCollegeLondon/formalising-mathematics-2024/tree/main/FormalisingMathematics2024/Section02reals
Is it this that you referred to?

So what you are basically saying is that one would have to learn a substantial amount of lean4 in order to play an analysis lean4 game?
I understand that yea. Although it might be worth it, after all I am a Software Developer and used to code. But it might not be worth it for everybody.

Playing the nng4 game, it was just really cool to have a system that won't let you do anything that is mathematically wrong. It makes the process more efficient. For example, if you come up with a different proof than the math book you are studying with, you don't have to have someone "peer review" your solution or anything like that. Lean just does it for you.
Also, having the building blocks (theorems) that you need to finish the exercise neatly in a sidebar is also not too bad.

I just like it a lot more than studying with books for those reasons.

But I understand your concern as well. Most people might not be willing to learn lean4 to study analysis.

[Kevin Buzzard]

Yes you got the link, sorry I didn't post it, I was in a taxi in Portugal on mobile

[Gridiron Player]

1. Do you think it is a good idea to learn analysis the way that the natural number game is structured? Meaning go from axioms to the more complex theorems a la building blocks but not doing any application exercises?
2. Do you happen to know a book or course that teaches analysis as such?

[Jireh Loreaux]

What you're describing sounds like Bourbaki, but I wouldn't recommend that to learn from for most people (although some people do it successfully).

[Bulhwi Cha]

Perhaps we need a more beginner-friendly Bourbaki.

[Siddhartha Gadgil]

Would Terry Tao's introductory Analysis books work for this? They do start with foundations.

[James Gallicchio]

I think Heather and Patrick both have taught some amount of real analysis with Lean on the side? eg https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Real.20analysis

Not sure if that's relevant for converting to a NNG-style game.