Just finished the game, what to do next

Stream: new members

[Andre Popovitch]

Sorry, I'm going to make a bunch of threads because I have some questions haha
I'm thinking of working through this text in lean https://smile.amazon.com/Real-Analysis-Constructive-Mark-Bridger/dp/0471792306 , would that be a good choice?

[Patrick Massot]

You can use Lean for this, but using mathlib would be very painful and frustrating because that library is not constructive.

[Andre Popovitch]

I see, do you have any advice for learning real analysis in a way that wouldn't be painful in lean? Or can I follow that book and just not use mathlib?

[Kevin Buzzard]

When you say "real analysis" do you mean "real analysis as taught in maths departments" or "constructive real analysis"? These are very different things

[Kevin Buzzard]

I personally would say that lean is not a good tool for learning any kinds of mathematics at all

[Patrick Massot]

I'm specifically commenting the word "constructive" in the book title

[Yaël Dillies]

Kevin, I learned order theory, convex analysis and additive combinatorics using Lean!

[Kevin Buzzard]

I would say that it's better to learn the mathematics in the traditional way and then engage with it in lean once you understand it

[Kevin Buzzard]

Yael, you also went to the international mathematics Olympiad so what works for you might not be a good measure of what works for others

[Andre Popovitch]

When you say "real analysis" do you mean "real analysis as taught in maths departments" or "constructive real analysis"?

Doesn't really matter to me, I'm just trying to learn more math

I personally would say that lean is not a good tool for learning any kinds of mathematics at all

:( that's too bad, I really enjoyed the natural number game for learning about the naturals, and I wanted to do the same thing for reals

[Kevin Buzzard]

I would recommend trying the community tutorial then. #tutorials

[Martin Dvořák]

Kevin Buzzard said:

I personally would say that lean is not a good tool for learning any kinds of mathematics at all

Didn't you say in your popular talk that Lean is great for teaching freshmen about what a mathematical proof is?

[Stuart Presnell]

This probably isn't the best book to use if your main interest is in learning how real analysis is conventionally done, just because the approach taken in this book isn't what's normally taught. But after skimming through the preview that's available on Google Books I think you could learn a lot by formalising this in Lean. In Chapter 1 the author goes very slowly step by step through the process of defining "intervals of rational numbers", proving properties of them, and picking out special families of these intervals that will play the role of real numbers. The fact that he's working constructively might actually be helpful to you, since it may be easier for you to imitate the same constructions and definitions in your formalisation.

[Stuart Presnell]

If you do decide to follow this path I'd suggest you start by working through the definitions and exercises in Chapter 0 (some of which will be repeating things you've already done in the game).

[Stuart Presnell]

Then when you come to formalise Chapter 1 you'll learn lots about how to define structures in Lean, how to define operations that take these objects as inputs and outputs (for example, the addition function on rational intervals in Definition 1.1.8), and how to use typeclasses to talk about properties of your structures (for example, to assert that there's an interval that plays the role of "zero").

[Stuart Presnell]

And of course if it does turn out to be horribly frustrating as others have warned then you can always give it up and turn to another book instead, or just study real analysis in a more conventional way. But I think it's worth the experiment.

[Martin Dvořák]

@Kevin Buzzard IIRC, your main thesis was "Lean is the right way to do math." ; not "Lean is the right thing to do in addition to doing math / after having learnt math." . Maybe I am pulling out a strawman, I don't know.

[Alex J. Best]

There's no such thing as "the right way" to do mathematics, of course. And there is a big difference between learning about the concept of proof, and what constitutes one (a necessary first step in advanced mathematics), and learning specific proofs and proof techniques.

[Arthur Paulino]

My experience has been that the more fluent I become in Lean, the easier it gets to learn mathematics with it. Understanding mathematical concepts while type-checking terms in my head "at the same time" often becomes a mental mess :smiley:

[Andre Popovitch]

@Stuart Presnell thank you for the advice, I'll give in a try and report back :p

[Kevin Buzzard]

Martin Dvořák said:

Kevin Buzzard said:

I personally would say that lean is not a good tool for learning any kinds of mathematics at all

Didn't you say in your popular talk that Lean is great for teaching freshmen about what a mathematical proof is?

I might have had different opinions in 2019 before I spent a year studying these ideas with a qualified math education specialist.

[Martin Dvořák]

Is Lean no longer used in the introductory mathematical-proving class for freshmen at Imperial? Do you still teach the class?

[Kevin Buzzard]

I use it in different ways now. I teach the maths first in a regular way and then show people how to do it in Lean afterwards

[Kevin Buzzard]

The problem with "here is the definition of an equivalence relation, let me show you right now what it looks like in Lean, let's do some simple examples all in Lean, isn't this cool" is that the students who would usually struggle with the concepts when taught in the usual way are likely to be struggling even more when presented with the added obfuscation of a theorem prover. This was one of the things we learnt after experimenting. Better to teach it in a regular way and then give an optional class where you do it in lean afterwards.

[Martin Dvořák]

I don't understand the emotions I am experiencing right now.

[Johan Commelin]

Note that all this might change in the future

[Johan Commelin]

Improved tooling could make this a great thing for education

[Johan Commelin]

People are actively working on making it a tool for high school teaching.

[Johan Commelin]

Kevin is observing that right now, using it in a 1st year course is not working.

[Patrick Massot]

And it's already a great tool when you first teach stuff in the usual way and then have students redo it in Lean. This is what I've been doing for four years.

[Arthur Paulino]

Do you think it's plausible to think about a test/control experiment with some students being asked to do it in Lean and some informally with pen and paper?

[Patrick Massot]

Are you asking me or Kevin?

[Arthur Paulino]

Both actually, or anyone who might have input on this

[Henrik Böving]

Just as a little remark: I think I have written more proofs in Lean and Isabelle than informally by hand so far, mostly because in my math courses we rather rarely get to see a proof or even develop one ourselves, and while I feel like being exposed to theorem provers rather early on (I first did a little bit of stuff with Isabelle close to the end of my 1st semester) did definitely give me a better understanding of the logic and reasoning part I don't at all feel competent enough to write proofs about the things we do in our math courses in Lean vs doing them informally on paper. Although that might also be because as mentioned above my math courses don't tend to stick to the entire proof stuff as much after all.

Just my 5 cents on the usefulness of ITPs in teaching^^

[Arthur Paulino]

After only 3 months of exposure to formal proofs (I had absolutely no experience with this subject previously), I can observe a huge impact on my way of thinking about mathematics. I am now more aware of things that I unconsciously took for granted while writing informal proofs

[Henrik Böving]

Hm well maybe I never felt that change because I didnt develop much intution for informal proofs before doing ITP stuff :sweat_smile: I certainly do observe that lots of other students in my classes struggle with writing a proof whenever it comes up while I don't

[Patrick Massot]

I would love to education science people doing some rigorous assessment of the impact of my course, but so far I haven't found interested people who have time to do it.

[Arthur Paulino]

Might be just a matter of time (I hope not too much)

[Andre Popovitch]

I teach the maths first in a regular way and then show people how to do it in Lean afterwards

I see. I remember you talking about a tool that allowed you to turn a lean source file into a nicely-formatted website, does that still exist?

[Stuart Presnell]

Note that what Kevin’s experience suggests is that you shouldn’t try to teach a whole class via Lean because the struggling students will struggle more. It doesn’t tell us that you as an individual student shouldn’t use Lean as part of your studying. You may well find, as others in this thread have reported, that the extra rigour of using Lean improves your understanding — for example, by preventing you from skimming over things you only half understand and then getting stuck later.

[Martin Dvořák]

In contrast with Kevin's (new) opinion, I found a thesis that suggests that students should learn formal proving in Coq first, and only then proceed to usual mathematical proofs. It is intended as plan for CS students, but nevertheless, it could be interesting to compare with opinions of various people here.

https://publishup.uni-potsdam.de/opus4-ubp/frontdoor/deliver/index/docId/42379/file/boehne_diss.pdf

students_start_Coq.png

[Patrick Massot]

Martin, maybe we should clarify that Kevin and I are very much aware that all this is very much an open research question (in education science). And we certainly hope that more research will be conducted, and more tools will be developed to lower the entry price into formal proofs.

[Martin Dvořák]

I should have mentioned; it is in Chapter 7. Alternatively, you can read similar thing here: https://arxiv.org/pdf/1803.01466v1.pdf

[Martin Dvořák]

students_start_Coq_exam_scores.png

[Martin Dvořák]

Is anybody interested in continuing the conversation about the educational stuff? If so, I'd fork this conversation.

[Yaël Dillies]

I love to compare those figures to those achieved by AI, like GPT-f, because the latter always are a bit underwhelming, but put into context they become pretty good!

[Kyle Miller]

@Martin Dvořák You could share this research on the #Lean for teaching stream

[Patrick Massot]

I was about to point out this stream

[Patrick Massot]

I should also say that I saw infinitely many more papers about using proof assistants to teach computer science than math, and the comments made there always seemed very hard to transpose to pure maths. That table clearly is about CS and programming.

[Patrick Massot]

All those words: first order logic, propositional logic, data type, inductive data types...

[Kevin Buzzard]

Theorem provers are used in many computer science departments. The problem we're trying to solve is getting them used more commonly in mathematics departments, where the curriculum is very different so the problems faced also seem to be different.

[Martin Dvořák]

Kevin Buzzard said:

Theorem provers are used in many computer science departments. The problem we're trying to solve is getting them used more commonly in mathematics departments, where the curriculum is very different so the problems faced also seem to be different.

They might be used on many CS department, but they are usually not used for the first contact between undergrads and mathematical proofs.

[Martin Dvořák]

In this aspect, I found your teaching methods (as you described them in https://www.youtube.com/watch?v=Dp-mQ3HxgDE in 2019) really revolutionary. Not because it was taught to Math students (as opposed to CS students) but because it was taught at the very beginning of their studies.

[Arthur Paulino]

Maybe this thread can be split and moved to #Lean for teaching (and probably merged into Martin's thread?)