Equity Premium
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Abstract
Equity Premium Puzzle — Machine-Checked Formalization
This paper presents 73 machine-verified theorems building on 2 established facts and 3 hypotheses. All results are formally verified in the Lean 4 (103 verification units, 52 proved statements) and exportable to Lean 4.
<!-- TODO: Write a proper abstract summarizing the key contributions -->
Length
984 words
Claims
66 theorems
Status
Skeleton
Novelty
Machine-checked formalization of equity premium puzzle results in a proof assistant, but the paper is a skeleton with no narrative, no abstract, and no exposition — the theorems are listed without mathematical content or context.