∑math20

Mathematical logic · Result 245

Weak normalization implies strong normalization in pure type systems

1 paperLean

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.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of Weak and strong normalization in pure type systems

Weak and strong normalization in pure type systems

OpenAI · September 25, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves the \(\beta\)-Barendregt–Geuvers–Klop conjecture for pure type systems: if every legal expression in every valid context has some terminating \(\beta\)-reduction sequence, then every \(\beta\)-reduction sequence from every such expression terminates. Reduction is allowed inside type annotations, and the specification may have arbitrary sorts and nonfunctional axioms or rules.

Comparator links

ResultComparator statement
Weak normalization implies strong normalization in every pure type systemTypeSystemNormalization.lean

Scope note on GitHub →