- Sources: Star Fleet Math, HN 48914646
- Summary: A site published by Colin Snyder presents proposed solutions to a set of open Erdős problems produced by "Star Fleet," a harness that runs up to 20 parallel Codex (GPT-5.6) instances emitting Lean 4 proofs. Each entry ships complete Lean 4 source pinned to a Mathlib version, automated checkers that reject
sorry placeholders, and a transitive axiom audit, with downloadable packages for independent verification. The results are framed as proposed solutions and are not peer reviewed, and one entry states an independent referee reran the verification. - Why it matters: Machine-checked Lean output is a stronger claim than a prose proof, so it is a concrete test of whether parallel LLM agents can produce verifiable mathematics, and it extends the GPT-5.6 Sol proof thread from earlier this month.
send feedback on this story