Einstein–de Sitter universe: the expansion age is $t=2/(3H)$

Proved

CosmoConstCentury.einstein_de_sitter_age

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

cosmologygeneral-relativitymathematical-physics

Let $G$ and $c$ be real constants and let $(R,\rho)$ solve the Friedmann–Lemaître dust equations with $\Lambda=0$ and flat space ( $k=0$ ) for all times $t>0$ — the Einstein–de Sitter model, whose first equation is the review's (18), $(R'/R)^2=\kappa\rho c^2/3$ . Assume that the universe is expanding, $R'(t)>0$ for all $t>0$ , and that it starts from a big bang at $t=0$ , i.e. $R(t)\to0$ as $t\to0^+$ . Then for every $t>0$ ,

t=\frac{2}{3H(t)},\qquad H=R'/R .

This is the timespan of expansion of the Einstein–de Sitter model quoted in footnote 24 of the review, $t=2/(3H_0)$ .

Formalization Note The predicate IsFriedmannSolution G c Λ k I R ρ requires, at every $t\in I$ , that $R(t)>0$ , that $R$ is $C^2$ in a neighbourhood of $t$ , and that the two equations hold with $\kappa=8\pi G/c^2$ .

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem einstein_de_sitter_age (G c : ℝ) (R ρ : ℝ → ℝ)
    (hsol : IsFriedmannSolution G c 0 0 (Set.Ioi 0) R ρ)
    (hexp : ∀ t > 0, 0 < deriv R t) (hbang : Tendsto R (𝓝[>] 0) (𝓝 0)) :
    ∀ t > 0, t = 2 / (3 * hubbleParam R t) := by sorry

end CosmoConstCentury

Source

C. O'Raifeartaigh, M. O'Keeffe, W. Nahm, S. Mitton, "One hundred years of the cosmological constant: from 'superfluous stunt' to dark energy", Eur. Phys. J. H 43, 73-117 (2018), https://doi.org/10.1140/epjh/e2017-80061-7; Section 5.1, p. 85, eq. (18) (Einstein and de Sitter 1932) and footnote 24 (t = 2/(3H0), Einstein 1933).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Disclosure: non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), at the explicit request of the proposal owner. It is not an independent or blind audit, and it must not be treated as independent testimony: its author knew the source paper and the intended meaning while writing it. Reviewers should compare it against the Lean code themselves.

Let $G,c$ be arbitrary real numbers and $R,\rho:\mathbb R\to\mathbb R$ . Assume:

$(R,\rho)$ is a Friedmann solution with $\Lambda=0$ and $k=0$ on the open half-line $(0,\infty)$ : for every $t>0$ , $R(t)>0$ , $R$ is $C^2$ near $t$ , $\dfrac{3R'(t)^2}{R(t)^2}=\kappa c^2\rho(t)$ and $\dfrac{R'(t)^2}{R(t)^2}+\dfrac{2R''(t)}{R(t)}=0$ (with $\kappa=8\pi G/c^2$ );
$R'(t)>0$ for every $t>0$ ;
$R(t)\to0$ as $t\to0$ from the right.

Conclusion: for every $t>0$ , $t=\dfrac{2}{3H(t)}$ where $H(t)=R'(t)/R(t)$ .

No positivity of $G$ or $c$ is assumed. Nothing is assumed about $R$ at $t\le0$ other than the right limit at $0$ .

Human review

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

View graph

Einstein–de Sitter universe: the expansion age is t=2/(3H)t=2/(3H)t=2/(3H)

Einstein–de Sitter universe: the expansion age is $t=2/(3H)$