easy to read proofs on mathlib4

Stream: Lean for teaching

[Apurva Nakade]

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]

Maybe IMO 2001 q6?

[Heather Macbeth]

Also IMO 2005 q3 and IMO 1964 q1

[Heather Macbeth]

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

[Apurva Nakade]

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

[Apurva Nakade]

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]

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]

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]

A few harder ones:

• exercise 1 in section 5.2
• exercise 1 in section 6.4
• exercise 4 in section 8.4