Prove You Can Win

I tried this as an introduction to interactive theorem proving. This game formalizes a maze game, but instead of finding a path, you prove that a path exists using a small set of axioms. The biggest downside is the UI/UX: compared to actual interactive theorem provers, it feels noticeably less smooth and less capable. Also, many interactive theorem provers are free, and there are plenty of free beginner-friendly materials for Lean 4 and Coq that can be just as fun (and more flexible). If you've never touched this kind of thing, the game does provide a very basic "onboarding" experience, so I can see some value there. If you're comfortable setting up tools, I'd recommend trying Lean 4 (Theorem Proving In Lean, Mathematics In Lean) / Coq (Software Foundations series) tutorials instead.

I bought it [i]because[/i] of a negative review saying "you may use more meaningful names to introduce arguments in a function". That basically told me that this game was created by a mathematician. Even though English is a little bit clumsy and it's hard to get into first, once you get the hang of it, it becomes a fun logic puzzle game. It's impressive how pathfinding turned into a set of axiom schemes. This would have been much greater if it was possible to enter proofs via interactive graphic system, though. For example, I would like to apply rule 1.2 via "drag one path to another to remove it", and rule 1.3 via clicking on a path. Enabling this would have made this game much more accessible.

This game was nice (even though it was a bit inconvinient) until Chapter 1-4, and when I saw last proposition in Chapter 5, I was really hype about it. But sadly, it's proof was really disappointing for me. It would be really wonderful if definitions and structures this game had constructed in previous chapter collapsed by itself, but definitely it was not the case. I feel like this proposition is a joke and the game betrayed my expectations.

The idea of this game is very interesting, and it is evident that the developer has put in much effort into the game. However, the tutorial is just too bad. It is not the coding element which deters me from playing, but the quality of the tutorial. The arguments in the code are arbitrary and hard to follow. Since this is tutorial, by all means you may use more meaningful names to introduce arguments in a function. For instance, instead of rule2.1(n,k,m,p,q,r), by all means you can write rule2.1(step, target_vertex, key_number, path_to_get_the_key_number, path_to_modified, lock_position). It is extremely annoying to see (n, k, m, p, q, r) every time. Furthermore, based on the renamed arguments above, the sequence of arguments seems also quite arbitrary and not logical.