Minkowski space is a vacuum solution

Proved

EinsteinFieldEquationsD.minkowski_vacuum_solution

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

differential-geometryeinstein-field-equationsgeneral-relativity

The Minkowski metric $\eta=\operatorname{diag}(-1,1,1,1)$ on $\mathbb{R}^4$ is a smooth nondegenerate symmetric metric on all of $\mathbb{R}^4$ , it is Ricci-flat, and it solves the vacuum field equations with zero cosmological constant (for any coupling $\kappa$ ).

Preamble

import Mathlib
import Definitions.Def_EinsteinFieldEquationsD_Defs

Formal statement

namespace EinsteinFieldEquationsD

theorem minkowski_vacuum_solution (κ : ℝ) :
    IsMetricOn minkowskiMetric Set.univ ∧
      (∀ x : Coord 4, ∀ a b : Fin 4, ricci minkowskiMetric x a b = 0) ∧
      EinsteinFieldEquationsOn minkowskiMetric 0 0 κ Set.univ := by sorry

end EinsteinFieldEquationsD

Source

Wikipedia, "Einstein field equations", revision oldid=1374672993, https://en.wikipedia.org/w/index.php?title=Einstein_field_equations&oldid=1374672993; section 'Vacuum field equations'

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements it describes, with full knowledge of the source and of the intended meaning. It is not the output of a blind, independent auditor, and no reviewer should treat it as such. Compare it against the Lean code yourself.

Here $\kappa$ is an arbitrary real and $\eta$ is the constant field on $\mathbb{R}^4$ whose value at every point is the diagonal matrix $\operatorname{diag}(-1,1,1,1)$ .

Claim. All three of the following hold:

$\eta$ is a metric on $\mathbb{R}^4$ (the whole space is open, components are $C^\infty$ , $\eta$ is symmetric and $\det\eta\neq0$ everywhere);
for every $x\in\mathbb{R}^4$ and all $a,b$ : $R_{ab}(x)=0$ for the Ricci tensor of $\eta$ ;
for every $x\in\mathbb{R}^4$ and all $a,b$ : $G_{ab}(x)+0\cdot\eta_{ab}=\kappa\cdot0$ , i.e. the field equations hold with $T\equiv0$ and $\Lambda=0$ .

Human review

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

View graph