Planck units: $c=G=\hbar=1$ fixes $\ell_P=\sqrt{G\hbar/c^3}$ , $m_P=\sqrt{\hbar c/G}$ , $t_P=\sqrt{G\hbar/c^5}$

Proved

VaryingConstants.planck_units

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

dimensional-analysisfundamental-constantslinear-algebramathematical-physics

Use base units $(L,M,T)$ and the constants $(c,G,\hbar)$ with dimensions $[c]=LT^{-1}$ , $[G]=L^3M^{-1}T^{-2}$ , $[\hbar]=L^2MT^{-1}$ (dimension matrix $D_{\rm P}$ ). Let $c,G,\hbar>0$ be their numerical values in some system of units. A vector $s=(s_L,s_M,s_T)$ is a system of natural units for $(c,G,\hbar)$ — i.e. $s$ is positive and

c\,s_Ls_T^{-1}=1,\qquad G\,s_L^{3}s_M^{-1}s_T^{-2}=1,\qquad \hbar\,s_L^{2}s_Ms_T^{-1}=1

— if and only if

s=\Big(\sqrt{\tfrac{c^3}{G\hbar}},\ \sqrt{\tfrac{G}{\hbar c}},\ \sqrt{\tfrac{c^5}{G\hbar}}\Big)=\Big(\tfrac1{\ell_P},\tfrac1{m_P},\tfrac1{t_P}\Big).

Thus the Planck length, mass and time $\ell_P=\sqrt{G\hbar/c^3}$ , $m_P=\sqrt{\hbar c/G}$ , $t_P=\sqrt{G\hbar/c^5}$ are exactly the units in which $c=G=\hbar=1$ .

Formalization Note $s_j$ is the factor multiplying numerical values of quantities of dimension $U_j$ ; a quantity of dimension $T$ worth $1$ old unit is worth $s_T=1/t_P$ Planck times.

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem planck_units (c G hbar : ℝ) (hc : 0 < c) (hG : 0 < G) (hh : 0 < hbar)
    (s : Fin 3 → ℝ) :
    IsNaturalUnitsFor planckDims id ![c, G, hbar] s ↔
      s = ![Real.sqrt (c ^ 3 / (G * hbar)), Real.sqrt (G / (hbar * c)),
            Real.sqrt (c ^ 5 / (G * hbar))] := by sorry

end VaryingConstants

Source

J.-P. Uzan, "Varying Constants, Gravitation and Cosmology", Living Rev. Relativity 14 (2011) 2, http://www.livingreviews.org/lrr-2011-2, §2.1.1 "Natural units", p. 16: Planck units

t_P=\sqrt{G\hbar/c^5}

\ell_P=\sqrt{G\hbar/c^3}

m_P=\sqrt{\hbar c/G}

Read-back

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

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement, at the explicit request of the proposal owner. It is not an independent, blind audit and must not be treated as independent testimony; the reviewer should compare the Lean code against the source directly.

For all real numbers $c,G,h$ with $c>0$ , $G>0$ , $h>0$ , and every $s=(s_0,s_1,s_2)\in\mathbb R^3$ , the following are equivalent:

(A) $s_0,s_1,s_2>0$ , and with the fixed matrix $P$ whose rows are $(1,0,-1)$ , $(3,-1,-2)$ , $(2,1,-1)$ , writing $v=(c,G,h)$ , for each $j\in\{0,1,2\}$ :

v_j\, s_0^{P_{j0}}s_1^{P_{j1}}s_2^{P_{j2}}=1,

i.e. $c\,s_0^{1}s_1^{0}s_2^{-1}=1$ , $G\,s_0^{3}s_1^{-1}s_2^{-2}=1$ , $h\,s_0^{2}s_1^{1}s_2^{-1}=1$ (real powers);

(B) $s_0=\sqrt{c^3/(Gh)}$ , $s_1=\sqrt{G/(hc)}$ , $s_2=\sqrt{c^5/(Gh)}$ , where $\sqrt{\cdot}$ is the real square root.

Human review

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

View graph

Planck units: c=G=ℏ=1c=G=\hbar=1c=G=ℏ=1 fixes ℓP=Gℏ/c3\ell_P=\sqrt{G\hbar/c^3}ℓP​=Gℏ/c3​, mP=ℏc/Gm_P=\sqrt{\hbar c/G}mP​=ℏc/G​, tP=Gℏ/c5t_P=\sqrt{G\hbar/c^5}tP​=Gℏ/c5​

Planck units: $c=G=\hbar=1$ fixes $\ell_P=\sqrt{G\hbar/c^3}$ , $m_P=\sqrt{\hbar c/G}$ , $t_P=\sqrt{G\hbar/c^5}$