Overview

This project is dedicated to the formalization of Kepler’s laws of planetary motion using the Lean 4 interactive theorem prover.

Resources