If every program can finish, must it?

0:00The question

In the lambda calculus, a program runs by rewriting: wherever a function meets its argument, substitute. A term may offer several places to rewrite. Take the function that ignores its argument, applied to Omega, a term that rewrites to itself forever. Rewrite the outside first and you finish at once; keep rewriting inside Omega and you never finish. So the term is weakly normalizing, some route ends, but not strongly normalizing, where every route ends. Type systems are meant to rule out terms like Omega. Pure type systems, introduced by Berardi and Terlouw, generalize Barendregt’s lambda cube, whose eight corners include the simply typed lambda calculus, System F and the calculus of constructions. Even a tiny typed program has many routes: our count for 3 applied to 2, as Church numerals in System F, is about 493 billion reduction orders, from 12 to 24 steps, all ending in the same normal form. In his 1993 thesis Herman Geuvers stated the conjecture: if every legal term of a pure type system has a normal form, then every reduction terminates. Credited to Barendregt, Geuvers and Klop, it is problem 9 on the list of open problems in typed lambda calculus. Partial results, by translations into a calculus where nothing is thrown away, covered classes of systems without dependent types, from Xi and Sørensen in the late 1990s to Mull in 2023.

1:32The claim

Result 245 is one OpenAI preprint, 72 pages, dated September 25, 2026. It claims the conjecture for beta reduction, for every pure type system: if every legal expression in every valid context has a beta normal form, every beta reduction sequence of a legal expression terminates. No assumption that a sort has only one type, or that each rule fixes one sort for a function type; open contexts allowed; and reduction inside type annotations counts. Not claimed: that a single term with a normal form is strongly normalizing; the version with eta reduction, which Geuvers also conjectured; normalization of any particular system; or extensions with inductive types, as in Coq or Lean.

2:23How the proof goes

First, reduce to finitely many sorts. Then give each normal type a profile, the set of sorts it inhabits, and arrange the profiles in a graph with signed edges: function domains negative, codomains positive. A reducibility argument in the style of Tait and Girard then runs one strongly connected piece of the graph at a time. Two cases are easy: pieces with no odd cycle of signs, handled with a fixed point, and pieces with no function type entirely inside them. The hard case needs a certain forbidden configuration to be absent. If it were present, the system could encode Hurkens’s version of Girard’s paradox as a legal term in an open context, and that term has no normal form, contradicting the hypothesis. So weak normalization is used twice: to normalize types, and to rule out the paradox. We transcribed the paper’s graph conditions and ran them on 11 known systems. The forbidden configuration appears in exactly the three paradoxical systems on our list, System U⁻, System U and Type : Type, and in none of the 8 normalizing ones, including the calculus of constructions. That is consistent with the theorem, not a check of its proof.

3:40Where it stands

The preprint is unrefereed and unchanged since release. In Lean, the theorem is formalized with de Bruijn terms, reduction in annotations and arbitrary specifications, about 29,500 lines with no unproved steps, and the weak normalization hypothesis is genuinely used. We did not build it. OSVerify has not reviewed it, and we found no expert reaction. If it holds, for every pure type system, a guarantee that every legal term can finish already guarantees that every legal term always finishes, the beta half of a conjecture from 1993.