Comment by silentOpen

In Euclidea, you don’t manipulate the proofs but unless you’re just brute-forcing the levels you have constructed a proof mentally. Similarly, if Euclidea is implemented correctly, it generates the proof internally and checks it (even if these stages are fused). I wouldn’t rely on a game for building large developments and indeed Euclidea lacks abstraction and modularity as far as I can tell but the same developer may have a freeform environment with these features. Euclidea is an activity that mentally scratches the same itch as proving and in the same or very similar theory to TFA.