Chain Bounding and the leanest proof of Zorn's lemma

We present an exposition of the *Chain Bounding Lemma*, which is a common generalization of both Zorn's Lemma and the Bourbaki-Witt fixed point theorem. The proofs of these results through the use of Chain Bounding are amongst the simplest ones that we are aware of. As a by-product, we show that for every poset P and a function f from the powerset of P into P, there exists a maximal well-ordered chain whose family of initial segments is appropriately closed under f. We also provide a "computer formalization" of our main results using the Lean proof assistant.