MangLean

The game is a five nights at Freddy's fangame in which the player is required to quickly write Lean4 formalized theorem proofs with Mathlib. Both lean and mathlib should already ship with the files, so you shouldn't have to download them separately. The AI difficulty for Mangle also corresponds to harder lean4 proofs.