Formal Verification of the Extended Theory of General Relativity

This deposit contains a fully formalized proof of an extended theory of General Relativity in the Lean 4 proof assistant. The extension adds a quadratic Riemann-squared term and a dynamical scalar field coupling governed by a curvature-dependent function. All key lemmas and theorems—including the variation of the action, the resulting metric and scalar field equations of motion, ghost‐freedom, and symmetric-hyperbolicity—are proved without any “sorry” placeholders. Included in this package:- PDF manuscript with the formal formulations- Lean 4 source files (lake project) implementing all proofs- A CI integration that compiles with `make proof` and shows a green build badge- Instructions for reproduction This work promotes rigorous, machine-checked reasoning in gravitational physics and provides a reusable foundation for further formal developments in relativity and field theory.