I created a puzzle game that literally mirrors the natural deduction of intuitionistic propositional logic, but you don't need to be a logician to play it, nor do you need to know formal logic.
https://zenrosadira.itch.io/modus-ponens
The goal of the game is to figure out which shapes can be "lit up" and find a way to do so, which is secretly just the representation of a theorem proof: the shapes are propositions, their contours are connectives, and the light represents truth.
With every solved puzzle, you earn a score and receive the proven logical formula as a badge.
