# Zulip Chat Archive

## Stream: new members

### Topic: Just finished the game, what to do next

#### Andre Popovitch (Jan 20 2022 at 19:41):

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 (Jan 20 2022 at 19:43):

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

#### Andre Popovitch (Jan 20 2022 at 19:54):

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 (Jan 20 2022 at 19:59):

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 (Jan 20 2022 at 20:00):

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

#### Patrick Massot (Jan 20 2022 at 20:00):

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

#### Yaël Dillies (Jan 20 2022 at 20:00):

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

#### Kevin Buzzard (Jan 20 2022 at 20:00):

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 (Jan 20 2022 at 20:01):

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 (Jan 20 2022 at 20:05):

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 (Jan 20 2022 at 20:08):

I would recommend trying the community tutorial then. #tutorials

#### Martin Dvořák (Jan 20 2022 at 20:34):

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 (Jan 20 2022 at 20:57):

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 (Jan 20 2022 at 21:00):

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 (Jan 20 2022 at 21:10):

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 (Jan 20 2022 at 21:13):

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 (Jan 20 2022 at 21:14):

@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 (Jan 20 2022 at 21:24):

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 (Jan 20 2022 at 21:39):

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 (Jan 20 2022 at 23:23):

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

#### Kevin Buzzard (Jan 20 2022 at 23:26):

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 (Jan 21 2022 at 00:10):

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

#### Kevin Buzzard (Jan 21 2022 at 00:18):

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 (Jan 21 2022 at 00:21):

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 (Jan 21 2022 at 00:26):

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

#### Johan Commelin (Jan 21 2022 at 00:26):

Note that all this might change in the future

#### Johan Commelin (Jan 21 2022 at 00:26):

Improved tooling could make this a great thing for education

#### Johan Commelin (Jan 21 2022 at 00:27):

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

#### Johan Commelin (Jan 21 2022 at 00:27):

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

#### Patrick Massot (Jan 21 2022 at 00:27):

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 (Jan 21 2022 at 00:30):

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 (Jan 21 2022 at 00:44):

Are you asking me or Kevin?

#### Arthur Paulino (Jan 21 2022 at 00:45):

Both actually, or anyone who might have input on this

#### Henrik Böving (Jan 21 2022 at 00:46):

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 (Jan 21 2022 at 00:52):

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 (Jan 21 2022 at 00:54):

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 (Jan 21 2022 at 00:59):

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 (Jan 21 2022 at 01:01):

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

#### Andre Popovitch (Jan 21 2022 at 06:54):

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 (Jan 21 2022 at 07:07):

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 (Jan 21 2022 at 19:21):

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

#### Patrick Massot (Jan 21 2022 at 19:26):

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 (Jan 21 2022 at 19:28):

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 (Jan 21 2022 at 19:34):

students_start_Coq_exam_scores.png

#### Martin Dvořák (Jan 21 2022 at 19:35):

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

#### Yaël Dillies (Jan 21 2022 at 19:37):

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 (Jan 21 2022 at 19:37):

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

#### Patrick Massot (Jan 21 2022 at 19:38):

I was about to point out this stream

#### Patrick Massot (Jan 21 2022 at 19:39):

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 (Jan 21 2022 at 19:40):

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

#### Kevin Buzzard (Jan 21 2022 at 20:07):

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 (Jan 21 2022 at 20:11):

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 (Jan 21 2022 at 20:18):

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 (Jan 21 2022 at 20:26):

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

Last updated: Dec 20 2023 at 11:08 UTC