Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
Summary
The article reports on Star Fleet Math, an AI-driven system that solves open Erdős problems in parallel using 20 GPT-5.6 assistants and Lean 4 with Mathlib. It describes the tech stack (TypeScript, Bun) and the verification workflow, including downloads and Claude/Codex integrations. It also discusses implications for AI-assisted mathematical research and machine-checked proofs.