**OpenAI 数学证明被指依赖未公开的专有公理，呼吁开源基础定义**

_Open AI Math Proofs modified sandbox_

> 近期研究发现，OpenAI 使用 Lean 4 编译器生成的数学证明存在严重问题：其构建过程依赖未公开的专有基础命名空间。由于底层公理和拓扑定义被隐藏，科学界无法独立验证这些证明是否真正解决了物理边界问题，还是仅仅进行了数学上的重新定义。该研究呼吁公开这些基础定义，以保障自动化形式化验证的完整性与可信度。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：论文
- **发布时间**：2026-10-29 06:26（北京时间）
- **原文**：[打开原文](https://zenodo.org/records/23717719)