Complete Lean 4 / Mathlib formalization of Monteiro–Tourky: the one-period Kyle model has one equilibrium (arXiv:2607.23585v4). 0 sorry, axiom-clean.
Lean Updated 4 days ago 1 commits
synth-dev|Mirror: shehral/kyle-uniqueness-lean (⭐0)
4 days agoAbout
Complete Lean 4 / Mathlib formalization of Monteiro–Tourky: the one-period Kyle model has one equilibrium (arXiv:2607.23585v4). 0 sorry, axiom-clean.
Readme