This paper introduces Finitary Physical Mathematics (FPM), a new foundational framework implemented in Lean 4, designed to align theoretical physics with the strict informational and thermodynamic limits of reality. It addresses the fundamental mismatch between the continuous, infinitary axioms of classical Zermelo-Fraenkel set theory (ZFC) and the discrete, resource-bounded nature of the physical universe. By rejecting completed infinities and non-constructive axioms, FPM seeks to resolve long-standing physical pathologies introduced by classical mathematics, including uncomputable variables, unphysical singularities, and the loss of determinism. Within the FPM framework, mathematical objects are redefined as algorithmically generated observables strictly constrained by explicit spatial and temporal precision budgets. The paper details the theoretical architecture of FPM, establishes its core finitary primitives, and demonstrates its viability through a dynamical physical model of a local oscillator. Ultimately, this work provides a foundational theory for a strictly computable, implementation-level mathematics tailored for physical modeling. Keywords: Lean 4, Mathlib, Mathematical Physics, Finitary Mathematics, Ultrafinitism, Theoretical Physics, ZFC Set Theory, Resource-Bounded Computation, Constructivism.
Aziz Arij (Fri,) studied this question.