Description
如果对Lean Prover没有了解的话，对这期内容感到疑惑是正常的。我前面做过两期视频，但我不觉得我能很快讲明白Lean的机制。
自然数游戏 : https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
学习使用Lean : https://leanprover-community.github.io/learn.html
下面是我尝试用简短的篇幅介绍这个游戏的理念，要求理解“类”和“实例”的概念。
我的理解可能有偏差，请多多指教！
用一句话介绍：命题同时是类、集合和Prop类（集合）的实例（元素），而拥有一个命题的实例（元素）可以视为认为这个命题是真命题。
难以理解的点在于看到命题、类、集合、实例与元素的共通之处。
举个例子：具有“如果（命题A）那么（命题B）”形式的命题可以被视为A→B的函数（视为类），这样如果我们有此命题的实例（即拥有了一个A→B的函数的实例，记为f），同时拥有命题A的实例a，那么f(a)就是命题B的实例。这和由A→B为真、A为真推出B为真的推理过程是对应的。
补充：将empty视为集合，拥有一个empty的元素表示存在悖论，对于false也一样。例如对A≠B的定义是A=B→false，即如果A=B，那么存在悖论。事实上，如果我们同时认为A≠B和A=B，则确实存在悖论。我们认为false的实例可以推出任何命题的实例，其实是因为要证任何命题的时候只要获得了false的实例就进入悖论了，进而解决目前的目标。
