Conservation of momentum from Newton's third law

Proved

ConservationLaws.momentum_conservation_of_third_law

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

conservation-lawmechanicsmomentum

Let $N$ particles in $\mathbb{R}^d$ have masses $m_i > 0$ , velocities $v_i(t)$ and accelerations $a_i(t) = \dot v_i(t)$ . Suppose the only forces are internal forces $F_{ij}(t)$ (force on $i$ due to $j$ ) obeying Newton's third law $F_{ij}(t) = -F_{ji}(t)$ , and Newton's second law $m_i a_i(t) = \sum_j F_{ij}(t)$ holds. Then the total momentum $P(t) = \sum_i m_i v_i(t)$ is constant: $P(t) = P(s)$ for all $t, s$ .

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem momentum_conservation_of_third_law
    {d N : ℕ} (m : Fin N → ℝ) (hm : ∀ i, 0 < m i)
    (v a : Fin N → ℝ → EuclideanSpace ℝ (Fin d))
    (F : Fin N → Fin N → ℝ → EuclideanSpace ℝ (Fin d))
    (hthird : ∀ i j t, F i j t = -F j i t)
    (hv : ∀ i t, HasDerivAt (v i) (a i t) t)
    (hnewton : ∀ i t, m i • a i t = ∑ j, F i j t) :
    ∀ t s, ∑ i, m i • v i t = ∑ i, m i • v i s := by sorry

end ConservationLaws

Source

Wikipedia, "Momentum" (uploaded PDF), https://en.wikipedia.org/wiki/Momentum, section "Conservation" (total change in momentum of interacting particles is zero)

Read-back

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

Disclosure: NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent or blind testimony and must not be treated as such by any reviewer. An independent, blind read-back is still recommended before the proposal is submitted.

Fix natural numbers $d$ and $N$ . Let $m_1,\dots,m_N$ be real numbers with $m_i > 0$ for every $i$ . Let $v_i, a_i : \mathbb{R} \to \mathbb{R}^d$ ( $i = 1,\dots,N$ ) be functions, where $\mathbb{R}^d$ is Euclidean space, and let $F_{ij} : \mathbb{R} \to \mathbb{R}^d$ be functions for every ordered pair $(i,j)$ , including $i = j$ . Assume:

$F_{ij}(t) = -F_{ji}(t)$ for all $i, j, t$ (in particular $F_{ii}(t) = 0$ );
for every $i$ and every $t$ , $v_i$ is differentiable at $t$ with derivative $a_i(t)$ ;
for every $i$ and $t$ , $m_i\, a_i(t) = \sum_{j=1}^N F_{ij}(t)$ (sum over all $j$ , including $j = i$ ).

Conclusion: for all real $t, s$ ,

\sum_{i=1}^N m_i v_i(t) = \sum_{i=1}^N m_i v_i(s).

Edge cases: $N = 0$ makes both sums zero; $d = 0$ makes $\mathbb{R}^d$ a single point. No position functions appear. The positivity of the masses is assumed but the conclusion does not mention it.

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