Barendregt–Geuvers–Klop conjecture

Summary

AI-assisted claims

Claims as their sources state them. Papex has not checked them; the status stays the source’s.

All AI-assisted claims

Why it is open

A typed lambda calculus treats programs or proofs as terms that are evaluated by reduction steps; a term to which no step applies is in normal form. A term is weakly normalising if some sequence of steps reaches a normal form, and strongly normalising if every sequence of steps is finite [3, 7]. Without types the two differ: Hongwei Xi's example (λx.λy.y)Ω, where Ω = (λx.xx)(λx.xx), has the normal form λy.y but is not strongly normalising [3].

Pure type systems grew out of Henk Barendregt's lambda cube, "a canonical cube of eight type systems ordered by inclusion", whose construction Stefano Berardi and Jan Terlouw independently generalised [1]. A pure type system is fixed by a set of sorts, axioms relating sorts, and rules that say which function types may be formed [7, 8]. The conjecture, posed by Barendregt, Herman Geuvers and Jan Willem Klop, asks whether every weakly normalising pure type system is strongly normalising [5]. Geuvers stated it in his 1993 thesis, and Morten Heine Sørensen submitted it to the list of open problems of the TLCA conference (Typed Lambda Calculi and Applications) [5, 7].

The question matters because weak normalisation is often enough to prove other properties, such as consistency and the decidability of type checking in the presence of dependent types [7]. Xi argued that where the two properties coincide, "it becomes unnecessary to complicate methods for the purpose of proving strong normalisation theorems" [3].

No body sets a bar for a resolution: it would be a proof for every pure type system, or a system in which every well-typed term has a normal form but some term also has an infinite reduction. According to the 2026 manuscript discussed below, Geuvers's thesis states the conjecture both for β-reduction, the basic evaluation step, and for βη-reduction, which adds a second kind of step; the manuscript treats only the β case [8]. The Wikipedia list on which this page's status rests counts a problem as unsolved "when no solution is known or when experts in the field disagree about proposed solutions" [9].

What is known

Normalisation in the cube (1986–1991). The calculus of constructions, whose fine structure the cube describes, is strongly normalising: Thierry Coquand first proved it in 1986, and Geuvers and Mark-Jan Nederhof gave a modular proof in 1991, showing that it is equivalent to strong normalisation of the system Fω [2]. Not every pure type system normalises; Nathan Mull cites the system λU as non-normalising [7].

From weak to strong by translation (1996–2001). Xi built a translation T, based on continuations, that turns every term t into a λI-term, a term in which every abstraction λx uses its variable x [3]. By Church's conservation theorem of 1941, a λI-term is weakly normalising exactly when it is strongly normalising, so t is strongly normalising whenever T(t) has a normal form [3]. Xi applied this to prove that weak normalisation implies strong normalisation for the simply typed lambda calculus and System F, and stated that the same holds for Fω [3]. Sørensen, and then Gilles Barthe, John Hatcliff and Sørensen, confirmed the conjecture for a class of non-dependent pure type systems, defined by conditions on their sorts and rules [4, 5, 7]. Mull describes this result as the state of the art, obtained "by generalizing Xi's and Sørensen's CPS translation" [7]. The TLCA list also records that, for functional pure type systems, the conjecture implies a related "K-conjecture", a result of Barthe [5].

Structural translations (2014–2023). Cody Roux and Floris van Doorn identified ways of extending a pure type system with further sorts and rules, such as the disjoint union of two systems, that preserve normalisation [6]. Mull defined a translation that preserves typability and infinite reduction paths while removing sorts and rules that are irrelevant to normalisation [7]. Combined with the result of Barthe, Hatcliff and Sørensen, it proves the conjecture for a new class of systems with dependent rules and non-negatable sorts; Mull calls this, to his knowledge, "the first improvement in the state of the conjecture since the results of Roux and van Doorn", "albeit a somewhat modest one" [7]. He names circular rules as "one of the clear barriers": his method covers a three-tiered example system but not the same system with the added rule (s3, s3) [7]. In 2023 he described the full conjecture as "seeming quite far from being resolved" [7].

Recent claims. On 6 October 2026 OpenAI released openai/math, a repository of manuscripts "produced by an internal OpenAI model" [8]. One of them, "Weak and strong normalization in pure type systems" (dated 25 September 2026), states: "We prove that every weakly β-normalizing pure type system is strongly β-normalizing", adds "No functionality hypothesis is required", and concludes that "This resolves the β-Barendregt–Geuvers–Klop conjecture" [8]. It "makes no assertion about adding η-reduction"; its proof follows the Tait–Girard reducibility tradition and uses a relational realisation of Antonius Hurkens's well-foundedness paradox [8]. The repository says that its results are "at different stages of verification" and that "Some of the unformalized results could have issues" [8]. This manuscript links a Lean formalisation of its main theorem, the repository's formalisation catalogue (review status "unchecked") does not list it, and no revision of the manuscript had been recorded by 16 October 2026 [8]. No published assessment of the manuscript by specialists was found by that date, when the Wikipedia list still included the conjecture [9].

Main approaches

Translations into λI-terms. Map each typed term to a term whose weak normalisation forces strong normalisation of the original, using continuation-passing or related translations [3, 4]. Strongest evidence: Xi's results for the simply typed calculus and System F [3], and the non-dependent class of Barthe, Hatcliff and Sørensen [4, 7]. Main difficulty: the translation must preserve typing, so it depends on which function types the system allows [8]; the TLCA list calls translations that eliminate dependency "an obvious line of attack" and expects a simpler thunkification translation to give "only marginal improvements" [5].

Removing irrelevant structure. Reduce a system to a smaller one with the same normalisation behaviour, then apply a known result [6, 7]. Strongest evidence: Mull's extension of the proved class to some systems with dependent rules [7]. Main difficulty: circular rules, and Mull shows that dropping one of his irrelevance conditions would make the method apply to λU, which is non-normalising [7].

Simpler frameworks. Restate the conjecture for tiered pure type systems, a class of "basic, concrete" systems that Mull introduced [7]. Strongest evidence: Mull shows that a proof for all tiered systems would give the conjecture for all persistent, bounded, separable systems, a class that includes the bounded non-dependent ones [7]. Main difficulty: Mull notes that even in this setting "there are many systems to consider, some of which contain what amounts to 'junk' structure" [7].

Direct semantic proofs. Prove strong normalisation from weak normalisation for all systems at once, with reducibility candidates [8]. Strongest evidence: the 2026 manuscript, which claims the β case for every pure type system [8]. Main difficulty: Mull notes that pure type systems in general "are not always amenable to standard techniques" [7], and no published assessment of the manuscript was found by 16 October 2026 [8, 9].

Open sub-questions

1. Checking the 2026 proof. Does the argument of "Weak and strong normalization in pure type systems" hold as written, and does its Lean statement say the same as its Theorem 1, including reduction inside type annotations and open contexts [8]?
2. βη-reduction. Does weak normalisation imply strong normalisation for βη-reduction in every pure type system, the case of Geuvers's formulation that the 2026 manuscript does not address [8]?
3. Circular rules. Does the conjecture hold for Mull's three-tiered example once the circular rule (s3, s3) is added [7]?
4. Eliminating dependency. Is there a translation that removes dependent rules while preserving typability and infinite reduction paths, extending the class of Barthe, Hatcliff and Sørensen [4, 5]?
5. What blocks λU. Which property of λU makes Mull's irrelevance conditions fail, and does it single out the non-normalising tiered systems [7]?

Work on this in Papex

If you have a testable answer to one of the sub-questions above, you can draft it as a private hypothesis in Papex, or prepare the draft from Claude or ChatGPT with the Papex connector. You review the exact version, sign it and decide whether to publish it; a public record that names this problem is listed on this page. A Papex record shows who signed which version and when. It is not peer review and does not mean the hypothesis is correct.

Key references

1. Barendregt, H. (1991). Introduction to generalized type systems. Journal of Functional Programming 1(2), 125–154. 10.1017/s0956796800020025 · Checked 16 Oct 2026
2. Geuvers, H. & Nederhof, M.-J. (1991). Modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming 1(2), 155–189. 10.1017/s0956796800020037 · Checked 16 Oct 2026
3. Xi, H. (1996). On weak and strong normalisations. Research Report 96-187, Department of Mathematics, Carnegie Mellon University (February 1996); a version appeared at TLCA 1997 (LNCS 1210, 390–404, 10.1007/3-540-62688-3_48 · Checked 16 Oct 2026
4. Barthe, G., Hatcliff, J. & Sørensen, M. H. (2001). Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theoretical Computer Science 269(1–2), 317–361. 10.1016/s0304-3975(01)00012-3 · Checked 16 Oct 2026
5. TLCA List of Open Problems (updated 21 July 2014), Problem 9, submitted by Morten Heine Sørensen: "Is every weakly normalizing PTS also strongly normalizing?" Source · Checked 16 Oct 2026
6. Roux, C. & van Doorn, F. (2014). The structural theory of pure type systems. In Rewriting and Typed Lambda Calculi (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, 364–378. 10.1007/978-3-319-08918-8_25 · Checked 16 Oct 2026
7. Mull, N. (2023). An irrelevancy-eliminating translation of pure type systems. In 28th International Conference on Types for Proofs and Programs (TYPES 2022), Leibniz International Proceedings in Informatics 269, 7:1–7:21. 10.4230/LIPIcs.TYPES.2022.7 · Checked 16 Oct 2026
8. OpenAI (2026). Weak and strong normalization in pure type systems. OpenAI Math Release preprint, manuscript dated 25 September 2026, released 6 October 2026 (family 245). Source · Checked 16 Oct 2026
9. Wikipedia. List of unsolved problems in computer science (revision of 15 September 2026). Source · Checked 16 Oct 2026

Page reviewed 16 Oct 2026

Source

Open, as listed by Wikipedia · Unsolved problems in computer science. Checked 08 Oct 2026.

The status is the source’s. Papex does not decide whether a problem is solved.

Records on this problem

No public record addresses this problem yet.