Using A Theorem Prover

I reccomend the Lean4 Natural Number Game.

I was playing around with the Lean4 Natural Number Game. (Via this discussion.) I really like this way of doing mathematics. Maybe in the future, all upper-level math classes will use this software for homework. And all math papers too (Professor Tao is working on formalizing his papers in Lean4!)