证明过程生成层次化的 HTML 文档

hbghlyj

幻灯片UCSC CSE Colloquium 2024/01/24 To formalized mathematics and back
YouTube视频
general>Finding a Lean to English analysis project
将已在 Lean 等系统中完成且经机器验证的形式化证明过程拆分为逻辑单元，提炼核心步骤，生成层次化的 HTML 文档。读者既可一览要点，也能通过“展开/折叠”功能查看各环节的详细证明。这种方式既保留了形式化证明的严谨性，又大大提升了可读性和可交互性。
示例：来自《数学分析原理》（Baby Rudin）
开集的补集
函数在稠密集的连续性
每个命题页面均以简明的定理陈述开头，读者可点击查看证明的各个层次细节。

GitHub仓库展示了页面生成器的结构与配置，但不包含全部自动化非正式化工具的实现细节。

hbghlyj

mathstodon.xyz/@tao/109870724335427662
Patrick Massot gave an impressive and highly entertaining demo of a (still in development) software tool to automatically convert a Lean proof into a web page providing an interactive human readable version of the proof.

能够自动将 Lean 证明转换为类似教材的可读文本，并在网页中以可展开的方式逐步呈现证明状态。
兼顾严谨与易读
打开页面后，你会看到证明过程中若干步骤的省略号表示。每个省略号对应证明中的一个“暂停点”，点击后显示该步骤的变量、待证明、假设。
基于一个plasTeX 插件leanblueprint
安装方式简单：

1. pip install leanblueprint

Copy the Code

即可获得命令行工具 leanblueprint，用来初始化和构建你的 Lean 项目的蓝图（blueprint），自动生成交互式网页和 PDF 文档。

多语言支持潜力
从插件架构来看 leanblueprint 本身并不强绑定任何自然语言，其核心是通过 LaTeX 宏将证明结构与 Lean 声明关联，再由 plasTeX 渲染到 HTML。因此，只要在 LaTeX 模板中替换英文字符串，就能生成中文版本的交互式网页通过这套基于 Lean 的自动化流水线，我们或许可以建立统一的数学形式化与自然语言表达桥梁，让严谨的形式化证明既对计算机“可执行”，又对人类“可阅读”，并能够轻松切换多种自然语言。

此外，Patrick Massot 的另一个项目 lean-verbose 曾提供受控自然语言的 Lean 扩展，最初版本为法语，后来也有英文支持，这进一步说明将 Lean 证明自动翻译到其他人类语言是可行的思路。未来完全可以实现从同一份 Lean 源码自动输出多种语言的严谨数学文本，从而打造一个“通用数学输入语言”。