Star Fleet Math es un sistema de inteligencia artificial creado por Colin Snyder con el asesoramiento de Mike Kim, inspirado en Ignis, que aborda algunos de los problemas abiertos más difíciles de la matemática empleando Lean 4. La aplicación de escritorio para macOS orquesta hasta 20 agentes autónomos en paralelo, bautizados como "starships", cada uno con su propia instancia de GPT-5.6 ejecutándose en un servidor dedicado de 60 vCPU y dedicado a un problema distinto. Todo el software está escrito desde cero en TypeScript y Bun.
Cada starship dispone de bursts de CPU x86-64 de hasta 2.000 vCPU para búsquedas masivamente paralelas, bursts de GPU H100, un corpus de premisas de Lean 4 (teoremas y lemas) consultable en lenguaje natural mediante embeddings de Gemini y una base vectorial Chroma, un índice de artículos de arXiv y repositorios de GitHub construido con Firecrawl, un verificador de pruebas basado en la API Claude Fable, un canal de iMessage para que el revisor humano valide los resultados y un sistema de memoria a largo plazo llamado Ton 618 que entrelaza las premisas verificadas en un grafo de dependencias. Además, cuenta con un sandbox de 60 vCPU y 120 GiB equipado con solvers SAT/SMT (CaDiCaL, kissat, Z3), CP-SAT de Google, sistemas de álgebra computacional (SageMath, PARI/GP, GAP, Macaulay2) y los toolchains completos de Rust, CUDA C++ y Lean 4.
El proyecto anuncia 27 soluciones propuestas, entre ellas la del Problema #123 de Erdős sobre sumas de monomios con la condición de que ninguno divida a otro, premio de 250 dólares en teoría de números. La demostración formal en Lean 4 articula una construcción en un nivel homogéneo, un sistema de códigos de aristas, progresiones aritméticas obtenidas vía van der Waerden y Hales–Jewett, y una innovadora "cáscara interior opcional" que preserva la primitividad de los sumandos. El texto se publica como reporte técnico de la estrategia matemática y de la arquitectura software que la hizo posible.