Prove2Me

F=NAe=96 485.332 123 310 0184F = N_Ae = 96\,485.332\,123\,310\,0184 exactly

Proved
CODATA2022.faradayConstant_exact

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

analysismathematical-physicsmetrology

The Faraday constant F=NAeF = N_Ae is likewise exactly known:

F  =  6.022 140 76×1023⋅1.602 176 634×10−19  =  96 485.332 123 310 0184 C mol−1,F \;=\; 6.022\,140\,76\times10^{23}\cdot 1.602\,176\,634\times10^{-19} \;=\; 96\,485.332\,123\,310\,0184\ \mathrm{C\,mol^{-1}},

the value tabulated by CODATA 2022 without uncertainty.

Preamble
import Mathlib
import Definitions.Def_CODATA2022_si_defining_constants
import Definitions.Def_CODATA2022_radiation_constants
open MeasureTheory
Formal statement
namespace CODATA2022
theorem faradayConstant_exact : faradayConstant = 96485.3321233100184 := 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: Faraday constant NAeN_Ae = 96 485.332 123 310 0184 (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⋅e  =  96485.3321233100184,N_A \cdot e \;=\; 96485.3321233100184,

where NA=6.02214076×1023N_A = 6.02214076\times10^{23} and e=1.602176634×10−19e = 1.602176634\times10^{-19} are the decimal literals of the definition file. Both sides are exact rationals; the claim is exact equality with the displayed decimal, including its final digits, not an approximate agreement.

View graph