Game Theory

Stream: new members

[Lucas Teixeira]

Is there any game theory formalized in mathlib?? If not, why is that?

[Scott Morrison]

There are combinatorial games in the sense of Conway, but I think nothing else, presumably because no one has done any yet. :-)

[Kevin Buzzard]

"Game Theory" means at least two different things :-/

[Heather Macbeth]

@Andrew Souther might be the person to ask -- see his repo on social choice theory. One basic problem is that we don't have many fixed point theorems yet, although I belive @Yaël Dillies and other are working on this.

[Lucas Teixeira]

Kevin Buzzard said:

"Game Theory" means at least two different things :-/

Such as??

Originally I had the theories covered in a text like this in mind
https://www.amazon.com/Game-Theory-Analysis-Roger-Myerson/dp/0674341163/

[Kevin Buzzard]

In mathematics it means this and this. Looks like you mean the former. Scott was talking about the latter.

[Andrew Souther]

I did recently start a small library of social choice theory in Lean, which I think of as adjacent to game theory. I would be interested in working on game theory, but I sense we need Brouwer's fixed point theorem from topology before I could prove the existence of Nash Equilibrium. Some game theory proofs may also require sophisticated probability theory (??)

[Yury G. Kudryashov]

Are you going to PR it?

[Yaël Dillies]

Oh yeah, we're working towards Brouwer's fixed point theorem on branch#sperner-again, although not at the moment. Bhavik and I will probably get back to it in a month or so now that we're done Szemerédi's regularity lemma.

[Andrew Souther]

PR my social choice theory work?
Tbh, I am still having fun just adding lemmas and building the repo. But I would love to PR soon.
Before the end of the year, I hope to start a conversation on Zulip about what a social choice PR may look like.

[Kevin Buzzard]

If you just prove Arrow's theorem and don't PR it, then all that will happen will be that someone else shows up and asks if we have Arrow's theorem, and someone else might say "it doesn't seem like we do" and then someone else will duplicate the work.

[Kevin Buzzard]

the other thing of course is that in 1 year's time your work won't compile with mathlib master because mathlib master constantly gets refactored and changed to make it better, and repos which don't keep up end up rotting.

[Yaël Dillies]

And your beautiful work will rot in the limbs of the Internet wilderness.

[Bryan Gin-ge Chen]

We also have this page which tracks external Lean projects (there's even a table which shows which Lean versions they're compatible with). This doesn't really solve the problem of rot outside of mathlib, but at least people can find your project there. The instructions at the leanprover-contrib repo even link to some CI scripts which can try to automatically update your project to work with the latest version of Lean / mathlib.

[Andrew Souther]

I do have the CI scripts set up, and I've been playing upgrade_lean whack-a-mole since the summer... Glad to hear there is such interest in the PR, and I will prioritize it before end of year.

[Kevin Buzzard]

that is a game with no end, unless you PR :D

[Eric Wieser]

It probably ends after the lean3 flag day, since I suspect that tool won't be running mathport automatically any time soon

[Mario Carneiro]

it could.. I hope mathport to be useful also for third party projects, not just mathlib

[Scott Morrison]

Daniel had lean-liquid as part of the pipeline for running mathport until I came along. :-) Hopefully once things are a bit more stable we can put it (and other projects?) back in.