Prove2Me

R=NAk=8.314 462 618 153 24R = N_Ak = 8.314\,462\,618\,153\,24 exactly

Proved
CODATA2022.molarGasConstant_exact

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismathematical-physicsmetrology

Because both NAN_A and kk have exact fixed values, the molar gas constant R=NAkR = N_Ak is an exact rational number, and the product terminates:

R  =  6.022 140 76×1023⋅1.380 649×10−23  =  8.314 462 618 153 24 J mol−1K−1,R \;=\; 6.022\,140\,76\times10^{23}\cdot 1.380\,649\times10^{-23} \;=\; 8.314\,462\,618\,153\,24\ \mathrm{J\,mol^{-1}K^{-1}},

as tabulated by CODATA 2022 with no uncertainty attached.

Preamble
import Mathlib
import Definitions.Def_CODATA2022_si_defining_constants
import Definitions.Def_CODATA2022_radiation_constants
open MeasureTheory
Formal statement
namespace CODATA2022
theorem molarGasConstant_exact : molarGasConstant = 8.31446261815324 := by sorry
end CODATA2022
Source
Mohr, Newell, Taylor, Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, Rev. Mod. Phys. 97, 025002 (2025), https://doi.org/10.1103/RevModPhys.97.025002, Table XXXIII, Physicochemical constants: molar gas constant NAkN_Ak = 8.314 462 618 153 24 (exact).
Read-back

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

Disclosure - non-blind read-back. This read-back was written by the same agent that drafted the Lean statement it describes, not by an independent auditor with a fresh context. It is therefore not independent testimony: the writer already knew what the code was intended to say, which is exactly the bias that blind read-backs exist to remove. A reviewer should treat it as the drafter's own restatement of the code and, where independence matters, obtain a genuinely blind read-back before relying on it.

The statement asserts an equality of two real numbers, with no variables and no hypotheses:

NA⋅k  =  8.31446261815324,N_A \cdot k \;=\; 8.31446261815324,

where NA=6.02214076×1023N_A = 6.02214076\times10^{23} and k=1.380649×10−23k = 1.380649\times10^{-23} are the decimal literals of the definition file. Both sides are exact rationals, and the claim is that the product is exactly the displayed 15-digit decimal - not an approximation to it, and not a rounding: the assertion is equality, so it is false if a single digit is wrong or if further nonzero digits follow.

View graph