From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem
Li Jingyuan
econ.TH
Jun 8, 2025 · v1
TL;DR
Formalizes the von Neumann-Morgenstern expected utility theorem, including existence and uniqueness, in Lean 4.
Abstract
This paper presents a comprehensive formalization of the von Neumann-Morgenstern (vNM) expected utility theorem using the Lean 4 interactive theorem prover. We implement the classical axioms of preference-completeness, transitivity, continuity, and independence-enabling machine-verified proofs of both the existence and uniqueness of utility representations. Our formalization captures the mathematical structure of preference relations over lotteries, verifying that preferences satisfying the vNM axioms can be represented by expected utility maximization. Our contributions include a granular implementation of the independence axiom, formally verified proofs of fundamental claims about mixture lotteries, constructive demonstrations of utility existence, and computational experiments validating the results. We prove equivalence to classical presentations while offering greater precision at decision boundaries. This formalization provides a rigorous foundation for applications in economic modeling, AI alignment, and management decision systems, bridging the gap between theoretical decision theory and computational implementation.
Problem
The von Neumann-Morgenstern expected utility theorem is foundational to decision theory but lacked a comprehensive machine-verified formalization, leaving a gap between theoretical economics and computational implementation.
Approach
The authors formalize the vNM utility theorem in Lean 4, implementing the classical axioms (completeness, transitivity, continuity, independence) and constructing machine-verified proofs of both existence and uniqueness of utility representations over lotteries. The formalization includes a granular implementation of the independence axiom and constructive demonstrations of utility existence.
Results
Both existence and uniqueness of the vNM utility representation are formally verified in Lean 4, with equivalence to classical presentations demonstrated. Computational experiments validate the formal results.
