文章摘要
Star Fleet是一个AI系统，通过Lean 4解决世界最难的数学问题。它是一款Mac桌面应用，可并行控制20个名为“starships”的智能代理，每个代理运行独立的GPT-5.6实例，配备专用服务器和多种计算资源，包括CPU、GPU、大型语料库及验证系统。
文章总结
好的，这是根据您的要求，对原文主要内容进行的中文重述，保留了核心细节，并删减了与主题无关的列表内容。
文章核心内容重述
“星际舰队数学”（Star Fleet Math）是一个旨在解决世界上最难的开放数学问题的人工智能系统。该系统由Colin Snyder构建，使用Lean 4形式化证明语言，并以Mac桌面应用程序的形式运行。
其核心机制是并行控制多达20个名为“星舰”的定制化AI代理。每个“星舰”都运行着独立的GPT-5.6实例，并配备有专用的60 vCPU服务器，各自负责解决一个不同的数学问题。整个系统使用TypeScript和Bun从零构建。
每个“星舰”都拥有强大的资源，包括： - 计算能力：可突发使用高达2000个vCPU进行搜索，并能将任务分片为数千个独立的单核作业；同时支持H100 GPU集群，用于大规模并行搜索。 - 知识库：拥有据称是全球最大的Lean 4定理与引理语料库，可通过自然语言进行搜索；并索引了arXiv.org的研究论文和GitHub代码库。 - 验证与反馈：集成了Claude Fable API作为证明验证代理，用于审查提交的答案。在Fable批准后，还可通过iMessage API请求人类专家Colin进行额外审查。 - 长期记忆系统：名为“Ton 618”的本地长期记忆系统，将所有已验证的Lean 4前提编织成一个依赖关系图，使得证明过程可以不断累积和复用。 - 开发环境：每个“星舰”都配备了一个专用的60 vCPU、120 GiB内存的沙盒环境，预装了多种SAT/SMT求解器、计算机代数系统以及完整的Rust、CUDA C++和Lean 4工具链。
该系统目前已经提出了27个问题的解决方案，主要针对Erdős问题（共650个），同时也涉及前沿数学问题（630个）和千禧年难题（14个）。项目团队强调，他们已尽力避免研究那些在网上已有非正式或部分答案的开放问题。
评论总结
根据评论内容，总结如下：
主要观点与论据：
技术实现与资源投入：评论关注项目使用的计算资源（如“thousands of vCPUs”）、搜索框架（“search harness”）以及Lean 4定理证明的语料来源。部分评论质疑代码是否开源（“Is the code backing Ton 618 open source?”），并指出计算成本巨大（“that’s a huge amount of compute”）。
证明质量与可读性：有评论认为生成的证明（由Fable审核）可读性差，充满技术术语和模糊引用（“real difficulty with the theory of mind of the reader”），但承认Lean 4证明本身是“compelling output artifact”。同时指出，将证明转化为人类可读形式仍需额外努力。
数学价值与影响：部分评论认为AI证明可能“sucking the fun out of math”，威胁数学家工作；另一些则强调其潜在价值，如发现新技巧或概念（“spur new techniques and concepts”），并期待“distillation/explanation into something humans and computers can grok together”。
个人实践与开源需求：有评论者分享类似尝试（如使用ChatGPT 5.5/5.6解决Erdos问题），并提及开源项目（如“github.com/aconsapart/thesisus”）。多人呼吁开源代码以降低计算门槛（“Are there any plans to open source this?”）。
模型与运行方式疑问：评论质疑GPT-5.6作为闭源模型如何用于个人项目（“GPT-5.6 is a closed source model”），并询问如何在自己的硬件上运行GPT（“How does one...do that?”）。
平衡性总结： - 支持方：认为AI证明是“fun experiment”，能推动数学进步，并分享个人成功经验。 - 质疑方：关注可读性、计算成本、开源问题，以及可能对数学人文价值的冲击。
关键引用（保留中英文）： - “What kind of harness does the exploration? Where did the corpus of Lean proofs come from?”（技术实现疑问） - “the proof summaries (from Fable) read like Claude tends to read to me these days - real difficulty with the theory of mind of the reader”（可读性批评） - “Isn't this sucking the fun out of math? ... why not let mathematicians keep their jobs?”（人文价值担忧） - “I only have one novel proof (non-Erdos) and 13 first-time formalizations thus far.”（个人实践成果） - “GPT-5.6 is a closed source model and this seems to be a personal project”（模型来源质疑）