education

Stream: Lean for teaching

[Daniel Ever]

Hi everyone! I'd like to apologize in advance in case I mess something up, I haven't been using Zulip before. Anyway, I'd like to know more about using Lean for educational purposes. Keep in my mind I've learnt about Lean 2 days ago and have no coding experience)

I happen to teach basic math to adults (mostly IT specialists) and they always find writing and understanding proofs the most frustrating part (as it seems for everyone with no prior math expericence). I've read some basic stuff and found the introductional tutorial, consisting of proving basic facts for inequalities, analysis etc. via different approaches.

I find all that extremely exciting and I believe it can improve any educational course in a great way. But can't find the info, are there any other intros like that, say, related to linear algebra or more advanced analysis? It seems that creating a pack of chapters that mix definitions and motivations with practical exercises (somewhat a companion to Rudin, Strang or any other undergrad textbook) would be incredibly helpful.

Can you hint where I should look for that? Thanks for your suggestions!

[Andrew Ashworth]

There's a stream on using Lean for teaching on the left. You may want to ask your question there, as the people who could help you do not necessarily read the "New members" topic

[Andrew Ashworth]

I am not sure the thing you want exists currently. My understanding is most educators write their own lecture notes. I recommend the same - using a theorem prover is fairly involved, and I'm not sure jumping directly to interactive programming exercises is worth it until you become very familiar with how mathlib works and is organized.

[Andrew Ashworth]

that said, Theorem Proving in Lean exists, as well as https://leanprover.github.io/logic_and_proof/#

[Andrew Ashworth]

Mathematics in Lean is being written, but is not currently finished

[Andrew Ashworth]

Uh, I am not sure what level you are targeting, though. I wouldn't put Rudin in front of an IT specialist learning basic math...

[Kevin Buzzard]

It would be nice if this thread were moved to #Lean for teaching . The big problem with using Lean to teach people about basic proofs is that the people who are able to take on the massive learning curve for figuring out how to use a theorem prover to e.g. prove $\sqrt{2}$ is irrational are, sadly, the people who don't really need to be taught how to do basic proofs because they figured it out already.

[Notification Bot]

This topic was moved here from #new members > education by Bryan Gin-ge Chen

[Daniel Ever]

@Kevin Buzzard indeed so. Though even with basic proofs people tend to get lost quickly, i.e., forgetting what tools they do have in their disposal. Much of the time it boils down to "keep trying one thing after another until it works", there's no goal tracking or conscious use or any tactics. In that way even reading the code in Lean is very beneficial.

Dare I say, it seems to me that combining Lean with some intuitive oriented approaches (say, 3Blue1Brown "essence" playlists) might open the new chapter of math education for non-mathematicians.

[Patrick Massot]

Daniel, did you watch https://www.youtube.com/watch?v=mTLuON5eRZI&list=PLlF-CfQhukNnO8z3TcFcoKozif9gbl7Yt&index=23 ?

[Daniel Ever]

@Patrick Massot Nope, I did not. Though I've checked some other videos, including Logic in Lean by Jeremy Avigad, which is very friendly and clears a lot of initial frustration

[Kevin Buzzard]

My impression is that if you're targetting non-mathematicians (e.g. doing outreach in a situation like a science fair or whatever) then it's extremely rare that proof is ever the focus. Instead one focusses on a more generic understanding, or calculations. I have found it very difficult to put Lean into a situation which is targetting non-mathematicians or weak mathematicians (including the weaker students on Imperial's undergraduate maths degree).

[Matthew Ballard]

In an intro to proofs course, I found the following
https://cseweb.ucsd.edu/~lerner/proof-game/
useful for sucking some of the anxiety out of the room. A good number of people are more comfortable with spatial reasoning than symbolic reasoning.

[Daniel Ever]

Perhaps I should elaborate on my situation a bit more clear. I teach random adults who for whatever reasons found out that they won't be able to futher escape the deeper understanding of math concepts for personal, career and other causes. The fact there's a huge gap between a layperson's thinking and the style of reasoning in most of the serious textbooks doesn't help either.

However, after the initial 2-3 months, when people become more confident of their abilities by practicing and exploring ideas, they feel the need to aid their intuition with some degree of rigour and that's when things usually collapse. I assume, if one actually cares to write down all the basic assumptions and schemes of reasoning, piling his desk with papers, he could avoid most of the trouble. But IRL very few people do that.

Plus IT guys have lots of experience with code, so in some way constructing blocks with calc or any other approach isn't as cryptic for them as, let's say, getting a hold of epsilon-delta notation or proving stuff about open pre-images with no solid background.

[Daniel Ever]

@Matthew Ballard thanks! that looks promising

[Matthew Ballard]

More general information on the project can be found at https://cseweb.ucsd.edu/~lerner/poly-blocks.html