FRONT_END: A Sudoku-type game interface for building finite magmas obeying various laws

[teorth]

Discussed here. This interface would create a "game" where one has to fill out a multiplication table of a specified size. At any given stage of the game, the table will be partially filled out, and the status of various selected laws will be displayed: "false" (with some explicit values of variables supplied on request), "true" (which would only happen when the table is fully completed), or "undetermined" (where the table is incomplete, but no counterexamples found so far).

A more advanced feature would be to suggest "autocompletes" (in the spirit of "Minesweeper") based on the laws one wants to prove - possibly even incorporating automated theorem provers or SAT solvers natively.

[EricGT]

FYI

When searching the topic in the Zulip forum, search for the word sudoku instead of game.

The idea started here.

[teorth]

See discussion of a prototype at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/The.20Finite.20Magma.20Game