The Barendregt-Geuvers-Klop conjecture for beta reduction: weak normalization implies strong normalization in every pure type system
A pure type system is given by a set of sorts , axioms and product rules , with full -reduction allowed everywhere, including inside type annotations. The system is weakly normalizing if every legal expression in every valid context has a -normal form, and strongly normalizing if no such expression admits an infinite -reduction sequence. Strong normalization was known to follow from weak normalization only for restricted classes (Sorensen; Barthe, Hatcliff and Sorensen for nondependent systems). Is every weakly -normalizing pure type system strongly -normalizing?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Type theory; lambda calculus; pure type systems
- Posed by
- Barendregt, Geuvers and Klop; stated by Herman Geuvers as Conjecture 8.1.2 of his thesis (Nijmegen, 1993)
- Year posed
- 1993
- Years open
- 33y
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 30 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: for every pure type system , with no functionality assumption on or , if every legal expression in every valid context is weakly -normalizing then every such expression is strongly -normalizing; reduction acts inside annotations and contexts may be open. Both properties are system-wide: the theorem does not say that an individual term with a normal form is strongly normalizing. It makes no claim about -reduction, the other half of Geuvers's formulation. The proof uses Tait-Girard style candidates indexed by sort profiles and a realization of Hurkens's paradox to exclude a graph configuration.
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with one fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region, whose write-up was human-edited). The manuscript is authored 'OpenAI' and names no human author.
Verification
No independent mathematician has checked this yet. Checked here: the abstract, introduction and Theorem 1.1 were read against Geuvers's conjecture. lean/docs/245.md points to ComparatorChallenges/TypeSystemNormalization.json (theorem OAI.PureTypeSystem.weak_implies_strong, solution module OAI.Computability.TypeSystem.Normalization); the solution file exists at the pinned commit, and the challenge is not in the formalization catalogue formalization.yaml. The statement was read here: for an arbitrary specification (any sort type, nonfunctional axiom and rule relations), with de Bruijn syntax, annotated lambda and pi, the seven PTS typing rules and full beta reduction including annotations, system-wide weak normalization of legal terms in valid contexts implies system-wide strong normalization. That is the headline claim. Not rebuilt here. The result covers beta only: the beta-eta half of Geuvers's conjecture is not addressed.