Nash's equation

John Nash's handwritten field equation for gravity, checked in Lean for every dimension and every metric.

Open the interactive version, no install needed.

In his last years John Nash wrote out, by hand, a field equation for gravity and two consequences of it:

□G^ab + G^ps (2 R_p^a_s^b − ½ g^ab R_ps) = 0

□R + ((n − 4)/(2n − 4)) (2 R^ps R_ps − R²) = 0        (the trace, in n dimensions)

□R^ab + 2 R^ps R_p^a_s^b − R R^ab − (g^ab/(2n − 4)) (2 R^ps R_ps − R²) = 0

"It is notable," he wrote, "that for 2 dims there is degeneracy and for 4 dims reduction to □R = 0."

This project proves all of that in Lean, and proves one thing that is not on the page.

In plain words

John Nash (1928–2015) is best known for game theory: the "Nash equilibrium" behind his 1994 Nobel prize in economics, and the film A Beautiful Mind. Mathematicians know him just as well for his work on geometry and on the equations that describe the physical world, which won him the Abel Prize in 2015.

In his last years he worked on gravity. Einstein taught us that matter bends space and time, and that the bending is gravity. Nash wrote down his own equation for that bending, and two consequences of it.

Lean, a computer proof assistant, has now checked both consequences, in any number of dimensions. It also proves something that is not on his page. The simplest model of a universe whose expansion speeds up, as ours does, obeys Nash's equation only when spacetime has four dimensions, the number we live in. And in his equation the rate of that expansion is not built into the law: any rate works.

"Checked in Lean" means a computer verified every step of the reasoning, down to the basic rules of logic, so none of it rests on anyone's say-so. Tenet, a second and independent checker, then re-checked every step.

For mathematicians

Nash's equation is a fourth-order vacuum equation for the metric: □G^ab carries four derivatives. Every Ricci-flat metric solves it, since G = 0, so every vacuum solution of general relativity does.

Everything is proved at a point, for any dimension n and any metric of any signature, over the rationals. The inputs are:

• a symmetric metric g_ab with inverse g^ab;
• a Riemann tensor R_pasb that is antisymmetric in its first pair and symmetric under swapping pairs;
• the values □R^ab and □R at the point, tied by □R = g_ab □R^ab.

Because ∇g = 0, □ passes through raising, lowering and contracting, so those values are the only way □ enters. The Ricci tensor is Nash's contraction, R_ps = g^ab R_pasb, on the second and fourth indices. With the opposite sign convention the same algebra goes through with R_p^a_s^b negated.

On the page:

Theorem	What it says
trace_nash	The trace of Nash's equation is ((2 − n)/2) □R + ((4 − n)/4)(2 R^ps R_ps − R²)
scalar_reduction	For n ≠ 2, every solution satisfies □R + ((n − 4)/(2n − 4))(2 R^ps R_ps − R²) = 0
two_dims	In two dimensions □R drops out of the trace: the degeneracy
four_dims	In four dimensions every solution has □R = 0
nash_eq_nashR, trace_nashR	The □R^ab form differs from the original by g^ab/2 times the scalar reduction
nash_iff_nashR	For n ≠ 2, Nash's equation and the □R^ab form have exactly the same solutions

Not on the page:

Theorem	What it says
einstein	If R_ab = k g_ab and □R^ab = 0, the left side is k²(1 − n/2)(2 − n/2) g^ab
einstein_solves_iff	So an Einstein space solves Nash's equation exactly when k = 0, n = 2 or n = 4
constCurv_ric, constCurv_solves_iff	A space of constant curvature K has R_ab = K(n − 1) g_ab, and solves the equation exactly when K = 0, n = 2 or n = 4
deSitter_four	De Sitter and anti-de Sitter space of every curvature solve Nash's equation in four dimensions
deSitter_other	…and in no other dimension from three up, unless flat

For n ≥ 3 the hypothesis □R^ab = 0 is automatic: the contracted Bianchi identity makes k constant (Schur's lemma). In four dimensions the curvature K of de Sitter space is free, so the cosmological constant is a constant of integration rather than a coupling in the equation.

The widget also shows the full left side of Nash's equation for de Sitter space, computed by Lean component by component from the Riemann tensor: zero in four dimensions, −η in three. #eval Nash.deSitterTable 5 gives 12 η in five, about fifteen seconds of computation.

The trace, in four dimensions	De Sitter space: zero in four dimensions, not in five

Not covered: the Lagrangian on the page, ∫ √−g (2 R^ps R_ps − R²). Deriving field equations from it needs the calculus of variations, which this project does not attempt.

Every theorem depends only on Lean's standard axioms. Tenet, Lean Studio's independent kernel, re-checks all 105 declarations: 105 verified, none resting on an assumption, none rejected.

Try it in Lean Studio

1. Install Lean Studio (on a Mac: brew install --cask keithadler/tap/lean-studio).
2. Clone this repository and open the folder: Open Folder, then pick nash-lean.
3. Open Nash.lean, click on the last line (#widget NashWidget with widgetProps) and choose the Infoview tab.

It works the same in VS Code with the Lean 4 extension. It uses core Lean only, with no Mathlib, so it builds in seconds:

lake build

Files

• Nash.lean: the definitions, the proofs, and the widget's data
• widget/Nash.js: the widget (React, nothing beyond what the infoview provides)
• docs/: the browser version; scripts/build-docs.sh refreshes it from Lean

Made in memory of John Nash, with Lean Studio and the assistance of Claude (Anthropic).

MIT License.