Zulip Chat Archive

Stream: Lean for teaching

Topic: education

Daniel Ever (Jun 04 2021 at 13:08):

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 (Jun 04 2021 at 13:33):

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 (Jun 04 2021 at 13:36):

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 (Jun 04 2021 at 13:40):

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

Andrew Ashworth (Jun 04 2021 at 13:40):

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

Andrew Ashworth (Jun 04 2021 at 13:42):

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 (Jun 04 2021 at 13:47):

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 2\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 (Jun 04 2021 at 13:51):

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

Daniel Ever (Jun 04 2021 at 14:08):

@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 (Jun 04 2021 at 14:09):

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

Daniel Ever (Jun 04 2021 at 14:13):

@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 (Jun 04 2021 at 14:26):

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 (Jun 04 2021 at 14:43):

In an intro to proofs course, I found the following
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 (Jun 04 2021 at 14:45):

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 (Jun 04 2021 at 14:46):

@Matthew Ballard thanks! that looks promising

Matthew Ballard (Jun 04 2021 at 14:47):

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

Last updated: Dec 20 2023 at 11:08 UTC