一键打开：https://gitpod.io/new/#https://github.com/chenjulang/RuntimeFormalization4
遇到错误的解决方案： 1.错误描述：unknown identifier 'git' 解决方案：curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain lake -Kenv=dev update