Chain Bounding, the Leanest Proof of Zorn's Lemma, and an Illustration of Computerized Proof Formalization. - Guillermo L. Incatasciato; Pedro Sánchez Terraf (Am. Math. Mon., 2026)