未来工作与待解决问题

文件格式

当前存在一个关于将导出文件格式迁移到 JSON 的开放 RFC 讨论，见 这里，这将是一项重大版本变更。

确保 Nat 和 String 的正确定义

Lean 社区尚未达成共识，关于如何判断导出文件中 Nat、String 及相关内核扩展所覆盖操作的声明，是否符合扩展所预期的要求，且不将导出器纳入可信代码范围。

类似于对 Eq 和 Quot 声明采取的方案——在类型检查器中手工定义并断言其一致性——因 Nat 上支持的二元操作的完全展开项复杂度过高而不可行。

改进 Pollack 一致性

Lean 4 提供了强大的自定义语法、宏和美化打印器行为的机制，且几乎所有内部实现都可由用户访问。这些设计是基于 Lean 3 期间 mathlib 社区反馈的有效回应。

虽然这些特性极大推动了 Lean 作为大型形式化工具的成功，但它们也与 Lean 4 的 Pollack 一致性（或称 Pollack 不一致性）存在冲突¹。如果不在美化打印器中复现宏和语法扩展的功能，类型检查器就无法以用户可识别的形式一致地回显表达式。将这些功能纳入美化打印器意味着扩大可信代码基，难以接受。另一种方案是放弃美化打印器，转而使用可信解析器（如 metamath zero），但 Lean 的解析器可在用户空间通过自定义语法声明动态修改。

随着 Lean 的成熟和采用度提升，未来很可能推动开发允许用户利用 Lean 可扩展性的技术和实践，同时尽可能减少对 Pollack 一致性的牺牲。

前向推理（Forward reasoning）

现有类型检查器主要实现了反向推理。另一种类型检查策略是接受并检查由外部程序计算出的前向推理链，这可能允许设计更为简洁的类型检查器。