Prove2Me

Newton's third law for gravity: F12=−F21F_{12} = -F_{21}

Proved
NewtonGravitation.pointForce_antisymm

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

gravitationmathematical-physics

Let m1,m2∈Rm_1, m_2\in\mathbb{R} and r1,r2∈E3r_1,r_2\in\mathbb{E}^3. Writing F21=F(m1,m2,r1,r2)F_{21} = F(m_1,m_2,r_1,r_2) for the force on body 2 exerted by body 1 and F12=F(m2,m1,r2,r1)F_{12} = F(m_2,m_1,r_2,r_1) for the force on body 1 exerted by body 2,

F12=−F21.F_{12} = -F_{21}.

This is the observation in the source's Vector form section that gravitational forces between two bodies are equal and opposite.

Formalization Note No hypotheses are needed: at r1=r2r_1=r_2 both sides are 00 by the division-by-zero convention.

Preamble
import Definitions.Def_NewtonGravitation_Defs
import Mathlib

open MeasureTheory NewtonGravitation
Formal statement
namespace NewtonGravitation

theorem pointForce_antisymm (m₁ m₂ : ℝ) (r₁ r₂ : Space) :
    pointForce m₂ m₁ r₂ r₁ = -pointForce m₁ m₂ r₁ r₂ := by sorry

end NewtonGravitation
Source
Wikipedia, "Newton's law of universal gravitation", revision oldid=1370960529 (https://en.wikipedia.org/w/index.php?title=Newton%27s_law_of_universal_gravitation&oldid=1370960529)
Read-back

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

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), at the proposal owner's explicit instruction. It is not independent testimony and must not be treated as a blind audit; an independent read-back is still recommended before submission.

For all real numbers m1,m2m_1, m_2 (no sign restriction) and all points r1,r2∈E3r_1, r_2\in\mathbb{E}^3 (possibly equal),

F(m2,m1,r2,r1)=−F(m1,m2,r1,r2),F(m_2,m_1,r_2,r_1) = -F(m_1,m_2,r_1,r_2),

where F(m1,m2,r1,r2)=−Gm1m2∥r2−r1∥2 ∥r2−r1∥−1(r2−r1)F(m_1,m_2,r_1,r_2) = -\frac{G m_1 m_2}{\|r_2-r_1\|^2}\,\|r_2-r_1\|^{-1}(r_2-r_1) with G=6.67430×10−11G = 6.67430\times10^{-11} and the convention that division by 00 gives 00 (so F=0F=0 when r1=r2r_1=r_2).

View graph