Formalising Binary Linear Constraint System Games in Lean

This project provides a Lean framework for reasoning about Binary Linear Constraint System games. It enables the formalisation 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 formalises 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.

Use the links below to read the report, browse the generated documentation, or inspect the project source.