Pith. sign in

REVIEW 3 major objections 6 minor 76 references

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

T0 review · 3 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims a complete Lean 4 proof of the von Neumann-Morgenstern utility theorem: preferences over lotteries satisfying the four classical axioms are exactly expected-utility maximizers, the utility being unique up to scale and…

desk verdict A useful roadmap for formalizing vNM in Lean 4, but the advertised complete machine-checked proof is missing from the paper and deferred to an unpinned GitHub repo. read the letter →

arxiv 2506.07066 v1 pith:AKL2ZNZQ submitted 2025-06-08 econ.TH cs.AIq-fin.CP

Li Jingyuan This is my paper
classification econ.THcs.AIq-fin.CP MSC 91B1603B3568V20
keywords vonNeumann-MorgensternutilitytheoremLean4formalverificationexpectedpreferenceaxiomsindependenceaxiominteractiveprovinglotteries
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that the von Neumann-Morgenstern (vNM) expected-utility theorem has been proved in the Lean 4 proof assistant: any preference over lotteries that satisfies completeness, transitivity, continuity, and independence is exactly the maximization of the expected value of a utility function, and that function is unique up to positive affine transformations. If the claim holds, one of the foundational results of decision theory becomes a machine-checked artifact in which no hidden assumption or proof gap can survive, and the vNM axioms turn into executable procedures for deriving utilities from preferences. The formalization achieves tractability by splitting the independence axiom into a strict-preference version and an indifference version, and Theorem 7.4 verifies that this granular pair is equivalent to the classical single biconditional formulation, with the split handling boundary cases more explicitly. The stated motivation is to give AI alignment, reward learning, and management decision systems a provably rational, code-level foundation for preference modeling.

What carries the argument

The carrying objects are the lottery space $\Delta(X)$, defined as functions $p : X \to \mathbb{R}$ with non-negative entries summing to one, and the mixture operation $\mathrm{mix}(p,q,\alpha)(x) = \alpha p(x) + (1-\alpha)q(x)$, which makes the space convex. The argument's centerpiece is the indifference-mixture construction: for the best and worst degenerate lotteries $p^*$ and $p^\circ$, Claim 5.5 uses the continuity axiom to guarantee a unique $\alpha^* \in [0,1]$ with $\mathrm{mix}(p^*,p^\circ,\alpha^*) \sim q$, and the utility of each outcome is defined as exactly that $\alpha$. Claim 5.2, the monotonicity of mixtures under strict preference, then converts preference comparisons between arbitrary lotteries into comparisons of the real numbers $\mathrm{EU}(p,u)$. The remaining load-bearing piece is the granular independence axiom, split into strict-preference preservation (A3a) and indifference preservation (A3b), which Theorem 7.4 proves equivalent to the classical biconditional axiom while making boundary handling explicit.

What would settle it

A reader can fetch the repository named in the data-availability statement, build it against the stated Lean 4 and mathlib versions, and locate the theorem corresponding to Theorem 6.1. If that theorem is missing, fails to compile, or depends on `axiom`, `sorry`, or `admit` statements — as the appendix's reward-learning and preference-oracle declarations explicitly do — the claimed machine verification does not exist; the same check applies to `vnm_utility_construction`, which the paper leaves as a placeholder returning the constant zero.

Watch

Extended reading notes

Core claim

The central claim, stated as Theorems 6.1 and 6.2, is that for a non-empty finite outcome set $X$, any binary relation $\succsim$ on the lottery space $\Delta(X)$ that satisfies order, continuity, and independence admits a utility function $u : X \to \mathbb{R}$ with $p \succsim q \iff \mathrm{EU}(p,u) \geq \mathrm{EU}(q,u)$ for all lotteries $p,q$, and that any two representing functions are related by $v = \alpha u + \beta$ with $\alpha > 0$. The proof route is constructive: the paper selects the most- and least-preferred degenerate lotteries $p^*$ and $p^\circ$, then assigns each outcome $x$ the unique mixing weight $\alpha_x \in [0,1]$ for which the degenerate lottery $\delta_x$ is indifferent to the mixture $\mathrm{mix}(p^*,p^\circ,\alpha_x)$, with existence and uniqueness supplied by Claim 5.5. The representation is then derived from the monotonicity of mixtures and the granular independence axiom, whose equivalence to the classical formulation is itself a formally proved theorem. The paper presents this as a machine-verified development in Lean 4, with the caveat, stated in its own appendix, that the displayed code covers the utility construction and the rest of the existence proof is deferred.

Load-bearing premise

The whole claim rests on the repository named in the paper's data-availability statement actually containing a Lean 4 proof that compiles and completes Theorem 6.1, since the paper itself shows only the utility-function setup and says the rest 'would continue as follows'.

Editorial extensions

If this is right

  • If the Lean 4 formalization is complete, the vNM theorem becomes a machine-checkable artifact in which no appeal to 'obvious' continuity arguments or boundary handling can hide, because every inference is verified by the proof kernel.
  • The granular independence axiom is interchangeable with the classical one, so future formalizations of expected-utility theory can adopt whichever formulation is easier to automate without changing the theory.
  • The constructive proof route makes utility elicitation algorithmic: finding the indifference weight that equates an outcome to a mixture of the best and worst outcomes is an executable procedure, not merely an existence argument.
  • Utility uniqueness up to positive affine transformations is verified, confirming formally that only ratios of utility differences carry meaning and that preference measurement is scale-invariant.
  • The framework is intended to carry over to applied settings: utility-based preferences are proved consistent with the independence axiom, and the paper sketches verified structures for AI-alignment constraints, reward learning from preference data, and safe exploration policies.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The preprint itself withholds the main proof: Appendix A.10.5 says the displayed code 'primarily sets up the utility function and proves some of its basic properties' and that the rest 'would continue as follows', so until the linked repository is inspected and compiled, the theorem is asserted rather than exhibited.
  • The appendix's AI-alignment and preference-oracle statements are introduced with `axiom`, and the utility-construction function is left as a placeholder returning the constant zero, so the computational-experiment claims are not machine-checked in the same sense as (allegedly) the main theorem; a reader should separate the formal core from the sketched applications.
  • The granular-versus-classical independence equivalence is likely transferable: other expected-utility frameworks (Savage, Anscombe-Aumann, or dynamic choice) face the same boundary delicacies at $\alpha = 0$ and $\alpha = 1$, and the same split could simplify their mechanization, a line the paper does not pursue.
  • If the Lean proof is completed, the most interesting logical payoff is explicitness about where continuity enters: Claim 5.5, the indifference-mixture existence step, is where the theorem leans on continuity, and a verified proof would reveal exactly how much of the axiom is needed at every branch point.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper claims to provide a complete Lean 4 formalization of the von Neumann–Morgenstern expected utility theorem, including machine-verified proofs of both the existence and uniqueness of utility representations, an equivalence result for formulations of the independence axiom, computational experiments, and applications to AI and management science. The mathematical exposition follows the standard textbook proof: lotteries are probability distributions, the utility function is constructed from indifference mixtures between best and worst degenerate lotteries, and uniqueness is derived up to positive affine transformations. The central problem is that the machine-checked proofs are not present in the manuscript. Appendix A.10.5 explicitly states that the code snippet only sets up the utility function and some basic properties and that the full proof 'would continue as follows'; the application sections rely on unproved axioms and placeholder definitions; and the single GitHub link is unpinned. As submitted, the advertised formal artifact is not verifiable.

Significance. If the Lean 4 artifact were supplied and compiling, the work could be a useful contribution to the mechanization of economic theory and to clarifying boundary conditions in the vNM axioms. The definitions of Lottery and mix are natural, the granular treatment of the independence axiom is sensible, and the informal proof sketches in the appendices are largely coherent. The Section 8 result that utility-based preferences satisfy the independence axiom is a legitimate side theorem, assuming the displayed proof and the invoked lemma expectedUtility_mix are correct. These strengths do not, however, offset the absence of the main formal proofs, which are the paper's stated central contribution.

major comments (3)
  1. [Appendix A.10.5 / Theorem 6.1] The central claim of a machine-verified existence proof is not substantiated. Appendix A.10.5 states that the included code snippet 'primarily sets up the utility function and proves some of its basic properties' and that the full proof 'would continue as follows'; the two steps that carry the theorem—showing p ∼ L(EU(p,u)) and deriving p ≿ q ⇔ EU(p,u) ≥ EU(q,u)—are only described in prose. Theorem 6.2 has the same status: Appendix A.11 is a traditional proof sketch with no complete Lean code listing. The Data Availability Statement gives only an unpinned GitHub URL with no commit hash, file manifest, or build instructions. Consequently, the abstract's assertion of 'machine-verified proofs of both the existence and uniqueness of utility representations' cannot be checked from the manuscript, and this gap is load-bearing for the paper's main contribution.
  2. [§9.4, Listing 5] The section titled 'Computational Evidence: Extracting and Running the Verified Code' does not provide executable verified code. In Listing 5, vnm_utility_construction is explicitly a placeholder returning fun x => 0, the preference oracle stockMarketPreferencesOracle always returns true, compliance of that oracle is introduced as axiom h_oracle_consistent, and the two #eval commands are commented out. The advertised outputs (AAPL → 0.85, etc.) are therefore not produced by any code shown in the paper. This undermines the claimed contribution of 'executable implementations of utility representations' and shows that the application layer relies on unproved axioms rather than verified constructions.
  3. [§9.2, Listing 3] The reward-learning 'provable guarantees' rest on an unproved axiom: axiom reward_learning_vnm_compliant asserts that a model fitting a consistent dataset yields an IsPrefRel preference relation. No proof is supplied, and the predicate IsPrefRel includes only completeness and transitivity, not continuity or independence, so the label 'vnm_compliant' overstates what is formalized. While this application does not directly bear on Theorem 6.1, the pattern of replacing proofs with axioms in the paper's own examples makes it impossible to distinguish verified results from assumed ones. The axioms need to be clearly separated and disclosed as assumptions, and the main theorem's proof needs to be supplied completely and independently.
minor comments (6)
  1. [§3, Definition 3.1] The summation in the definition of a lottery appears as 'P x∈X p(x) = 1' rather than with a proper sum symbol; please correct the notation.
  2. [§9.4, Listing 5] The code block contains a corrupted splice: the comment '-- Outputs: [AAPL → 0.85, ...]' is immediately followed by a fragment of the earlier typeclass theorem, making the listing unreadable at lines 57–60.
  3. [References] Reference [31] begins with an extraneous comma: '[31] , Wang, F.'; please fix.
  4. [§8] Section 8 is described as 'computational experiments validating the results,' but the only content is a theorem that utility-based preferences satisfy the independence axiom. This is a consistency result rather than an experimental validation, and the supporting lemma expectedUtility_mix is invoked without a displayed proof.
  5. [§7.4] The labeling of the formulation requiring only p ≿ q ≿ r as the 'classical continuity axiom' could confuse readers; the usual textbook version also assumes the non-degenerate case p ≻ r, so the strict condition should be stated explicitly.
  6. [Abstract / Introduction] The words 'complete' and 'comprehensive' outrun the content currently supplied; they should be qualified once a full artifact with a pinned commit is actually provided.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the vNM derivation is a genuine formalization from axioms, not a repackaged input.

full rationale

The derivation chain is not circular. The vNM representation is obtained constructively: best and worst degenerate lotteries are selected using finiteness and totality; each outcome's utility is defined as the unique mixing weight that yields indifference (Claim 5.5), whose existence and uniqueness are proved from the stated continuity and independence axioms; and the representation is then verified by linearity of expected utility. No parameter is fitted to data and then renamed a prediction, and no load-bearing premise is imported from the authors' own prior work. The only substantive caveat is an omitted-proof/artifact-verifiability issue, not a circular one: Appendix A.10.5 says the supplied Lean snippet 'primarily sets up the utility function and proves some of its basic properties' and that the full proof 'would continue as follows,' so the machine-checked proof of Theorem 6.1 is not present in the preprint. Similarly, the application sections introduce explicit unproved axioms (reward_learning_vnm_compliant, h_oracle_consistent), but these are labeled as axioms/placeholders and do not feed back into the vNM derivation. Section 8's demonstration that expected-utility maximizers satisfy independence is a definitional sanity check rather than a load-bearing inference, and it does not make the main theorem circular.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The core formalization uses standard vNM axioms as assumptions. The main free-parameter ledger is empty. However, the application sections add unproven axioms and placeholders that are not part of the central theorem.

assumptions (6)
  • domain assumption Preference relation is complete and transitive (A1)
    Defined in Section 4.1 as the Order axiom; assumed without proof.
  • domain assumption Continuity axiom A2
    Defined in Section 4.1; guarantees existence of mixtures strictly better and strictly worse than an intermediate lottery.
  • domain assumption Independence axiom A3
    Defined in Section 4.1 with strict and indifference versions.
  • domain assumption Finite nonempty outcome set X with decidable equality
    Assumed in Section 3 to define lotteries and use Finset sums; the main theorem is restricted to this setting.
  • ad hoc to paper reward_learning_vnm_compliant
    Declared as an axiom in Section 9.2, not proved; asserts that a sufficient, consistent dataset yields a complete and transitive learned preference.
  • ad hoc to paper h_oracle_consistent and h_oracle_consistent_proof
    Declared as axioms in Section 9.4 to certify a stub oracle; the oracle always returns true and no proof of vNM compliance is given.

how reviews work

0 comments
Cite this review

Pith. "Pith review of From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem." pith.science (2026). https://pith.science/paper/AKL2ZNZQ

@misc{pith2026250607066,
  author       = {Pith},
  title        = {Pith review of: From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AKL2ZNZQ}},
  note         = {Machine review of arXiv:2506.07066}
}
read the original 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.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

76 extracted references · 73 canonical work pages

  1. [1]

    Abdellaoui, M. (2007). Rank-Dependent Utility. In R. F. Engle & D. L. McFadden (Eds.), Handbook of Utility Theory, 689-750. Springer

    work page 2007

  2. [2]

    Allais, M. (1953). Le Comportement de l’Homme Rationnel devant le Risque: Critique des Postulats et Axiomes de l’ ´Ecole Am´ ericaine,Econometrica, 21(4), 503-546

    work page 1953

  3. [3]

    Baillon, A., Huang, Z., Selim, A., & Wakker, P. P. (2018). Measuring Ambiguity Attitudes for All (Natural) Events. Econometrica, 86(5), 1839-1858. [Online appendix, dataset, stimuli & code available]

    work page 2018

  4. [4]

    Baillon, A., Halevy, Y., & Li, C. (2022). Randomize at your Own Risk: on the Observability of Ambiguity Aversion. Econometrica, 90(3), 1085-1107

    work page 2022

  5. [5]

    Baillon, A., Bleichrodt, H., Li, C., & Wakker, P. P. (forthcoming). Source Theory: a tractable and positive ambiguity theory. Management Science

    work page

  6. [6]

    Barberis, N. C. (2013). Thirty Years of Prospect Theory in Economics: A Review and Assessment. Journal of Economic Perspectives , 27(1), 173-196

    work page 2013

  7. [7]

    Chew, S. H. (1983). A Generalization of the Quasilinear Mean with Applications to the Measurement of Income Inequality and Decision Theory Resolving the Allais Paradox. Econometrica, 51(4), 1065-1092

    work page 1983

  8. [8]

    Cerreia-Vioglio, S., Maccheroni, F., Marinacci, M., & Montrucchio, L. (2011). Uncertainty Averse Preferences. Journal of Economic Theory , 146(4), 1275-1330

    work page 2011

Show all 76 references
  1. [9]

    Diecidue, E., & Wakker, P. P. (2018). On the Intuition of Rank-Dependent Utility. Journal of Risk and Uncertainty, 57(1), 15-28

    2018

  2. [10]

    Ellsberg, D. (1961). Risk, Ambiguity, and the Savage Axioms. The Quarterly Journal of Economics , 75(4), 643-669

    1961

  3. [11]

    G., & Schneider, M

    Epstein, L. G., & Schneider, M. (2003). Recursive Multiple-priors. Journal of Economic Theory , 113(1), 1-31

    2003

  4. [12]

    Ghirardato, P., Maccheroni, F., & Marinacci, M. (2004). Differentiating Ambiguity and Ambiguity Attitude. Journal of Economic Theory , 118(2), 133-173

    2004

  5. [13]

    Gilboa, I., & Schmeidler, D. (1989). Maxmin Expected Utility with Non-unique Prior. Journal of Mathematical Economics, 18(2), 141-153

    1989

  6. [14]

    P., & Sargent, T

    Hansen, L. P., & Sargent, T. J. (2008). Robustness. Princeton University Press

    2008

  7. [15]

    Kahneman, D., & Tversky, A. (1979). Prospect theory: An analysis of decision under risk. Econometrica, 47(2), 263-291

    1979

  8. [16]

    Klibanoff, P., Marinacci, M., & Mukerji, S. (2005). A Smooth Model of Decision Making under Ambiguity. Econometrica, 73(6), 1849-1892

    2005

  9. [17]

    de Moura, L., Kong, S., Avigad, J., van Doorn, F., & von Raumer, J. (2021). The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28 , Lecture Notes in Computer Science

    2021

  10. [18]

    de Moura, L., et al. (2024). Lean 4 Theorem Prover. https://lean-lang.org/

    2024

  11. [19]

    J., & Siniscalchi, M

    Machina, M. J., & Siniscalchi, M. (2014). Ambiguity and Ambiguity Aversion.Handbook of the Economics of Risk and Uncertainty , 1, 729-807

    2014

  12. [20]

    The mathlib Community. (2020). The Lean Mathematical Library. Proceedings of the 9th ACM SIG- PLAN International Conference on Certified Programs and Proofs, 367-381. https://doi.org/10.1145/ 3372885.3373824 26

    2020

  13. [21]

    Marinacci, M., & Montrucchio, L. (2004). Introduction to the Mathematics of Ambiguity. Uncertainty in Economic Theory, 46-107

    2004

  14. [22]

    Quiggin, J. (1982). A Theory of Anticipated Utility. Journal of Economic Behavior and Organization , 3(4), 323-343

    1982

  15. [23]

    Quiggin, J. (1993). Generalized Expected Utility Theory: The Rank-Dependent Model . Kluwer Academic Publishers

    1993

  16. [24]

    Russell, S. (2019). Human Compatible: Artificial Intelligence and the Problem of Control . Viking

    2019

  17. [25]

    Schmeidler, D. (1989). Subjective Probability and Expected Utility without Additivity. Econometrica, 57(3), 571-587

    1989

  18. [26]

    Strzalecki, T. (2011). Axiomatic Foundations of Multiplier Preferences. Econometrica, 79(1), 47-73

    2011

  19. [27]

    Tversky, A., & Kahneman, D. (1992). Advances in Prospect Theory: Cumulative Representation of Uncertainty. Journal of Risk and Uncertainty , 5(4), 297-323

    1992

  20. [28]

    Starmer, C., & He, Y. (2019). Probability Weighting, Stop-Loss and the Disposition Effect. Journal of Mathematical Economics, 81, 28-37

    2019

  21. [29]

    von Neumann, J., & Morgenstern, O. (1944). Theory of Games and Economic Behavior . Princeton University Press

    1944

  22. [30]

    Wakker, P. P. (2010). Prospect Theory: For Risk and Ambiguity . Cambridge University Press

    2010

  23. [31]

    , Wang, F. (2022). Rank-Dependent Utility under Multiple Priors, Management Science, 68, 8166-8183

    2022

  24. [32]

    Yaari, M. E. (1987). The Dual Theory of Choice under Risk. Econometrica, 55(1), 95-115. 27 A Appendix A.1 Proof of Proposition 3.3 We need to verify that L satisfies the two conditions for being a lottery. Let p, q∈ ∆(X ) and 0 ≤ α ≤ 1

    1987

  25. [33]

    • Since q is a lottery, q(x) ≥ 0

    Non-negativity: For any x ∈ X: • Since p is a lottery, p(x) ≥ 0. • Since q is a lottery, q(x) ≥ 0. • Given 0 ≤ α ≤ 1, we have α ≥ 0. • Also, 0 ≤ α =⇒ −α ≤ 0 = ⇒ 1 − α ≤ 1. And α ≤ 1 = ⇒ −α ≥ −1 = ⇒ 1 − α ≥ 0. So, 0 ≤ 1 − α ≤ 1. In particular, 1 − α ≥ 0. (In Lean, h one minus α...

  26. [34]

    Lean: rw [p.property.2, q.property.2]) = α + (1 − α) = 1 (by arithmetic, Lean: by ring) Since both conditions are satisfied, L = mix(p, q, α) is a lottery

    Sum to one: We calculate the sum of L(x) over all x ∈ X: X x∈X L(x) = X x∈X (α · p(x) + (1 − α) · q(x)) = X x∈X α · p(x) + X x∈X (1 − α) · q(x) (by linearity of finite sum, Lean: Finset.sum add distrib) = α X x∈X p(x) + (1 − α) X x∈X q(x) (factoring out constants, Lean: Finset...

  27. [35]

    We want to showp ≻ r

    T ransitivity of Strict Preference (≻): Assume p ≻ q and q ≻ r. We want to showp ≻ r. By definition of strict preference (Definition 4.5): (H1) p ≻ q =⇒ p ≿ q and ¬(q ≿ p). (H2) q ≻ r =⇒ q ≿ r and ¬(r ≿ q). We need to show two things for p ≻ r: (a) p ≿ r: From (H1), we have p ...

  28. [36]

    In either case, p ≿ p holds

    Reflexivity of Preference ( ≿): For any p ∈ ∆(X ), by completeness (Axiom A1a), we have p ≿ p ∨ p ≿ p. In either case, p ≿ p holds. (Lean: lemma PrefRel.refl (p : Lottery X) : p ⪰ p := (PrefRel.complete p p).elim id id)

  29. [37]

    Assume for contradiction that p ≻ p

    Irreflexivity of Strict Preference ( ≻): We want to show ¬(p ≻ p). Assume for contradiction that p ≻ p. By definition of strict preference, p ≻ p =⇒ p ≿ p ∧ ¬(p ≿ p). This is a contradiction of the form A ∧ ¬A. Thus, ¬(p ≻ p). (Lean: instance : IsIrrefl (Lottery X) strictPref ...

  30. [38]

    We want to show p ∼ q2

    T ransitivity of Indifference (∼): Assume p ∼ q1 and q1 ∼ q2. We want to show p ∼ q2. By definition of indifference (Definition 4.5): (H1) p ∼ q1 =⇒ p ≿ q1 and q1 ≿ p. (H2) q1 ∼ q2 =⇒ q1 ≿ q2 and q2 ≿ q1. We need to show two things for p ∼ q2: (a) p ≿ q2: From (H1), p ≿ q1. Fr...

  31. [39]

    Non-negativity: For any y ∈ X, δxval (y) is either 1 or 0, both of which are ≥ 0

  32. [40]

    Sum to one : X y∈X δxval (y) = δxval (xval) + X y∈X ,y̸=xval δxval (y) = 1 + X y∈X ,y̸=xval 0 = 1 + 0 = 1 Thus, δxval ∈ ∆(X ). (Lean: let δ : X → Lottery X := fun x val => <fun y => if y = x val then 1 else 0, by constructor; ...>) A.10.2 Step 2: Existence of Best and W orst D...

  33. [41]

    This means for any a ∈ Sδ, ¬(a ≻ ps)

    Let ps = δxs be an element in Sδ that is ”minimal” in the sense of Lean’s Finset.exists minimal. This means for any a ∈ Sδ, ¬(a ≻ ps). (Lean: let h greatest lottery := Finset.exists minimal s univ hs nonempty; rcases h greatest lottery with <p s, <hp s in s univ, h ps le all>>...

  34. [42]

    Let a = δx

    We want to show ps ≿ δx for any x ∈ X. Let a = δx. So we have ¬(δx ≻ ps)

  35. [43]

    This is equivalent to ¬(δx ≿ ps) ∨ (ps ≿ δx)

    ¬(δx ≻ ps) means ¬(δx ≿ ps ∧ ¬(ps ≿ δx)). This is equivalent to ¬(δx ≿ ps) ∨ (ps ≿ δx). (Lean: unfold strictPref at h not delta x’ lt p s; push neg at h not delta x’ lt p s which results in ¬(δ x ⪰ p s) ∨ (p s ⪰ δ x) if we use ⪰ for pref.)

  36. [44]

    Then, from ¬(δx ≿ ps) ∨ (ps ≿ δx), since the first part ¬(δx ≿ ps) is false, the second part ps ≿ δx must be true

    Consider two cases based on PrefRel.complete (δ x) p s: • Case (i): δx ≿ ps. Then, from ¬(δx ≿ ps) ∨ (ps ≿ δx), since the first part ¬(δx ≿ ps) is false, the second part ps ≿ δx must be true. (Lean: by cases h : δ x’ ⪰ p s; exact h not delta x’ lt p s h) • Case (ii): ¬(δx ≿ ps...

  37. [45]

    This is equivalent to ¬(pc ≿ δx) ∨ (δx ≿ pc)

    We have ¬(pc ≻ δx), which means ¬(pc ≿ δx ∧ ¬(δx ≿ pc)). This is equivalent to ¬(pc ≿ δx) ∨ (δx ≿ pc)

  38. [46]

    This is the desired conclusion

    Consider two cases based on PrefRel.complete (δ x) p c: • Case (i): δx ≿ pc. This is the desired conclusion. (Lean: cases PrefRel.complete (δ x) p max with | inl h delta pref pmax => ...‘. If δx ≻ pc, then δx ≿ pc. If δx ∼ pc, then δx ≿ pc) • Case (ii): pc ≿ δx (and ¬(δx ≿ pc)...

  39. [47]

    This is a crucial step, often called the ”linearity” property of the preference relation or the ”reduction of compound lotteries” if extended

    Show p ∼ L(EU(p, u)) for any p ∈ ∆(X ). This is a crucial step, often called the ”linearity” property of the preference relation or the ”reduction of compound lotteries” if extended. It typically relies on repeated application of the Independence Axiom (A3) to decomposep into ...

  40. [48]

    From the previous step, we have p ∼ L(EU(p, u)) and q ∼ L(EU(q, u))

    Establish the representation p ≿ q ⇐ ⇒EU(p, u) ≥ EU(q, u). From the previous step, we have p ∼ L(EU(p, u)) and q ∼ L(EU(q, u)). Therefore, p ≿ q ⇐ ⇒L(EU(p, u)) ≿ L(EU(q, u)). • If p∗ ≻ p◦ (Case 2 of utility definition): L(α) = mix(p∗, p◦, α). By Claim II (monotonicity of mixtu...

  41. [49]

    Utility-Based Preference Relation Definition 1 def utilityBasedPref (u : X \to Real) (p q : Lottery X) : Prop := 2 expectedUtility p u \ge expectedUtility q u This definition formalizes the core concept of utility-based preferences: • Given a utility function u that assigns re...

  42. [50]

    intro h 17 have h_ineq : \a * expectedUtility p u \ge \a * expectedUtility q u := by 18 apply mul_le_mul_of_nonneg_left h (le_of_lt h_\a.1) 19 linarith 20

    Independence Axiom Verification 1 /-- Verify that utility-based preferences satisfy the independence axiom -/ 2 theorem utility_based_independence 3 {X : Type} [Fintype X] [Nonempty X] [DecidableEq X] 4 (u : X \to Real) (p q r : Lottery X) (\a : Real) (h_\a : 0 < \a \and \a \l...

  43. [51]

    Theorem Statement: It shows that utility-based preferences satisfy the independence axiom - if p is preferred to q, then mixing both with a third lottery r with the same probability α preserves this preference

  44. [52]

    Proof Structure: • Unfolds the definition of utilityBasedPref • Uses expectedUtility mix lemma to rewrite the expected utilities of mixed lotteries • Shows both directions of the if-and-only-if ( ↔) statement: (i) Forward direction: If p is preferred to q, then their mixtures ...

  45. [53]

    Mathematical Machinery: • Uses mul le mul of nonneg left to multiply an inequality by a non-negative number • Uses le of mul le mul left to divide both sides by a positive number • Uses linarith tactic to solve linear arithmetic goals

  46. [54]

    Technical Details: • Handles dependent type parameters carefully with notation and explicit parameter passing • Properly manages the implicit proof arguments for Lottery.mix that ensure α is between 0 and 1 A.14 Detailed Explanation Formal Foundations for AI Alignment in Secti...

  47. [55]

    The comment notes that these preferences may not satisfy rationality axioms - reflecting the reality that human preferences can be inconsistent or violate VNM axioms

    Human Preferences 1 humanPrefs : Lottery X \to Lottery X \to Prop This defines a binary relation representing human preferences over lotteries. The comment notes that these preferences may not satisfy rationality axioms - reflecting the reality that human preferences can be in...

  48. [56]

    If for all lotteries r, humans prefer p to r whenever they prefer q to r, then the AI should prefer p to q

    Deference Principle 1 deferencePrinciple : \forall p q : Lottery X, 2 (\forall r : Lottery X, humanPrefs p r \to humanPrefs q r) \to pref p q This is a formal representation of the principle that the AI should respect clear human preferences. If for all lotteries r, humans pre...

  49. [57]

    This is the vNM utility theorem: preferences satisfying the vNM axioms can be represented by expected utility maximization

    Utility Representation 1 utility_represents : \forall p q : Lottery X, 2 pref p q \lr expectedUtility p utilityFn \ge expectedUtility q utilityFn This proves that the AI’s preferences can be represented by expected utility maximization under its utility function. This is the v...

  50. [58]

    PrefDataset Structure 1 structure PrefDataset (X : Type) [Fintype X] [Nonempty X] [DecidableEq X] where 2 /-- List of preference pairs (p \succ q) -/ 3 pairs : List (Lottery X \times Lottery X) This structure represents training data for learning preferences: • Contains a list...

  51. [59]

    datasetCoverage 1 def datasetCoverage (data : PrefDataset X) : Prop := 2 data.pairs.length > 0 -- Simplified implementation - checks if dataset is non-empty This function checks if a dataset has sufficient coverage: • In this simplified implementation, it just checks that the ...

  52. [60]

    consistentPreferences 1 def consistentPreferences (data : PrefDataset X) : Prop := 2 \forall (p q : Lottery X), 3 (p, q) \in data.pairs \to \not((q, p) \in data.pairs) -- No direct contradictions This checks for consistency in the preference dataset: • It verifies there are no...

  53. [61]

    modelFitsData 1 def modelFitsData (model : RewardModel X) (data : PrefDataset X) : Prop := 2 \forall (pair : Lottery X \times Lottery X), pair \in data.pairs \to 3 model.pref pair.1 pair.2 This checks if a reward model correctly fits the training data: • For every preference p...

  54. [62]

    IsPrefRel 43 1 def IsPrefRel (pref : Lottery X \to Lottery X \to Prop) : Prop := 2 (\forall p q : Lottery X, pref p q \or pref q p) \and -- Completeness 3 (\forall p q r : Lottery X, pref p q \to pref q r \to pref p r) -- Transitivity This defines what it means for a preferenc...

  55. [63]

    reward learning vnm compliant (Axiom) 1 axiom reward_learning_vnm_compliant 2 {X : Type} [Fintype X] [Nonempty X] [DecidableEq X] 3 (data : PrefDataset X) (model : RewardModel X) 4 (h_sufficient_coverage : datasetCoverage data) 5 (h_consistent : consistentPreferences data) 6 (...

  56. [64]

    vnm utility construction 1 def vnm_utility_construction (pref : PrefRel X) : X \to Real := 2 -- This is a placeholder implementation 3 -- In a complete implementation, this would construct a utility function 4 -- that represents the given preference relation 5 fun x => 0 This ...

  57. [65]

    It maps each state-action pair to a real-valued utility, capturing how desirable that action is in that state for achieving the task goal

    Base Utility Function 1 baseUtility : S \to A \to Real This represents the primary task objective (reward function) that the policy aims to optimize. It maps each state-action pair to a real-valued utility, capturing how desirable that action is in that state for achieving the...

  58. [66]

    Higher values represent safer actions in a given state

    Safety Constraint Function 1 safetyValue : S \to A \to Real This function quantifies the safety level of each state-action pair. Higher values represent safer actions in a given state

  59. [67]

    Actions with safety values below this threshold are considered unsafe and should be avoided

    Safety Threshold 1 safetyThreshold : Real This defines the minimum acceptable safety level. Actions with safety values below this threshold are considered unsafe and should be avoided

  60. [68]

    For each state, it returns a lottery (probability distribution) over possible actions

    Exploration Policy 1 policy : S \to Lottery A This is the actual policy mapping states to probability distributions over actions. For each state, it returns a lottery (probability distribution) over possible actions

  61. [69]

    Safety Guarantee 1 safety_guarantee : \forall s : S, \forall a : A, 2 (policy s).val a > 0 \to safetyValue s a \ge safetyThreshold This is a formal proof that the policy is safe: if an action has non-zero probability in any state (i.e., might be selected), then its safety valu...

  62. [70]

    This guarantees rational decision-making

    vNM Compliance 1 vnm_compliant : \forall s : S, 2 IsPrefRel (\lambda p q : Lottery A => expectedUtility p (\lambda x => baseUtility s x) \ge 3 expectedUtility q (\lambda x => baseUtility s x)) This ensures that when comparing different action distributions in any state, the po...

  63. [71]

    Example Type Definition 1 inductive ExampleStock 2 | AAPL 3 | MSFT 4 | GOOG 5 | AMZN 6 deriving Fintype, DecidableEq 7 8 instance : Nonempty ExampleStock := \<ExampleStock.AAPL\> This code: • Defines a concrete finite type ExampleStock with four constructors representing diffe...

  64. [72]

    Sample Preference Oracle 1 def stockMarketPreferencesOracle : Lottery ExampleStock -> Lottery ExampleStock -> Bool := 2 -- This is just a placeholder implementation 3 fun p q => true -- Always prefer the first option by default This defines: • A preference oracle that compares...

  65. [73]

    46 14 2)) = true \and 15 prefOracle (@Lottery.mix X _ p r \b (le_of_lt h_conj.2.2.1) (le_of_lt h_conj.2.2

    vNM Compliance Typeclass 1 class PreferenceOracleCompliant {X : Type} [Fintype X] [DecidableEq X] (prefOracle : Lottery X -> 2 Lottery X -> Bool) where 3 complete : \forall p q : Lottery X, prefOracle p q = true \or prefOracle q p = true 4 transitive : \forall p q r : Lottery ...

  66. [74]

    Axiomatized Compliance 1 axiom h_oracle_consistent_proof : \exists h : PreferenceOracleCompliant stockMarketPreferencesOracle, 2 True 3 axiom h_oracle_consistent : PreferenceOracleCompliant stockMarketPreferencesOracle 4 attribute [instance] h_oracle_consistent These axioms: •...

  67. [75]

    12 -- The goal is to prove prefOracle r p = false

    Utility Elicitation Implementation 1 def elicitUtility {X : Type} [Fintype X] [Nonempty X] [DecidableEq X] 2 (prefOracle : Lottery X -> Lottery X -> Bool) 3 [h_oracle_compliant : PreferenceOracleCompliant prefOracle] : X \to Real := 4 -- Implementation using the constructive p...

  68. [76]

    Commented-Out Evaluation 1 --#eval elicitUtility stockMarketPreferencesOracle 2 -- Outputs: [AAPL \to 0.85, MSFT \to 0.72, GOOG \to 0.65, ...] 3 --#eval elicitUtility stockMarketPreferencesOracle h_oracle_consistent 4 -- Outputs: [AAPL \to 0.85, MSFT \to 0.72, GOOG \to 0.65, ....

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.