# Weak normalization implies strong normalization in pure type systems

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

- [Weak and strong normalization in pure type systems](../../preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf)

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

| Result | Comparator statement |
| --- | --- |
| Weak normalization implies strong normalization in every pure type system | [TypeSystemNormalization.lean](../ComparatorChallenges/TypeSystemNormalization.lean) |