given that I dug up some old game theory results, I was thinking of writing an ongoing thread in the Coq Discourse about "current status of game theory in Coq". For example, there is https://arxiv.org/abs/0705.3316 by Le Roux from 2007 which has no links to code. @Erik Martin-Dorel do you know if this code/paper is superceded by https://arxiv.org/abs/1709.02096 (GandALF 2017 paper)?

Hi @Karl Palmskog good question, actually the answer is no: both papers deal with Nash equilibria (probably the most typical solution concept in game theory) but the GandALF 2017 paper https://arxiv.org/abs/1709.02096 is actually a follow-up (and a dual formalization (in Coq+Isabelle) of part) of the following article: http://dx.doi.org/10.1002/malq.201300034

BTW we are precisely working on an extension of the GandALF 2017 paper which could lead to a new release of our Coq and Isabelle formalizations ;)

(currently, the GandALF 2017 code was only available on my IRIT webpage: https://www.irit.fr/~Erik.Martin-Dorel/winning2ne/)

@Erik Martin-Dorel thanks, and how large is the gap to the work by Stewart et al. (e.g., https://jfr.unibo.it/article/view/7235 and https://github.com/gstew5/games), do you use similar definitions? It seems you and them are both using MathComp, at least.

@Karl Palmskog good question again :) so Stewart et al.'s library is available at https://github.com/gstew5/games as well as in opam, both libraries use MathComp but the two main differences lie in the choice for modelling the games themselves, and the overall aim:

- Definitions:
* The

`games`

library use less dependent types (in particular, the definition of a game assume the "actions" (aka "strategies") for all players are taken in the same codomain`T`

, albeit some actions are not admissible… which is modelled by means of a relation`move`

that describes admissible moves between strategies) and uses`realFieldType`

-valued outcomes (aka "costs");* while in the

`winning2ne`

library we focused on providing first the most generic definitions (with arbitrary outcomes and dependently-typed strategies (which as always, can introduce some "dependently-typed technicalities")):

```
Variables (Agt : Type) (Strat : Agt→Type) (Outc : Type).
Definition strategy := ∀a : Agt, Strat a.
[…]
```

- Focus:
* In

`winning2ne`

we specifically worked on formalizing [LeRoux 2014], instantiating the general definitions above with 2-player multi-outcome games, to formalize LeRoux's`Nash equilibria transfer theorem`

, after introducing e.g. the notion of**determinacy**.* While

`games`

rather aims at being a general-purpose library AFAICT, providing a nice, comprehensive library of many results in game theory.

BTW I have precisely started developing a small theory attempting to "bridge the gap" between the two games definitions, e.g. to be able later on, to port one theorem already available in one library to the other; assuming obviously that the result can be expressed in both contexts! (but this development is still work-in-progress)

@Erik Martin-Dorel very nice comparison, do you mind if I sum this up in a Discourse post and lift some stuff verbatim?

no worries, please do! :)

BTW, are you specifically interested in game theory in general, or maybe in specific results?

I was interested in what has been done so far, not really any specific results. Mainly due to my ongoing work on blockchains

it looks like auction theory is not covered so well at present, this is a bit unfortunate since I think this is where Coq constructivity actually makes a lot of sense (verified algorithms). I'm sure somebody somewhere is already doing work in this direction though.

yes indeed

unfortunately `games`

doesn't work with Coq 8.12 / MC 1.11, e.g., fails on 8.11+MC-1.11.

yesterday, I managed to track down (and port to recent Coq) 3 out of 4 old game theory Coq developments. Those 4 together with `winning2ne`

and `games`

seem to be everything there is on Coq. Beyond Coq, there is also the work by Parsert and Kaliszyk in Isabelle. Waiting for some info on the missing 4th, then I will probably put everything on GitHub.

ah, got them all now working on at least 8.10 to 8.12:

- https://github.com/palmskog/InfiniteExtensiveGames
- https://github.com/palmskog/SequentialNashEquilibria
- https://github.com/palmskog/DependentTypesForExtensiveGames

Now just to add some metadata/CI, probably over the weekend

Last updated: Jun 18 2024 at 08:01 UTC