Binary Linear Constraint System Games in Lean

This project provides a Lean framework for reasoning about Binary Linear Constraint System games. It enables the formalization of the games themselves, of strategies in both the projector and observable formalisms, and of associated constructions such as winning and losing operators and the solution group.

Building on this framework, the project formalizes results concerning perfect strategies, including the sum-of-squares decomposition of the losing operator and the connection with representations of the solution group. The magic square game is developed as a central example.

Visit the project webpage at sean.perazzolo.ch/lcs for the source and the report.