Wojciech Karpiel be9be5346c co ja robię ze swoim życiem | 11 ماه پیش | |
---|---|---|
Wygryw | 11 ماه پیش | |
.gitignore | 11 ماه پیش | |
README.md | 11 ماه پیش | |
Wygryw.lean | 11 ماه پیش | |
lake-manifest.json | 11 ماه پیش | |
lakefile.lean | 11 ماه پیش | |
lean-toolchain | 11 ماه پیش |
Learning Lean by formalizing simple game theory lemmas. Nothing serious, just learning Lean
Lemmas so far:
[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