Open Research Index

Chain Bounding

Pedro Sánchez Terraf

Palomar Registrypalomar/PALOMAR-2026-09-17-000002Sep 17, 2026math.LOscore 0

Lean 4 formalization of the core results of "Chain bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization" by Guillermo L. Incatasciato and Pedro Sánchez Terraf, published at the American Mathematical Monthly (preprint freely accessible at http://arxiv.org/abs/2404.11638). It formalizes the order-theoretic notion of _good chains_ for an "expander" of subsets of a poset: the comparability of good chains, the existence of a greatest good chain, the well-ordering of good chains for an expander of the form C ↦ C ∪ {f C}, the Chain Bounding Lemma…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-17-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-17-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-17-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'