关于 Lean 4 数学证明生成中的公理黑箱问题

对公开 Lean 4 数学证明编排的审计显示，其依赖专有且未公开的基础命名空间，导致学界无法独立验证证明的完整性。 底层公理与拓扑定义处于混淆状态，阻碍了对生成证明是否解决物理边界问题的独立审查。 文章呼吁公开发布这些基础定义，以确保自动化形式化验证的完整性。