# Star Fleet：用20个并行GPT-5.6智能体解决埃尔德什难题

- 来源：Hacker News 热门（buzzing.cc 中文翻译）
- 作者：colin7snyder
- 发布时间：2026-07-15 14:15
- AIHOT 分数：36
- AIHOT 链接：https://aihot.virxact.com/items/cmrlpa4rs00eybih5qt1ohw0o
- 原文链接：https://www.starfleetmath.com/

## AI 摘要

Star Fleet 是一个基于 Lean 4 的 AI 系统，通过 Mac 桌面应用并行控制 20 个独立 GPT-5.6 实例，每个实例配备 60 vCPU 服务器，分别处理一个数学问题。系统集成了 H100 GPU 集群、Lean 4 语料库及 CaDiCaL、Z3 等求解器，目前已提出 27 个解决方案。

## 正文

Star Fleet is an AI system that solves the world's hardest open mathematics problems using Lean 4. It's a Mac desktop app that controls up to 20 custom agentic harnesses called “starships” in parallel, each running its own GPT-5.6 instance on a dedicated 60-vCPU server and working on a separate math problem. Everything is built from scratch in TypeScript & Bun.

Each starship has access to:

x86-64 CPU bursts of up to 2,000 vCPUs for search programs that shard into thousands of independent single-core jobs

H100 GPU bursts for massively parallel search programs

The world's largest corpus, afaik, of Lean 4 premises (theorems & lemmas), searchable in plain English via gemini-embeddings-2 & chroma vector db

A Firecrawl.dev index of arXiv.org research papers & GitHub repos

Claude Fable API wrapped in a proof-verifier agentic harness to review submitted answers + an iMessage API to ask Colin (the human) for an additional review after Fable's approval

Ton 618, a local long-term memory system where every verified Lean 4 premise (theorem or lemma) is woven into a dependency graph, so proofs compound

A dedicated 60-vCPU, 120 GiB memory sandbox preinstalled with SAT/SMT solvers (CaDiCaL, kissat, Z3), Google's CP-SAT, computer algebra systems (SageMath, PARI/GP, GAP, Macaulay2), and the full Rust, CUDA C++, and Lean 4 toolchains

Proposed Solutions (19)

Many problems listed as “open” carry informal or partial answers already available online; we tried extremely hard to avoid working on any such problems (but most likely failed in certain cases). If there are attribution mistakes, please let us know.