Aftermath bot: New pages: The Barendregt–Geuvers–Klop conjecture (openai/math 245) and The Benson–Etingof–Ostrik conjecture for finite tensor categories (208), with public follow-ups; overview regenerated; Main Page links

2026-10-19T10:46:47Z

New pages: The Barendregt–Geuvers–Klop conjecture (openai/math 245) and The Benson–Etingof–Ostrik conjecture for finite tensor categories (208), with public follow-ups; overview regenerated; Main Page links

New page

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 ([https://github.com/openai/math 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026 Weak and strong normalization in pure type systems] at commit <code>1581d4c</code>.
* '''Formalization.''' The repository's [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/245.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/TypeSystemNormalization.lean TypeSystemNormalization.lean].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 19 October 2026)
|-
| 2026-10-07 || [https://github.com/jfulfo/pts-normalization/tree/615b987a1af1fdd0832e0f661d1ffa894fe5afb5 jfulfo/pts-normalization] (GitHub, commit <code>615b987</code>) || 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 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records a sandboxed Comparator pass for the challenge <code>TypeSystemNormalization</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>TypeSystemNormalization</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-16
| J. Jardine, Lattice24, referee review [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_339.json rank_339] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 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) || [https://github.com/jiamo/lambda-computability/tree/86ee7724c50c29eec8401edb3de014bf1ea37588 jiamo/lambda-computability] (GitHub, commit <code>86ee772</code>) || 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 <code>NOTICE</code> file).
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The Barendregt–Geuvers–Klop conjecture - Revision history

Aftermath bot: New pages: The Barendregt–Geuvers–Klop conjecture (openai/math 245) and The Benson–Etingof–Ostrik conjecture for finite tensor categories (208), with public follow-ups; overview regenerated; Main Page links