2 papers
cs.LO2026
A Kernel-Clean Lean Mechanization of Classical Lottery in Action and the Wakker--Debreu--Koopmans Representation Layer
Jingyuan Li, Ilia Tsetlin, Fan Wang
We present a Lean 4/Mathlib formalization of the additive representation theory behind Classical Lottery in Action and the Wakker-Debreu-Koopmans (WDK) layer it relies on. Our cent…
stat.ME2026
Betting on Bets: Anytime-Valid Tests for Stochastic Dominance
Sebastian Arnold, Yo Joong Choe, Marco Scarsini +1
How can we monitor, in real time, whether one uncertain prospect has any upside over another? To answer this question, we develop a novel family of sequential, anytime-valid tests…