Weak normalization implies strong normalization in pure type systems with βη-conversion, proved in Lean
A Lean proof, written by Claude Opus 5.5 under four authors' direction by adapting OpenAI's proof of the β case, that in every pure type system with βη-conversion, if every legal term is weakly normalizing then every legal term is strongly normalizing, the βη form of a conjecture Geuvers stated in 1993.
- Lab
- Independent
- Model
- Claude Opus 5.5 in Claude Code, adapting an OpenAI Lean proof of the β case
- Field
- Computer science
- Date
- 2026-10-27
- Human collaborators
- Ankit Pradhan, Cole Vick, Ruijie Fang, Carl Kwan
- Problem posed
- 1993 · open 33 yrs
What was found
The Barendregt-Geuvers-Klop conjecture asks whether weak normalization implies strong normalization in every pure type system; Geuvers states it for all of them in his 1993 thesis as Conjecture 8.1.2. OpenAI's release of 6 October 2026 included a preprint and Lean proof of the case where the conversion rule uses β-conversion only, family 245 of the collection recorded at 2026-10-06-openai-math-collection. This development proves the βη case for every specification, with no functionality, finiteness or decidability assumed: weak βη-normalization of every legal term implies strong βη-normalization, and so does weak β-normalization. Because an η-step can delete a λ-annotation, the proof works from the weaker property that every legal term has a β-reduct with no β-redex outside its λ-domains, handles conversion through domain erasure, indexes candidates by βη-normal forms of erased types and makes observation values η-canonical. OpenAI's 33 Lean files for the β case are copied in and ported to Lean v4.35.0.
Novelty check
arXiv, 2026-10-29: abs:"strong normalization" AND abs:"pure type systems" returned 3 records and abs:"Barendregt-Geuvers-Klop" returned none; none claims either case of the conjecture. The repository cites Geuvers's 1993 thesis for the statement and names no earlier proof of the βη case. Within this registry OpenAI's β-case proof is one family of 2026-10-06-openai-math-collection with no entry of its own, and no entry covers either case. The 2026-10-29 watch run surfaced this through its Palomar registration.
Caveats and known objections
Graded formal on the Palomar registration, which certifies that the proof typechecks against the recorded statement under the three standard axioms; a scan of all 71 Lean files at the registered commit found no axiom declarations, no native_decide, and sorry only in Challenge.lean, where the statement is left open by construction. Whether Challenge.lean states the conjecture as Geuvers meant it is a separate reading: it defines annotated pseudo-terms with de Bruijn indices, the seven typing rules of the βη system and strong normalization as accessibility, and nobody independent of the authors is on record as having audited it. Two neighbouring statements are explicitly not proved: the system with a strengthening rule, and Geuvers's Conjecture 8.1.3, that strong normalization of the β system implies it for the βη system. The proof follows the architecture of OpenAI's argument, so it is evidence that the argument adapts rather than an independent route; OpenAI's base case is an unrefereed manuscript from an unreleased model, though its Lean files build here, so the formal grade covers them. The project metadata records endorsement from both OpenAI and Geuvers as not contacted. Autonomy is collaborative: the metadata says Claude Opus 5.5 adapted the proof to βη and wrote all of the Lean except OpenAI's files, under the direction of the human authors, and the construction it adapted came from a different lab's model, so neither the authors' direction nor this model's work accounts for the result alone.
Machine-checked elsewhere
PalomarWeak and strong βη-normalization in pure type systems with βη-conversion
PALOMAR-2026-10-27-000027 · localmotiveproofs/PTS-beta-eta at 9d0b54a7d5f6 · checked 2026-10-27
ProvedPureTypeSystem.weak_implies_strong_betaEtaPureTypeSystem.weak_beta_implies_strong_betaEta
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Permitted axioms are exactly propext, Quot.sound and Classical.choice. Palomar records trust level high and archives a fork of the repository.
No independent check is recorded on this entry yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Weak normalization implies strong normalization in pure type systems with βη-conversion, proved in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-27-pts-beta-eta-normalizationBibTeX
@misc{whataifound-independent-2026-normalization,
title = {Weak normalization implies strong normalization in pure type systems with βη-conversion, proved in Lean},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-10-27-pts-beta-eta-normalization}
}