No perpetual motion machine of the first kind

Proved

FirstLawThermo.no_perpetual_motion_first_kind

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

first-lawinternal-energythermodynamics

Let $\mathcal P$ be a set of processes of a closed system with state set $\sigma$ , and let $U$ be an internal energy for $\mathcal P$ . If $p\in\mathcal P$ is adiabatic and cyclic ( $p_{\mathrm{start}}=p_{\mathrm{finish}}$ ), then the system does no net work:

W(p)=0.

This is the impossibility of a perpetual motion machine of the first kind: no engine working in a cycle can produce net work "from nothing", that is, without energy being resupplied as heat.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.no_perpetual_motion_first_kind {σ : Type*} (procs : Set (Process σ))
    (U : σ → ℝ) (hU : IsInternalEnergy procs U) (p : Process σ) (hp : p ∈ procs)
    (had : p.adiabatic) (hcyc : p.IsCyclic) :
    p.work = 0 := by sorry

Source

Wikipedia, "First law of thermodynamics", revision oldid=1366986255, https://en.wikipedia.org/w/index.php?title=First_law_of_thermodynamics&oldid=1366986255; lead section: "An equivalent statement is that perpetual motion machines of the first kind are impossible; work done by a system on its surroundings requires that the system's internal energy be consumed ..."; Section "Various statements of the law for closed systems": Planck (1897/1903) "it is impossible to construct an engine which will work in a cycle and produce continuous work, or kinetic energy, from nothing."

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 an arbitrary type $\sigma$ , an arbitrary set $\mathcal P$ of processes, a function $U:\sigma\to\mathbb R$ satisfying $U(q_{\mathrm{finish}})-U(q_{\mathrm{start}})=-W(q)$ for every $q\in\mathcal P$ whose adiabatic proposition holds, and a process $p\in\mathcal P$ whose adiabatic proposition holds and with $p_{\mathrm{start}}=p_{\mathrm{finish}}$ :

W(p)=0.

Human review

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

View graph