Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle

Jacques D. Fleuriot, Lawrence C. Paulson

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The approach previously used to mechanise lemmas and Kepler’s Law of Equal Areas from Newton’s Principia [13] is here used to mechanically reproduce the famous Propositio Kepleriana or Kepler Problem. This is one of the key results of the Principia in which Newton demonstrates that the centripetal force acting on a body moving in an ellipse obeys an inverse square law. As with the previous work, the mechanisation is carried out through a combination of techniques from geometry theorem proving (GTP) and Nonstandard Analysis (NSA) using the theorem prover Isabelle. This work demonstrates the challenge of reproducing mechanically Newton’s reasoning and how the combination of methods works together to reveal what we believe to be flaw in Newton’s reasoning.
Original languageEnglish
Title of host publicationAutomated Deduction in Geometry
Subtitle of host publicationSecond International Workshop, ADG’98 Beijing, China, August 1–3, 1998 Proceedings
EditorsXiao-Shan Gao, Dongming Wang, Lu Yang
PublisherSpringer Berlin Heidelberg
Number of pages20
ISBN (Electronic)978-3-540-47997-0
ISBN (Print)978-3-540-66672-1
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle'. Together they form a unique fingerprint.

Cite this