Paper: arXiv 2505.12840

Authors: Jingyuan Li

Abstract

This paper introduces and formally verifies a novel geometric framework for first-order stochastic dominance (FSD) in $N$ dimensions using the Lean 4 theorem prover. Traditional analytical approaches to multi-dimensional stochastic dominance rely heavily on complex measure theory and multivariate calculus, creating significant barriers to formalization in proof assistants. Our geometric approach characterizes $N$-dimensional FSD through direct comparison of survival probabilities in upper-right orthants, bypassing the need for complex integration theory. We formalize key definitions and prove the equivalence between traditional FSD requirements and our geometric characterization. This approach achieves a more tractable and intuitive path to formal verification while maintaining mathematical rigor. We demonstrate how this framework directly enables formal analysis of multi-dimensional economic problems in portfolio selection, risk management, and welfare analysis. The work establishes a foundation for further development of verified decision-making tools in economics and finance, particularly for high-stakes domains requiring rigorous guarantees.

Complexity vs Empirical Score

  • Math Complexity: 8.0/10
  • Empirical Rigor: 1.5/10
  • Quadrant: Lab Rats — theoretically deep, empirically untested

Why this score: The paper relies heavily on advanced mathematical formalization using the Lean 4 theorem prover and measure-theoretic concepts, but focuses on theoretical equivalence proofs and does not involve backtesting, real data, or implementation-ready strategies.

Research Flowchart

  flowchart TD
  G["Research Goal: Formalize N-Dim FSD"] --> M["Geometric Framework via Survival Probabilities"]
  M --> I["Input: Random Vectors & Orthants"]
  I --> C["Computation: Lean 4 Theorem Prover"]
  C --> F1["Equivalence Proven"]
  C --> F2["Tractable Integration Bypassed"]
  F1 & F2 --> O["Outcomes: Verified Framework & Economic Applications"]
  O --> O1["Portfolio Selection"]
  O --> O2["Risk Management"]