The Barendregt–Geuvers–Klop conjecture
From OpenAI Aftermath
The Barendregt–Geuvers–Klop conjecture asserts that in a pure type system, weak normalization implies strong normalization: if every legal expression has some terminating reduction sequence, then every reduction sequence terminates. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September 2026, claims a proof for β-reduction in every pure type system, and the collection includes a Lean formalization of the statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Geuvers formulated the system-wide conjecture, for β- and βη-reduction, in his 1993 thesis (Conjecture 8.1.2).
- Earlier work reduced strong normalization to weak normalization of translated terms: Sørensen's continuation-passing construction for generalized nondependent, clean, negatable systems; the uniform nondependent result of Barthe, Hatcliff and Sørensen; and Mull's thesis, which weakens these restrictions in the nondependent tiered setting. Roux and van Doorn proved weak-normalization preservation for some structural extensions, Mull showed that the implication transfers from the irrelevance reduction of a tiered system, and Roux has proposed an internal proof translation.
- Barthe and Coquand exhibited nonnormalizing pure type systems in which erasing domain annotations identifies terms that are not β-convertible, which constrains comparisons between systems.
The original result
- Claim. Theorem 1 of Weak and strong normalization in pure type systems states that for every pure type system, with no functionality assumption on its axioms or product rules, if every legal expression in every valid context is weakly β-normalizing, then every such expression is strongly β-normalizing. Reduction is allowed inside type annotations. The manuscript states that the result concerns β-reduction only and makes no assertion about η-reduction.
- Method, as described: after reducing to finite sort and rule sets, the proof records the "sort profile" of each normal type and runs a Tait–Girard reducibility argument with candidates processed along the strongly connected components of a finite signed graph of profiles. One remaining graph configuration would block the construction; weak normalization rules it out through a second, typed argument that realizes Hurkens's paradox relationally.
- Source. The manuscript Weak and strong normalization in pure type systems at commit
1581d4c. - Formalization. The repository's scope note states that the formalization proves the β-version of the conjecture for pure type systems with arbitrary sorts and nonfunctional axioms or rules, with reduction inside type annotations. Its Comparator statement is TypeSystemNormalization.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 19 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | jfulfo/pts-normalization (GitHub, commit 615b987) |
Verification (two kernels) | A fork of the collection containing only this result's Lean proof, with the Comparator challenge run with the nanoda kernel enabled. Its published run log records that both nanoda and Lean's default kernel accept the solution. | GitHub repository. |
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records a sandboxed Comparator pass for the challenge TypeSystemNormalization. |
The review states that it does not say the mathematics is correct beyond what Lean checked; it describes itself as a model-assisted reading without a referee yet. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list TypeSystemNormalization, so the challenge was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_339 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer states that it read the main sections closely and only spot-checked the long relational encoding of Hurkens's paradox. Its one minor note concerns a three-sort specification without a (*, *) rule that the manuscript's exclusion proposition implies is not weakly normalizing; the reviewer suggests that the paper state or illustrate such nonstandard consequences, and states that it does not regard the example as a counterexample. | The reviews are published under CC BY 4.0. |
| 2026-10-19 (latest commit) | jiamo/lambda-computability (GitHub, commit 86ee772) |
Use (Lean port) | A Lean library on lambda calculus and computability that adapts the collection's formalization of this result (with several others) to its own Lean and Mathlib versions, stating that "the mathematics and the proofs are upstream's". Its own addition here is λΠ presented as a pure type system, whose strong normalization it derives independently of the adapted theorem. | GitHub repository (created before the release; the adaptation is listed in its NOTICE file).
|
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
