@dove 另外，在形式化证明中通常使用的定义自然数的方式是递归定义而不是使用带有大小限制的原始数据类型（比如unsigned long long），这点我在博客中也提到了。