If your game is big, then your proof will need to be huge. It works basically the same as Lean.