collaborators

1 paper

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…