Eq. (13): a classical ideal gas with $C_V=\tfrac32R$ violates the third law

Proved

ThirdLawThermo.classical_ideal_gas_entropy_diverges

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

The molar heat capacity at constant volume of a monatomic classical ideal gas is the constant $C_V=\tfrac32R$ , where $R>0$ is the molar gas constant. Fix $T>0$ .

Theorem. The molar entropy difference between $T_0$ and $T$ diverges as $T_0\to0$ :

S(T)-S(T_0)=\int_{T_0}^{T}\frac{\tfrac32R}{t}\,dt\longrightarrow+\infty\qquad(T_0\to0^+).

So a gas with constant heat capacity all the way down to absolute zero contradicts the third law; the source resolves the conflict by quantum statistics (Fermi–Dirac and Bose–Einstein gases) at low temperature.

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem classical_ideal_gas_entropy_diverges (R T : ℝ) (hR : 0 < R) (hT : 0 < T) :
    Tendsto (fun T₀ => ∫ t in T₀..T, (3 / 2 * R) / t) (𝓝[>] 0) atTop := by sorry

end ThirdLawThermo

Source

Wikipedia, "Third law of thermodynamics", revision oldid=1369622029, https://en.wikipedia.org/w/index.php?title=Third_law_of_thermodynamics&oldid=1369622029; section "Consequences", subsection "Specific heat", Eq. (13) ("the molar specific heat at constant volume of a monatomic classical ideal gas ... is given by CV = 3/2 R ... We can verify this more fundamentally by substituting CV in Eq. (14), which yields (13). In the limit T0 → 0 this expression diverges, again contradicting the third law of thermodynamics").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic), the drafting agent itself; non-blind read-back

Disclosure: this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted these Lean statements, with full knowledge of the source text and of the intended meaning. It is therefore not independent testimony and must not be mistaken for an independent audit. Reviewers should check the Lean code against the source themselves.

For all reals $R$ and $T$ with $R>0$ and $T>0$ , the statement asserts

\int_{T_0}^{T}\frac{\tfrac32R}{t}\,dt\to+\infty\quad\text{as }T_0\to0\text{ with }T_0>0 .

No gas, volume or particle number is modelled; the integrand is the constant $\tfrac32R$ divided by $t$ .

View graph

Eq. (13): a classical ideal gas with CV=32RC_V=\tfrac32RCV​=23​R violates the third law

Eq. (13): a classical ideal gas with $C_V=\tfrac32R$ violates the third law