Earthbound OST with theorem proving in Lean 4 is surprisingly fitting. I think Mr. Saturn would like this language