Basics of game theory?

Stream: Is there code for X?

[Ilmārs Cīrulis]

Is there anything already?

If not, I will slowly (and lazily) do it, probably. (It allows me to understand the material better, for one.)
Does anyone want to join?

[Shreyas Srinivas]

There are a couple of PRs adding game theoretic stuff. One of them is mine, and another is on auction theory (I don't know the author's zulip)

[Ilmārs Cīrulis]

Greetings!

What's in your PR?

[Shreyas Srinivas]

Discrete fair division

[Violeta Hernández]

What kind of game theory? We've got a bunch of stuff on the combinatorial side

[Ilmārs Cīrulis]

I translated part of course description (apologies for possibly weird English):

1. Examples, intuition and formal definition (of strategic game).
2. Extensive form with full information.
3. Extensive form with partial information.
4. Convex game
5. Nash equilibrium in convex games
6. Cournot model of oligopoly, patent competitions and other examples of convex games.
7. Existence of Nash equilibrium in mixed strategies.
8. Ecological game and other games with parameter.
9. Finding Nash equilibrium in mixed strategies for games of size 2*n.
10. Finding Nash equilibrium in mixed strategies for games of size 3x3.
11. Notion of Bayesian game.

That's what I will be studying and trying to formalize at least partly (because that helps me to understand better :sweat_smile: ).

[Shreyas Srinivas]

So this is game theory of the strategic interactions variety

[Alexander Hicks]

The existence theorem would be interesting, but I don't know if the Brouwer or Kakutani fixed point theorems are in mathlib?

[Yaël Dillies]

Brouwer is formalised outside of mathlib. Kakutani I still hope to do one day, but it's not a priority at the moment

[Shreyas Srinivas]

Alexander Hicks said:

The existence theorem would be interesting, but I don't know if the Brouwer or Kakutani fixed point theorems are in mathlib?

existence of what?

[Shreyas Srinivas]

Fwiw, sperner's lemma with triangulations is the more interesting version for games. I know only the triangle version of this

[Alexander Hicks]

Shreyas Srinivas said:

Alexander Hicks said:

The existence theorem would be interesting, but I don't know if the Brouwer or Kakutani fixed point theorems are in mathlib?

existence of what?

Existence of a nash equilibrium i.e., every finite game has a mixed strategy Nash equilibrium (there exists a few variations of this).

[Violeta Hernández]

Question, is there any overarching definition for a game (of this strategic kind)? Or are there multiple overlapping notions?

[Violeta Hernández]

I was thinking about a certain infamous IMO problem the other day, and how it would even be formalized. I think you could frame it as asking for an existence of a strategy in a certain two player game with partial information, but I then have no idea what the best way to formalize that is.

[Edward van de Meent]

this is likely somewhat besides the point, but this is one way to formalize the statement with current mathlib:

import Mathlib.Analysis.Normed.Lp.ProdLp

abbrev Coordinates : Type := WithLp 2 (Real × Real)

def wf_defined_sequence [Preorder α] (B : (α → β) → (α → β)) :=
  ∀ (f g : α → β), ∀ N, (∀ n < N, f n = g n) → ∀ n < N, B f n = B g n
-- when inputs are the same up to at least N, the output is consistent up to at least N.
-- i.e. `B` can't make decisions on future differences in strategy

def isTrackerFor (A : ℕ → Coordinates) (P : ℕ → Coordinates) := ∀ n, ‖A n - P n‖ ≤ 1

def isMoveSequence (S : ℕ → Coordinates) : Prop := ∀ n, ‖ S (n + 1) - S n‖ = 1

def final_moment : ℕ := 10 ^ 9

def Imo_2017_Problem_3 := ∃ (B : (ℕ → Coordinates) → (ℕ → Coordinates)), (wf_defined_sequence B ∧
  ∀ (A P : ℕ → Coordinates),
    isTrackerFor A P →
    isMoveSequence A →
    B P 0 = A 0 →
      ‖B P final_moment - A final_moment‖ ≤ 100 ∧ isMoveSequence (B P))

[Shreyas Srinivas]

Violeta Hernández said:

Question, is there any overarching definition for a game (of this strategic kind)? Or are there multiple overlapping notions?

This is one of those areas where a single overarching decision, if at all it exists, is likely to be obscure and require too much effort to prove theorems which are usually specific to the instantiations

[Shreyas Srinivas]

Normal form games can be represented as maps from finite types to costs, keeping with Lean's generality w.r.t matrices. Extended form games could be represented as an inductive type, which ought to make proofs by induction simpler

[Daniel Weber]

Here's a definition of a partially observable, multiagent, deterministic, sequential, static, and discrete environment, but I agree that it's quite unusable in practice (and it's not even fully general - it could be made nondeterministic and continuous)

import Mathlib.Tactic

structure GeneralGame where
  Agents : Type*
  State : Type*
  initialState : State
  Observesions : Agents → Type*
  observe : ∀ a : Agents, State → Observesions a
  Actions : ∀ a : Agents, Observesions a → Type*
  step : (current : State) → (∀ a : Agents, Actions a (observe a current)) → State
  reward : Agents → (ℕ → State) → ℝ

def GeneralGame.Strategy (g : GeneralGame) (a : g.Agents) : Type _ := ∀ x : g.Observesions a, g.Actions a x

def GeneralGame.run (g : GeneralGame) (s : ∀ a, g.Strategy a) : ℕ → g.State
| 0 => g.initialState
| n + 1 => g.step (run g s n) (fun a ↦ s a (g.observe a (run g s n)))

def GeneralGame.evaluate (g : GeneralGame) (s : ∀ a, g.Strategy a) (a : g.Agents) : ℝ :=
  g.reward a (g.run s)

-- Augment a game to give a memory to all agents
def GeneralGame.withMemory (g : GeneralGame) (mem : g.Agents → Type*) [∀ a, Inhabited (mem a)] : GeneralGame where
  Agents := g.Agents
  State := g.State × (∀ a, mem a)
  initialState := ⟨g.initialState, fun _ ↦ default⟩
  Observesions a := g.Observesions a × mem a
  observe a s := ⟨g.observe a s.1, s.2 a⟩
  Actions a o := g.Actions a o.1 × mem a
  step cur actions := ⟨g.step cur.1 (fun a ↦ (actions a).1), fun a ↦ (actions a).2⟩
  reward a game := g.reward a (fun n ↦ (game n).1)

[Shreyas Srinivas]

An agents reward can depend on the actions of all other agents apart from its observation of the extent state

[Shreyas Srinivas]

This definition doesn't capture that. In normal form games, even with iterations, all agents simultaneously observe the state and choose actions.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

In any case, as you pointed out, this is a case where abstraction is not helping reduce tedium. Just adding to it. A horizontal abstraction is better

[Daniel Weber]

Shreyas Srinivas said:

This definition doesn't capture that. In normal form games, even with iterations, all agents simultaneously observe the state and choose actions.

Sorry, I don't follow - could you give a concrete example?

[Shreyas Srinivas]

Sorry. Edited a message instead of adding one.

[Shreyas Srinivas]

Take iterated prisoners dilemma

[Shreyas Srinivas]

The state of the system is the set of actions that all agents have played up to an iteration

[Shreyas Srinivas]

In the next iteration, each agent can read this state, and has access to the cost function determined by the state and all possible actions by other agents

[Shreyas Srinivas]

The agent cannot know its final utility in the next iteration because it cannot know the actions of other agents in that iteration

[Shreyas Srinivas]

Anyway, my more important point is, if you try to fix this abstraction, it will get more complicated and still not capture all possible strategic interactions

[Daniel Weber]

Is this definition wrong?

def score : Fin 2 → (Bool × Bool) → ℝ
| 0, (false, false) => -1
| 1, (false, false) => -1
| 0, (true, true) => -2
| 1, (true, true) => -2
| 0, (false, true) => -3
| 1, (false, true) => 0
| 0, (true, false) => 0
| 1, (true, false) => -3

noncomputable def iteratedPrisonersDilemma : GeneralGame where
  Agents := Fin 2
  State := List (Bool × Bool)
  initialState := []
  Observesions _ := List (Bool × Bool)
  observe _ s := s
  Actions _ _ := Bool
  step cur actions := (actions 0, actions 1) :: cur
  reward a game := Filter.liminf (fun n : ℕ ↦ ((game n).map (score a)).sum / n) Filter.atTop

[Eric Wieser]

My initial take on that structure is that it probably is more convenient to unbundled all the type-valued fields

[Shreyas Srinivas]

My take is, that there is no per round reward and that the per round reward would also depend on the moves of other player in the current around which a player wouldn't know in advance

[Shreyas Srinivas]

And I will emphasize again that the TCS people's approach is going to prove more ergonomical in this area. Universal and all-encompassing abstractions are wonderful when they simplify and remove details that are not necessary. That is not happening here.

[Shreyas Srinivas]

The other problem is probably more human. let's say you find the perfect all encompassing and useful abstraction for games (big if). Now people contributing game theory have to learn this thing. They usually come from TCS backgrounds or economics backgrounds. You will now find yourself in the same position as some constructivists do when they say that you need to express complex numbers in a certain way (borrowing from Kevin's story iirc)

[Lars Ericson]

I noticed this repo: Formalizing Game Theory. It has 6 sorrys in it, so not 100% done yet. Where would it fit in mathlib? Top level GameTheory directory like FieldTheory or InformationTheory? I am curious what the taste guidelines and acceptance criteria are for putting significant branches of applied mathematics into mathlib. That is, what do the primary mathlib caretakers consider core mathematics areas that should go into mathlib and what areas are non-core and should stay in GitHubs. Game theory could be thought of as applied mathematics. Is applied math in or out of scope?

[Kim Morrison]

Applied maths that is done at appropriate levels of generality and that reuses existing foundational material where relevant is very welcome, and in scope.

That said, these criteria do seem to be harder to satisfy than in pure mathematics. In particular I think there's been a tendency for work in this direction to struggle to get agreement on definitions.

[Abraham Solomon]

(deleted)

[Lars Ericson]

There are many ways to organize facts into definitions in math. Clearly the proof of a fact has to be finished before the definitions that it relates to can go into mathlib. The game theory github has sorrys. In another thread, a hybrid logic github has sorrys. It is fun to find those cases where it turns out to be very hard to translate a paper proof into Lean, and then to understand why and get through it or discover a Lean limitation. Is it that the paper proof that is hand waving over some more complicated mechanics? Did the person coding the Lean proof take a wrong turn on an issue where there is a known path that the paper proof didn't spell out? Or is there something that can't be expressed in Lean?

[Shreyas Srinivas]

It is almost never a lean issue. It is almost always the case that the "proofs" in this area are heavily underspecified.

[Shreyas Srinivas]

Secondly sometimes generality is really not even mathematically sensible. I am currently formalising fair division theory in my spare time. In this domain, problems in the allocation of indivisible goods is inherently different than for divisible goods. Further, even in the indivisible world, chores (negatively valued goods) behave differently from goods.

[Alessandra Simmons]

Lars Ericson said:

I noticed this repo: Formalizing Game Theory. It has 6 sorrys in it, so not 100% done yet.

Oh, hey, this is my Game Theory repo. I would say my current definitions for games and strategies and properties of games are close to if not completely finished (in terms of the information they convey, not necessarily their exact Lean formatting). Almost all of the sorrys I currently have are in preparation to write proofs of existence for mixed Nash Equilibriums in matrix-like and continuous games, which are going to be quite complicated. I currently have a few example proofs of basic facts in game theory (for a specific prisoner's dilemma) that don't require sorrys, and I'm hoping to add example proofs of more general statements soon.

Most of my aim with this project was to create a definition of games that was general enough to encompass most (if not all) strategic game theory, but this is my first Lean project with such a large scope, so I'm very open to critique. From the work I've done so far, I would say it's definitely possible to formalize generalizations about games, but I'm not entirely sure about how much foundational material it would end up using. I know for sure that a fixed-point theorem is necessary for the proof of existence of mixed Nash Equilibriums in matrix-like games, and that it becomes even more complex for continuous games, but aside from that, I wouldn't be entirely sure about use of other formal mathematics.

[Shreyas Srinivas]

I just uploaded this today based off my mathlib PR for another reference :
https://github.com/Shreyas4991/FairDivision

[Malvin Gattinger]

Hi all! For my project on PDL I probably will need the result that in a finite two-player game with alternating moves and without draws one of the two players must have a winning strategy - Edit: apparently it is called "Zermelo's theorem".

I know little about combinatorial games, but at first sight it seems that I could specify the game using docs#SetTheory.PGame.State - is there any theorem that then gives me (existance of) a winning strategy? I could not even find a definition of strategies, so maybe I am missing something crucial about combinatorial games here ;-)

The game I have is finite, i.e. finitely branching AND even finite depth, so in particular it is "short" in the sense of Mathlib.SetTheory.Game.Short, in case that matters.

And on the other hand, the repository MixedMatched/formalizing-game-theory is only about one-shot / single-round games such as prisoners dilemma, but not iterated or multi-round games, correct?

[Shreyas Srinivas]

I think in general combinatorial games and strategic games are studying different concepts so I doubt that they'd mix well in a formalism.

[Alessandra Simmons]

Malvin Gattinger said:

And on the other hand, the repository MixedMatched/formalizing-game-theory is only about one-shot / single-round games such as prisoners dilemma, but not iterated or multi-round games, correct?

It is possible to have iterated strategic games using my representation, as long as the game is provably finite, although I'm not sure how easy it would be to prove the properties you want. I just pushed such an example for a 5-round iterated prisoner's dilemma at the bottom of Basic.lean, if you want a reference. I would, however, advise against using my project in its current state to do more complicated formalization tasks because I'm not really sure that it's ready for that. Obviously, you can use it at your own discretion.

[Antoine Chambert-Loir]

Just to say that @Anatole Dedecker and I have a formalization of von Neumann's theorem in the version of Sion involving quasiconvex/quasiconcave semicontinuous functions.

https://github.com/AntoineChambert-Loir/Sion4

[GasStationManager]

The existence of mixed Nash equilibrium in finite games absolutely belongs in mathlib once formalized. You'd need a fixed point theorem (Brouwer or Kakutani). If you have one of those in Mathlib then existence of Nash is quite doable (Nash 1950 via Kakutani, Nash1951 via Brouwer are both short proofs; or follow one of the textbooks). If you don't have a fixed point theorem then it can't be done (One can prove Brouwer from existence of Nash). In that case perhaps you could state Brouwer's fixed point theorem with sorry in place of proof, and go from there.

[Alexander Heckett]

Hey! I'd also really like some basic game theory results in Mathlib. Are we sure we need fixed point theorems? I recall being able to use strong duality / linear programming results instead, at least in some situations. If I'm insane and we do really need Brouwer / Kakutani, how hard would that be? I think we'd want some sphere homology results and I found some other conversations indicating that formalizing sphere homologies could take a while. Are there alternative proofs of Brouwer we could appeal to? I recall proving Brouwer in a course that didn't use algebraic topology but the proof did need mollification at one step. Sorry for sounding impatient -- all of my research is in game theory and I'm hesitant to formalize it until the foundational results are made canonical.

[Shreyas Srinivas]

As a rule of thumb we don't really need fixed point theorems in the level of generality that mathematicians prove them in. One can almost always work with elementary versions in euclidean space.

[Shreyas Srinivas]

Getting it into mathlib or even building off mathlib's constructions is a different story.

[Ma, Jia-Jun]

Shreyas Srinivas said:

As a rule of thumb we don't really need fixed point theorems in the level of generality that mathematicians prove them in. One can almost always work with elementary versions in euclidean space.

I am mentoring an ongoing student project (https://github.com/math-xmum/gametheory/blob/master/GameTheory/Scarf.lean) to prove Brouwer fixed point theorem following this paper:
https://arxiv.org/abs/1902.00827

If you are interested, you are welcome to join the project.