# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: easy to read proofs on mathlib4

#### Apurva Nakade (Jul 14 2023 at 14:43):

Hi, I'm giving a talk in a couple of days about Mathlib. What are some easy to read proofs on Mathlib4 (at undergraduate math level) that are somewhat close to their natural language versions?

I usually just default to the "infinity of primes" proof. I'd like to mix things up a bit and also am myself curious about this.

When I skimmed through the library, proofs of many results that I thought were basic used a hierarchy of instances and we're very far from a natural language proof. I haven't yet looked at the IMO problems but I am hopeful of finding some good examples there.

#### Heather Macbeth (Jul 14 2023 at 14:45):

Maybe IMO 2001 q6?

#### Heather Macbeth (Jul 14 2023 at 14:46):

Also IMO 2005 q3 and IMO 1964 q1

#### Heather Macbeth (Jul 14 2023 at 14:48):

IMO problems are not really mathlib, though. The talk is really on mathlib and not just on Lean?

#### Apurva Nakade (Jul 14 2023 at 14:48):

Just doing math in Lean (I tend to conflate the two :P in my head)

#### Apurva Nakade (Jul 14 2023 at 14:50):

I'm giving a talk at a summer camp. The kids are the kind who love solving IMO problems, they would love these proofs in Lean haha

Thank you so much for your suggestions!

#### Heather Macbeth (Jul 14 2023 at 14:52):

If it doesn't need to be mathlib, you might like my lecture notes, for that audience. There are tons of problems with a tiny kick, and most of them are "standalone" tactic-only proofs (no lemmas).

#### Apurva Nakade (Jul 14 2023 at 14:56):

Thank you! This is great. Do you have any favorites? (I know we're not supposed to say that :P)

I'll also direct them to your book for "further reading".

#### Heather Macbeth (Jul 14 2023 at 15:01):

A few harder ones:

Last updated: Dec 20 2023 at 11:08 UTC