研究论文形式化

从研究论文到可独立核查的 Lean 工程：通过 Quokka 完成相关形式化操作，在 ReasLab 中验证形式化证明，并根据定理依赖图深入了解定理之间的依赖关系。

演示视频

核心能力

• 在论文原始上下文中阅读定理，并定位对应的形式化陈述。
• 通过 Quokka 完成相关形式化操作并生成 Lean 工程。
• 在 ReasLab 中检查并验证形式化证明，查看实时编译反馈与 Infoview 结果。
• 通过编辑器导航回溯导入定义与中间引理。
• 确认形式化证明通过 Lean 内核检查并完整闭合。
• 根据定理依赖图，进一步理解不同定理之间的依赖关系。

开始使用

• Lean 形式化指南 · Lean 工具链