Lean 4运行#check Proof报unknown identifier错误如何解决？

Proof并非Lean4标准库的内置标识符，是《定理证明在Lean4》教程讲解「命题即类型」概念时，为了降低理解门槛引入的演示用虚拟类型，默认开发环境不存在该定义，因此直接运行教程中的#check Proof会触发未知标识符报错。

对应的解决方法如下：

• 若仅需要复现教程中的演示效果，在执行#check命令前先手动定义Proof类型即可：

def Proof (p : Prop) : Type := p
#check Proof   -- Proof : Prop → Type

该定义和教程描述完全匹配，运行后输出结果和文档展示一致。

对于每个元素p : Prop，我们可以引入另一个类型Proof p，表示p的证明的类型

• 实际编写Lean4代码时不需要单独定义和使用Proof类型：教程引入这个包装类型只是入门阶段的教学手段，Lean原生逻辑中命题本身就是其对应证明的类型，熟悉概念后直接写h : p即可表示h是命题p的证明，不需要额外加Proof包装。

内容的提问来源于stack exchange，提问作者Bobjoesmith