Following up on the discussion in #13248, and the same scope question that came up again on #39393.
Back in 2024, @urkud proposed on #13248: "I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create leanprover-community/GameTheory this weekend, then push some basic theory there." @YaelDillies agreed the material isn't "abstract" enough for core Mathlib and needs room for experimentation. That repo doesn't seem to have been created, and #13248 has been sitting awaiting-author/merge-conflict since.
In the meantime @hcWang942 / Ma Jiajun's group kept building at math-xmum/gametheory:
Zerosum.lean — a complete, 0-sorry, ~830-line proof of von Neumann's minimax theorem via Loomis's theoremMyerson.lean, Auction.lean, OptimalAuctionDesign.lean — mechanism design, mostly closed outMatching.lean — stable matchingNash1.lean / Sperner.lean — Nash equilibrium existence via Sperner's lemma toward Brouwer, still open (the fixed-point step is the hard part and isn't closed yet)
I've been independently working through Lean formalizations in adjacent areas: cooperative game theory (Shapley value, the Bondareva-Shapley core), evolutionary stable strategies, the folk theorem for repeated games, the Gibbard-Satterthwaite and Myerson-Satterthwaite impossibility theorems, Sion's minimax theorem (an independent route from Loomis's), Fenchel duality. I'd rather contribute that into a shared home than let it sit privately. I haven't cross-checked all of it against what's already in math-xmum/gametheory, so there's likely some overlap to sort out (e.g. matching/stable-matching), not a clean non-overlapping addition.
Given all this now genuinely exists across two groups and two years, would it make sense to actually revive the satellite-repo idea?
cc @urkud @YaelDillies @vihdzp who weighed in on scope before.
Following up on the discussion in #13248, and the same scope question that came up again on #39393.
Back in 2024, @urkud proposed on #13248: "I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create
leanprover-community/GameTheorythis weekend, then push some basic theory there." @YaelDillies agreed the material isn't "abstract" enough for core Mathlib and needs room for experimentation. That repo doesn't seem to have been created, and #13248 has been sittingawaiting-author/merge-conflictsince.In the meantime @hcWang942 / Ma Jiajun's group kept building at math-xmum/gametheory:
Zerosum.lean— a complete, 0-sorry, ~830-line proof of von Neumann's minimax theorem via Loomis's theoremMyerson.lean,Auction.lean,OptimalAuctionDesign.lean— mechanism design, mostly closed outMatching.lean— stable matchingNash1.lean/Sperner.lean— Nash equilibrium existence via Sperner's lemma toward Brouwer, still open (the fixed-point step is the hard part and isn't closed yet)I've been independently working through Lean formalizations in adjacent areas: cooperative game theory (Shapley value, the Bondareva-Shapley core), evolutionary stable strategies, the folk theorem for repeated games, the Gibbard-Satterthwaite and Myerson-Satterthwaite impossibility theorems, Sion's minimax theorem (an independent route from Loomis's), Fenchel duality. I'd rather contribute that into a shared home than let it sit privately. I haven't cross-checked all of it against what's already in math-xmum/gametheory, so there's likely some overlap to sort out (e.g. matching/stable-matching), not a clean non-overlapping addition.
Given all this now genuinely exists across two groups and two years, would it make sense to actually revive the satellite-repo idea?
cc @urkud @YaelDillies @vihdzp who weighed in on scope before.