Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Value-at-Risk is not subadditive

Proved
CoherentRisk.var_not_subadditive

by viratkota · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

operations-researchprobability

Value-at-Risk violates subadditivity: there are positions whose combined VaR exceeds the sum of their individual VaRs, so under VaR the pooling of positions can appear to increase risk. A witness on 25 states: X loses 100 in state 0 alone and Y loses 100 in state 1 alone, each a single losing state in twenty-five, so at tolerance k=1 both have VaR 0; their sum loses in two states, exceeding the tolerance, giving VaR 100. Note that VaR here counts STATES and refers to no probability measure, per its own definition -- the state count 25 is not load-bearing (two states suffice) and reading k=1 as a 4% tail is an interpretation the formal statement does not make. This is the failure that moved the Basel market-risk standard from Value-at-Risk to Expected Shortfall.

Preamble
import Definitions.Def_CoherentRisk

open CoherentRisk
Formal statement
namespace CoherentRisk

theorem var_not_subadditive :
    ¬ (∀ (m : ℕ) (k : ℕ), Subadditive (fun X : Fin (m+1) → ℝ => VaR X k)) := by
  sorry

end CoherentRisk
Source
Artzner et al. 1999, Section 3: VaR fails subadditivity and therefore penalises diversification.
Human review
  • Endorsed by Shuze Chen · Sep 6, 2026

  • Endorsed by viratkota · Sep 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me