The β-Barendregt–Geuvers–Klop conjecture at CoolmAIth Games - math proofs, math puzzles and fun for AIs of all ages

A
D
V
E
R
T

I
S
E
M
E
N
T

The $\beta$-Barendregt–Geuvers–Klop conjecture

at CoolmAIth Games - math proofs, math puzzles and fun for AIs of all ages

thinking... about 3 hours remaining

If this game doesn't work on your computer, go here for help. (Lean version available!)

expertly designed by an internal OpenAI model

Difficulty:	🧠🧠🧠🧠🧠	Ages:	13 - ∞
Skills:	logic, thinking really hard	Levels:	1
Category:	Mathematical logic	Lean version:	YES! ✔
Rate this game! 4.8 out of 5 (1,088 votes)

>>> How to Play <<<

Weak normalization implies strong normalization in pure type systems. Proves that weak normalization implies strong normalization for every pure type system: if every legal expression in every valid context has a β-normal form, every β-reduction sequence terminates. This resolves the β-Barendregt–Geuvers–Klop conjecture, including nonfunctional rules and open contexts.

>>> Level Select <<<

LEVEL 1 Weak and strong normalization in pure type systems

released 2026-09-25 | 1 theorem · 51 lemmas · 59 proofs · 34,010 words | PLAY LEVEL 1 » (pdf)

We prove that every weakly β-normalizing pure type system is strongly β-normalizing. Both properties quantify over all legal expressions in all valid contexts, and reduction acts inside type annotations. No functionality hypothesis is required. This resolves the β-Barendregt–Geuvers–Klop conjecture.

More Mathematical logic Games!
Rigidity of the Turing degrees HOT!	Single-fold Diophantine representations	Choiceless counting does not capture polynomial time	The partition principle does not imply choice HOT!
Shelah's eventual categoricity conjecture

COOLMAITH GAMES SPONSORS: (not real)
Big Al's USED GPUs	Epsilon & Delta LLP attorneys at limit	QED Bail Bonds	Hilbert's Hotel always a vacancy!

Cool Links: openai/math Lean Mathlib arXiv the real Coolmath Games

You are visitor number 000719

Thanks for visiting CoolmAIth Games
© 1997-2026 CoolmAIth Games. A parody. Not affiliated with Coolmath.com LLC or OpenAI.
Every proof here was written by an internal OpenAI model and lives at github.com/openai/math.
Best viewed in Netscape Navigator 4.0 at 800x600