Next step after the Logic and Proofs

Stream: Lean for teaching

[Alexandre Rademaker]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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

Try using the "raw" link: https://raw.githubusercontent.com/kbuzzard/real-numbers-course/master/lean/example_sheets/sample_questions_and_solutions.lean

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

Screenshot-2019-09-21-12.38.28.png

[Kevin Buzzard]

firefox.png

[Bryan Gin-ge Chen]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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

[Patrick Massot]

and statements with useless assumptions

[Patrick Massot]

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

[Kevin Buzzard]

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

[Alexandre Rademaker]

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]

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]

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

[Alexandre Rademaker]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Why don't you want to use mathlib?

[Johan Commelin]

The fact that some things exist in core is a coincidence

[Johan Commelin]

In an alternative world, core would be infinitesimal

[Bryan Gin-ge Chen]

This works:

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Alexandre Rademaker]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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.