The leanest proof of Zorn's Lemma

Stream: maths

[Pedro Sánchez Terraf]

My colleague G.L.Incatasciato has produced what I believe is the simplest proof of Zorn's Lemma. You can find it at the end of our expository manuscript; I hope you find it useful for your classes!

In order to make sure that we did not miss any details, we formalized it in Lean :tada: (along with the main results of the paper). The introduction to Lean is rather terse, but perhaps it works to get more people involved. Comments are welcome!

[Peter Nelson]

Nice proof! I am about to start teaching a grad topics course in formalization this week, and I’m going to include formalizing it as one of the exercises.