Abstract
This paper presents a comprehensive formalization of the vonNeumann-Morgenstern (vNM) expected utility theorem using the Lean 4 interactivetheorem prover. We implement the classical axioms of preference-completeness,transitivity, continuity, and independence-enabling machine-verified proofs ofboth the existence and uniqueness of utility representations. Our formalizationcaptures the mathematical structure of preference relations over lotteries,verifying that preferences satisfying the vNM axioms can be represented byexpected utility maximization. Our contributions include a granular implementation of the independenceaxiom, formally verified proofs of fundamental claims about mixture lotteries,constructive demonstrations of utility existence, and computational experimentsvalidating the results. We prove equivalence to classical presentations whileoffering greater precision at decision boundaries. This formalization provides a rigorous foundation for applications ineconomic modeling, AI alignment, and management decision systems, bridging thegap between theoretical decision theory and computational implementation.