Colin SnyderのStar Fleet、20体のGPT-5.6エージェント並列稼働でオープン エルデシュ問題に挑戦
独立系研究者Colin Snyderによる「Star Fleet」は、最大20体の「starship」エージェントを並列でオーケストレーションする。各エージェントは、SAT/SMTソルバーとLean 4の前提検索を備えた専用の60 vCPUサーバ上で稼働するGPT-5.6インスタンスであり、13件のエルデシュ問題に対してカーネルチェック済みのLean 4証明を投稿している。これは査読を経ていない自主公開の取り組みであり、提案された解のうち少なくとも2件はすでに撤回されている。ここで注目すべきは個別の解ではなく、この基盤である。形式的検証と並列エージェントのオーケストレーションを組み合わせたアプローチは、証明スペースを大規模に探索する有望な手法として浮上しつつある。
出典： starfleetmath.com ↗
Star Fleetは、Lean 4を使って世界で最も困難な未解決の数学問題を解くAIシステムだ。
コリン・スナイダー、Star Fleet Math
なぜ重要か
- → Formal verificationをparallel agent orchestrationと組み合わせることで、困難な未解決問題への証明探索を大規模化する。
- → AIシステムがpeer review gatekeepingなしにErdős-class mathematicsに取り組む実現可能性を示す。
- → Lean 4 kernel validationは、正しさの裁定者として従来の出版に取って代わる。
Parallel agents、Lean proofs