林一二2023年07月02日 01:02
小时候证明东西都是写「状态」，把长长的包含一堆字母的式子一行行往下抄，每一行也就删减增加几个字符，写得很累。如果还想写下证明用到的定理，则需要写更多文字了，例如用到定理xxx。
今天玩Lean的证明，则只需要写下操作，而且操作还很短，例如 rw add_zero 即可，而且还是打字写的，让手指一点也不费力。
中间长长的状态，则直接显示在屏幕上，由 Lean 来输出，一点也不费手指了，也避免了慢悠悠地写字占用大量的时间，导致数学作业写不完。（很像加了 log 语句之后变卡了的程序的感觉）