Browse › Mathematical logic › 245 Weak normalization implies strong normalization in pure type systems
Weak and strong normalization in pure type systems
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that every weakly β-normalizing pure type system is strongly β-normalizing. Both properties quantify over all legal expressions in all valid contexts, and reduction acts inside type annotations. No functionality hypothesis is required. This resolves the β-Barendregt–Geuvers–Klop conjecture.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope note for family 245: Weak normalization implies strong normalization in pure type systems (lean/docs/245.md; original at openai/math commit adc7f12). The scope note says the Lean development proves the β-Barendregt–Geuvers–Klop implication with reduction inside annotations and arbitrary, possibly nonfunctional, axioms and rules, and links the comparator statement
ComparatorChallenges/TypeSystemNormalization.lean. [family-level]
Possibly relevant literature (found by the agent, not checked)
- M. H. Sørensen (submitter), TLCA List of Open Problems, Problem #9: Is every weakly normalizing PTS also strongly normalizing? (TLCA open problems list). Standard open-problem record of the conjecture addressed by Theorem 1, noting that Barthe's K-conjecture follows from it for functional PTSs (Barthe 1998); neither is cited in the paper's bibliography.
- P.-A. Melliès and B. Werner, A generic normalisation proof for pure type systems (TYPES 1996, LNCS 1512, 1998). A generic reducibility-style strong normalisation proof for arbitrary PTSs assuming suitable Λ-sets for each sort, bearing on the paper's Tait–Girard candidate construction indexed by sort profiles.
- Sebastián Urciuoli, A Machine-checked Proof of Consistency for Impredicative Pure Type Systems (arXiv:2607.20188; EPTCS 449, 2026-07-22). Its Agda formalizations of β-confluence and subject reduction for pure type systems may provide a comparison for the corresponding metatheoretic lemmas in Section 2 of the paper.
Digests and expositions
- AI Proved What?, If every program can finish, must it? (episode 245, October 2026). Provides a video and transcript explaining the system-wide hypothesis, the restriction to β-reduction, and the proposed proof through sort profiles and exclusion of a paradox-supporting configuration. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 245
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Weak-and-strong-normalization-in-pure-type-systems-September-25-2026,
author = {{OpenAI}},
title = {{Weak and strong normalization in pure type systems}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf}{OAI:Weak-and-strong-normalization-in-pure-type-systems-September-25-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/245.md. The Lean statements have not been checked by people against the paper's claims.
Family 245: Weak normalization implies strong normalization in pure type systems
Proves that weak normalization implies strong normalization for every pure type system: if every legal expression in every valid context has a β-normal form, every β-reduction sequence terminates. This resolves the β-Barendregt–Geuvers–Klop conjecture, including nonfunctional rules and open contexts.
This is the only paper in this family.