From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem

ArXiv ID: 2506.07066 “View on arXiv”

Authors: Li Jingyuan

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.

Keywords: expected utility theorem, formal verification, decision theory, interactive theorem prover, lotteries

Complexity vs Empirical Score

  • Math Complexity: 9.0/10
  • Empirical Rigor: 2.0/10
  • Quadrant: Lab Rats
  • Why: The paper relies heavily on advanced formal mathematics, including measure theory and dependent type theory for axiomatization in Lean 4, which pushes the math complexity to the upper end of the scale. However, it lacks real-world data or backtesting, focusing instead on theoretical verification, resulting in low empirical rigor.
  flowchart TD
    A["Research Goal<br>Formalize vNM Utility Theorem<br>in Lean 4"] --> B["Methodology: Axioms<br>Completeness, Transitivity,<br>Continuity, Independence"]
    B --> C["Input: Lotteries<br>Preference Relations"]
    C --> D["Computational Process<br>Mechanized Proofs<br>Mixture Properties"]
    D --> E["Outcome: Verified Theorem<br>Existence & Uniqueness<br>of Utility Representation"]
    E --> F["Applications<br>Economic Modeling, AI Alignment,<br>Decision Systems"]