OpenAI Astra 一次发布十项数学与理论计算机科学进展，并为每项结果给出 Lean certificate

OpenAI 于 8 月 1 日发布内部版本 Astra 产生的十项研究结果，覆盖高维 sphere packing、binary/spherical codes、non-sofic groups、Connes rigidity、arithmetic circuit complexity、quantum parallel repetition、closest vector problem、Ehrhart volume conjecture、multicolor Ramsey numbers 与 extremal graph theory。OpenAI 表示数学论证由系统生成，人类负责整理 manuscript 与正确性责任，随后模型为每项结果生成 Lean certificate；官方估算寻找这些解答所需 tokens 若按 Sol API 计费约为 2,000 美元。