Sudoku formalization in lean Inspired by a Coq implementation Build with nix build . Run tests with nix run .#test