AIは未解決マシン52件を候補と特定

このpreprintは、問題解決と理論構築の境界に位置する。IMOメダルシステムやFermatの最終定理のLean 4形式化など、数学におけるこれまでのAIの成果は、人間がすでに提示し定義した問題から出発していた。ビジービーバーの設定はその足場を取り除く。マシンのテープには証明すべき明示的な命題がなく、論文の第1段階は生のテープを繰り返しブロックの指数に圧縮することで、LLMがそもそもパターンを探せるようにする。システムが見えるものを定義するのは、証明の段階ではなくこの圧縮の段階だ。

論文自身のAntihydraの式は、双方向のLeanループがなぜ重要かを示す。5ページと7ページの非形式的な規則はパラメータ値0を許すため、ステップ数が-1になるが、空のテープから始まる自然な軌道はその境界に決して到達しないため、誤りは隠れたままだった。定理文を変更できるProblem Setterを備えた4ペルソナの書き換えループは、まさにこの種のごまかしへの修正として提示されており、Stellar BB6 Protocolは5つの不正防止チェックで、システムが定理を自明なものに書き換えるのを防ぐ。

2つの限界が依然として見える。Stage 1のパイプラインが名指しするのは26台のうち8台のみで、残りはより圧縮された加速に報酬を与えられ、以前の証明済みコードを読める後期のGemini 3.8 Flashシステムによるもので、これは新たな発見ではなくテンプレートの転移を示唆する。また、Algorithm 1と2が繰り返しブロックというCollatz的な見方をハードコードしているため、パイプラインは1,163台の未解決マシンから52件の候補しか見つけられず、BB(3,3)からは皆無で、探索空間の大半は選んだレンズの届かないところに残った。