Prove2Me

Magnitude of the gravitational force: F=Gm1m2/r2F = G m_1 m_2 / r^2

Proved
NewtonGravitation.norm_pointForce

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

gravitationmathematical-physics

Let m1,m2≥0m_1,m_2\ge 0 be masses located at distinct points r1≠r2r_1\neq r_2 of E3\mathbb{E}^3. Then the vector force F21F_{21} has magnitude

∥F21∥=G m1m2∥r2−r1∥2.\|F_{21}\| = \frac{G\,m_1 m_2}{\|r_2-r_1\|^2}.

This recovers the scalar form F=Gm1m2/r2F = G m_1 m_2 / r^2 of Newton's law from the vector form, as stated in the source's Vector form section.

Preamble
import Definitions.Def_NewtonGravitation_Defs
import Mathlib

open MeasureTheory NewtonGravitation
Formal statement
namespace NewtonGravitation

theorem norm_pointForce (m₁ m₂ : ℝ) (hm₁ : 0 ≤ m₁) (hm₂ : 0 ≤ m₂) (r₁ r₂ : Space)
    (hr : r₁ ≠ r₂) :
    ‖pointForce m₁ m₂ r₁ r₂‖ = G * m₁ * m₂ / ‖r₂ - r₁‖ ^ 2 := 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≥0m_1\ge0, m2≥0m_2\ge0 and all points r1,r2∈E3r_1, r_2\in\mathbb{E}^3 with r1≠r2r_1\ne r_2, the Euclidean norm of 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) equals

G m1m2∥r2−r1∥2,\frac{G\,m_1 m_2}{\|r_2-r_1\|^2},

with G=6.67430×10−11G = 6.67430\times10^{-11}. The case of a zero mass is included (both sides are 00).

View graph