Game Theory lemmas

Wojciech Karpiel be9be5346c co ja robię ze swoim życiem 11 mēneši atpakaļ
Wygryw be9be5346c co ja robię ze swoim życiem 11 mēneši atpakaļ
.gitignore 09a7dae522 init 11 mēneši atpakaļ
README.md d709b8904c CZYTAJMNIE 11 mēneši atpakaļ
Wygryw.lean 09a7dae522 init 11 mēneši atpakaļ
lake-manifest.json 6d8685edcc nie mam pojęcia co to ale jest w vc 11 mēneši atpakaļ
lakefile.lean 09a7dae522 init 11 mēneši atpakaļ
lean-toolchain 09a7dae522 init 11 mēneši atpakaļ

README.md

Wygryw

Learning Lean by formalizing simple game theory lemmas. Nothing serious, just learning Lean

Lemmas so far:

  • Every deterministic game without draws has winning strategy for one of the players[1]

[1] The starting point for the proof is assuption that all possible gameplays of a deterministic game can be represented by a finite tree, which I have yet to formalise