OpenAI math 开放固定Lean工具链与形式化验证资源

OpenAI首次公开math仓库的README列出722篇手稿、372个问题族，并提供部分形式化验证与推理材料。此条收录可独立使用的Lean库和Comparator挑战入口，而不是重复10.6的数学研究流程披露。目标版本固定Lean 4.34.1，依赖及兼容补丁由lakefile记录，可从lean目录取得依赖缓存并运行指定Comparator挑战。根目录和Lean库采用Apache-2.0，外部依赖及引用论文保留自身许可。大型库建议分部分编译，环境还可能需要调整Lean构建内存映射选项。形式化资源不是通用数学证明模型，也不能推定所有手稿或自然语言结论都已正确形式化；本次核对代码及流程，未编译整个库。