From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem
创建于 更新于
摘要
本文利用Lean 4交互式定理证明器，全面形式化了冯·诺依曼-摩根斯坦(vNM)效用定理，包括偏好公理的机器验证证明、效用表示的存在性及唯一性证明，并提供了严格的独立公理细化及等价性证明。实现了从理论到可执行代码的桥接，推动了经济理论、人工智能对齐及管理科学中决策系统的精确建模与验证 [page::0][page::1][page::7][page::9][page::11][page::15][page::23][page::24][page::39][page::46].
