LCS in Lean4

 Formalisation of Linear Constraints Systems games in Lean4🔗

Sean Perazzolo, Spring 2026

This manual acts as a research companion to the Lean 4 formalisation of Linear Constraint System (LCS) games. Its purpose is to explain the mathematical objects formalised in the library. Exhaustive declarations and theorem statements are left to the generated API documentation.

Main Verified Results

  • The Mermin-Peres Magic Square observables are formalised and assembled into a valid strategy in the library. See the Magic Square API page.

  • The local winning and local loss operators are formalised for a general LCS game, together with the sum-of-squares decomposition theorem for the local loss operator. See the Winning condition API page.

  • The bridge from observable strategies to projector strategies is implemented explicitly, so the two strategy formalisms can be compared inside one framework. See the Strategy equivalence API page.

Reference Links

  • A snapshot of the project's current written status is available in the status report PDF.

  • The generated API documentation for the Lean library is available in the API docs.

Contents

  1. 1. About This Project
  2. 2. Introduction to Linear Constraint System Games
  3. 3. Formalising Linear Constraint System Games
  4. 4. Strategy Formalisms and Equivalence