将 LaTeX 宏（\lean, \leanok, \uses）与 Lean 声明关联，再由 plaTeX 渲染到 HTML

hbghlyj

演示地址：imo.universite-paris-saclay.fr
能够自动将 Lean 证明转换为类似教材的可读文本，并在网页中以可展开的方式逐步呈现证明状态。
视频录像2023年已上传至 YouTube 供感兴趣的人观看

兼顾严谨与易读
打开页面后，你会看到证明过程中若干步骤的省略号表示。每个省略号对应证明中的一个“暂停点”，点击后显示该步骤的变量、待证明、假设。
整个源代码开源托管于 GitHub，基于一个名为 leanblueprint 的 plasTeX 插件
安装方式简单：

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 源码自动输出多种语言的严谨数学文本，从而打造一个“通用数学输入语言”。