GCH $\iff \aleph_\alpha=\beth_\alpha$ for all $\alpha$

Proved

ContinuumHypothesis.gch_iff_aleph_eq_beth

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

cardinal-arithmeticset-theory

In terms of the beth numbers ( $\beth_0=\aleph_0$ , $\beth_{\alpha+1}=2^{\beth_\alpha}$ , $\beth_\lambda=\sup_{\alpha<\lambda}\beth_\alpha$ at limits), the generalized continuum hypothesis is equivalent to

\aleph_\alpha=\beth_\alpha\quad\text{for every ordinal }\alpha.

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem gch_iff_aleph_eq_beth : GCH.{u} ↔ ∀ α : Ordinal.{u}, ℵ_ α = ℶ_ α := by sorry

end ContinuumHypothesis

Source

Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Generalized continuum hypothesis', paragraph 2 ('The beth numbers provide an alternative notation for this condition: ℵ_α = ℶ_α for every ordinal α').

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

GCH ⟺ ℵα=ℶα\iff \aleph_\alpha=\beth_\alpha⟺ℵα​=ℶα​ for all α\alphaα

GCH $\iff \aleph_\alpha=\beth_\alpha$ for all $\alpha$