## Stream: Lean for teaching

### Topic: Next step after the Logic and Proofs

#### Alexandre Rademaker (Sep 21 2019 at 13:48):

Last semester I taught a course using the Avigad book Logic and Proofs. Now the students are asking for a course going deeper in Logics, theorem proving and Lean foundations, one possibility is to follow the Theorem Prover in Lean. Any other idea? What would be the next steps for students that are interested in dependent types and ITP?

#### Kevin Buzzard (Sep 21 2019 at 15:17):

I used Lean in some of my standard maths undergraduate introduction to proof course and it was quite chaotic. Some stuff like functions and equivalence relations go really nicely, except for when you need to explicitly invoke the axiom of choice (e.g. splitting a surjection) -- but I think we have a tactic choose for that now. But a lot of stuff using e.g. the real numbers is very hard for students, because they don't know their way around the library, and everything is hard, e.g. they want transitivity of <, they just don't know where to look. They want distributivity of multiplication over addition -- they don't know what it's called. They want to prove 2 + 2 = 4 -- again they're stuck.

Maybe it would be interesting just to develop a course here on Zulip just teaching the absolute basics of the real numbers. Explain the "mathematician's interface" to the real numbers and document it in a way mathematicians can read. If you put the documentation in a good order then this can be part of the teaching materials. Then just give lots of basic questions about the real numbers in Lean, but introducing things in an order which is natural for Lean, not the random order which is chosen in the maths books. This is always the problem I am having -- mathematicians write books and give lectures in a way which can be difficult to literally translate into Lean. But one can imagine going for a beginnings of analysis course, where all the homework is formalised but the material goes through precisely which lemmas and tactics will be useful for solving the problems. One could start off just showing them how to do basic arithmetic in Lean like a goal of $3^2+4>7$, then show them how to prove basic stuff which they know from school like (x+y)/z=x/z+y/z -- that is not going to be a triviality because z=0 must be dealt with and probably ring isn't going to do it because there's division. Once the students have learnt the basics of how to use the reals as an ordered field then they can start on doing the basic theory of sequences and series. You could target, for example, the sandwich theorem as "a main theorem of the course".

http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html

A decent 2nd year maths undergraduate at my university should be able to give you a proof of that theorem on a whiteboard. Why not teach your students to be able to give you a 21st century proof?

#### Kevin Buzzard (Sep 21 2019 at 15:24):

https://github.com/kbuzzard/real-numbers-course

#### Kevin Buzzard (Sep 21 2019 at 15:48):

It is really annoying that leanprover.github.io does not have linarith. @Mohammad Pedramfar can you make me a standard Lean 3.4.2 + current mathlib server so people can try doing the questions online without having to install Lean?

#### Kevin Buzzard (Sep 21 2019 at 16:06):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/idiomatic.20statement.20of.20sandwich.20thm

#### Kevin Buzzard (Sep 21 2019 at 16:08):

I ran an experimental version of this course last year, very informally (it was not for credit or anything), and we tried problems from their actual analysis course in Lean, and it was horrible because there were all these crappy calculations which were such a pain; without linarith (which @Rob Lewis had only just implemented a month or two before and which was an absolute lifesaver for us) we would have sunk without trace.

#### Kevin Buzzard (Sep 21 2019 at 16:10):

The thing it taught me really clearly was that a coherent real analysis course in Lean really looks nothing like a standard real analysis course taught in a maths department. The material needs to be presented in a different way.

#### Kevin Buzzard (Sep 21 2019 at 16:12):

https://github.com/kbuzzard/real-numbers-course/blob/master/lean/example_sheets/sample_questions_and_solutions.lean

#### Kevin Buzzard (Sep 21 2019 at 16:13):

I think that you can train students to solve these kinds of questions. I think it would make a really great course.

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:17):

It is really annoying that leanprover.github.io does not have linarith.

https://leanprover-community.github.io/lean-web-editor is usually up to date with a mathlib commit from within the past day or so.

#### Kevin Buzzard (Sep 21 2019 at 16:23):

Should I be able to view https://github.com/kbuzzard/real-numbers-course/blob/master/lean/example_sheets/sample_questions_and_solutions.lean on the community version?

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:28):

It works for me. There's a known issue where the Lean server won't run if you're using ublock origin though.

#### Kevin Buzzard (Sep 21 2019 at 16:28):

I ran it through the proxy and I got a bunch of xml (something to do with github presumably)

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:29):

Oh, I see, you mean if you put the URL in the form:

#### Kevin Buzzard (Sep 21 2019 at 16:32):

Oh this is great. This could be a cute little challenge for people incapable of little more than clicking.

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:34):

Yes, there's still a lot of unexplored potential for Lean on the web...

#### Kevin Buzzard (Sep 21 2019 at 16:35):

There are issues for people like me who left their glasses in the other room so just wacked the font size up 3 notches

#### Kevin Buzzard (Sep 21 2019 at 16:35):

The green lines look like they're crossing out the lemmas

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:36):

Could you share a screenshot? It looks OK to me zoomed in.

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:39):

This is what I see with my browser's zoom bumped up 3 notches:

Screenshot-2019-09-21-12.38.28.png

firefox.png

#### Bryan Gin-ge Chen (Sep 21 2019 at 16:53):

Ah, I guess you're running into this issue: https://support.mozilla.org/en-US/questions/1024343

I'm able to reproduce the overlapping if I bump up the "minimum font size" in my settings instead of using the zoom feature. I'll see if there's something I can do about this in the web editor stylesheet.

#### Kevin Buzzard (Sep 21 2019 at 16:58):

Good catch! Thanks so much for the link. tinyURL.com/real-numbers-in-lean is it OK if I bang on about that link on Twitter once we've written some basic docs?

#### Bryan Gin-ge Chen (Sep 21 2019 at 17:00):

Sure, I'll even retweet it. :grinning:

#### Bryan Gin-ge Chen (Sep 21 2019 at 17:46):

I've just deployed a new version of the web editor which has a workaround for the minimum font size issue. You'll have to refresh to get it to look right if you change the mininum font size after you've opened it, but I think that's not too much of a restriction.

#### Mario Carneiro (Sep 21 2019 at 18:45):

Regarding

Then just give lots of basic questions about the real numbers in Lean, but introducing things in an order which is natural for Lean, not the random order which is chosen in the maths books.

I think the most important thing for making things line up better with lean + mathlib is to front load the abstract algebra. STOP USING REALS. Use them as motivation, and then say that we're going to take an axiomatic approach, where we first identify the basic algebraic theorems that reals have and then show their consequences incrementally, first introducing an addition (additive groups), then a multiplication (rings, maybe semirings), then division (fields). Don't touch the actual real numbers until you are actually taking limits.

#### Patrick Massot (Sep 21 2019 at 19:20):

I don't think it's possible to seriously use mathlib for teaching. We can use mathlib tactics of course, but the mathematical library itself is developed without any pedagogical purpose. Reading mathlib in order to learn basics of real analysis will be exactly as successful as reading Bourbaki, for the same reason.

#### Patrick Massot (Sep 21 2019 at 19:22):

I still dream of writing a formalized introduction to elementary real analysis, but I think it will have to be largely independent of mathlib. When I think about this I sort of imagine writing axioms for real numbers instead of using mathlib reals. And then define limits in the elementary way, without filters, although there could be an appendix explaining that all those limits can be unified by the filter abstraction. But I'm not writing this because we have a paper to write, @Kevin Buzzard .

#### Patrick Massot (Sep 21 2019 at 19:25):

Kevin, in your example file, did you put wrong statements on purpose?

#### Patrick Massot (Sep 21 2019 at 19:31):

and statements with useless assumptions

#### Patrick Massot (Sep 21 2019 at 19:33):

Ah yes, I see question 5 is the optimal version of question 4

#### Kevin Buzzard (Sep 21 2019 at 22:43):

I didn't want to prove them -- spoilers :-)

#### Alexandre Rademaker (Sep 26 2019 at 01:48):

Hi @Kevin Buzzard thank you very much for your ideas. I am curious about how you implemented the page that shows the sandwich theorem, nice interactive document.

I was thinking also in another possible direction. Instead of use Lean to make proofs, I could discuss the foundations of Lean. There are many things I am still trying to learn in this area. For instance, what is the connection between CoC and Martin-Löf type theory? Martin-Löf type theory is also part of the https://ncatlab.org/nlab/show/pure+type+system?

In the "using Lean" line of thought, the course my have few students, not more than 5. Maybe would be nice to have a list of TODO items in the mathlib or ideas of simple libraries that could be implemented as part of a course?

#### Bryan Gin-ge Chen (Sep 26 2019 at 01:49):

I am curious about how you implemented the page that shows the sandwich theorem, nice interactive document.

I believe it uses @Patrick Massot's https://github.com/leanprover-community/format_lean

#### Kevin Buzzard (Sep 26 2019 at 06:44):

I did use Patrick's formatter yes. I don't know anything about the foundations of type theory though.

#### Alexandre Rademaker (Sep 30 2019 at 18:38):

Hi @Kevin Buzzard , in the link, there is a tactic called obvious_ineq. Where is it defined? I am trying to prove

lemma l0 : ¬ (7 < 0 + 5) := _


and I can see what you said above about how simple things can be complex.

#### Rob Lewis (Sep 30 2019 at 18:46):

I'm not sure what obvious_ineq is, but this is provable with norm_num.

#### Johan Commelin (Sep 30 2019 at 18:48):

obvious_ineq is a tactic that (I think) Patrick wrote, and it is more or less specially made for the sandwich theorem file?
Also, it has a more self-descriptive name (in this limited context, with this audience) than norm_num

#### Alexandre Rademaker (Sep 30 2019 at 18:52):

wow! norm_num is a namespace with many lemas in mathlib. So no simple solution without mathlib?!

#### Johan Commelin (Sep 30 2019 at 18:53):

Why don't you want to use mathlib?

#### Johan Commelin (Sep 30 2019 at 18:53):

The fact that some things exist in core is a coincidence

#### Johan Commelin (Sep 30 2019 at 18:53):

In an alternative world, core would be infinitesimal

#### Bryan Gin-ge Chen (Sep 30 2019 at 18:54):

This works:

lemma l0 : ¬ (7 < 0 + 5) := dec_trivial


#### Rob Lewis (Sep 30 2019 at 18:57):

norm_num is a tactic, you can ignore everything in the namespace. The other option without using mathlib is, indeed, dec_trivial. But this doesn't scale very well, and it won't work on types like the reals.

#### Johan Commelin (Sep 30 2019 at 18:57):

The reals are in mathlib... who cares (-;

#### Rob Lewis (Sep 30 2019 at 19:00):

Fine, it won't work on an arbitrary linear ordered whatever you need for numerals, which is in core :p

#### Alexandre Rademaker (Sep 30 2019 at 19:19):

Hi @Johan Commelin I am trying to use Lean in simples puzzles that ended up introducing such complications. But this is part of a course and I don't want to introduce another complication to the students. The use of mathlib requires the creation of a project for installing the library. Students are not yet comfortable with basic tools.

#### Alexandre Rademaker (Sep 30 2019 at 19:23):

Thank you @Bryan Gin-ge Chen ! Interesting to learn about dec_trivial.

#### Patrick Massot (Sep 30 2019 at 19:52):

Indeed I wrote obvious_ineq in https://github.com/ImperialCollegeLondon/M1P1-lean/blob/master/src/xenalib/M1P1.lean, and it definitely depends on mathlib.

#### Patrick Massot (Sep 30 2019 at 19:52):

Alexandre, there is very little math you can hope to do without a math library.

#### Patrick Massot (Sep 30 2019 at 19:53):

What kind of students do you have? Do they work in a computer lab you have some control on? Or do you want them to install Lean at home?

#### Patrick Massot (Sep 30 2019 at 19:55):

In the worst case scenario you can use Lean online, either using the WASM build or on CoCalc. In both case you can use a library. In the first case I would definitely recommend to use a tiny part of mathlib, unless you want your webpage to take forever to load. But the tactic part of mathlib shouldn't be too bad.

Last updated: Dec 20 2023 at 11:08 UTC