実験記録・未レビュー
予算$1,000でteai/maxに
「人類の未解決問題」を解かせてみた。
「最近解かれた問題以外の未解決問題を解かせてみて、予算は$1,000」というリクエストから始まった実験。リーマン予想やP対NPのようなミレニアム懸賞問題は、LLMがそれらしい証明もどきを書いても専門家レビューで確実に崩れるため最初から除外し、OEIS(整数列データベース)に眠る小さいが正真正銘の未証明予想45件に絞って挑ませた。結果は1件について、専門家レビュー待ちの証明候補を得た(自分たちで実データと突き合わせる検算はしたが、第三者の査読はまだ)。総コストは予算の2%未満。誤判定を自分で発見して直した過程も含めて全部公開する。
この記事のステータス(2026-08-17時点) 以下で紹介する証明候補はOEISの編集者にまだ査読されていません(アカウント登録・投稿準備は完了、掲載審査待ち)。また調査の過程で、この事実と数学的に同値な主張が2018年に著者自身によって別の言い回しで(証明なしに)既に使われていたことも判明した。「世界初の発見」ではなく「未証明のまま残っていた一文を、初めて第一原理から埋めた候補」という位置づけとして読んでほしい。
結論から3行: ①ミレニアム懸賞問題級は除外、OEISの小さな未証明予想に絞るのが現実的な戦場だった。②45件中1件(A196020)について、実データとの突き合わせ検算は完了・OEIS編集者の査読は未完了という証明候補を得た。③自動判定パイプラインに2回バグを発見(うち1回は「証明放棄」を「証明成功」と誤判定する重大なもの)。自分で見つけて直した。
なぜミレニアム懸賞問題を除外したか
最初にteai/max自身にブレインストーミングさせたところ、リーマン予想・P対NP・ナビエストークス方程式などが並んだ。これらは実際には手が届かない。LLMは自信満々にそれらしい証明を書くが、専門家レビューで論理の飛躍が見つかって崩れる、というのが定番の失敗パターンだからだ。調査の結果、この種の取り組み自体は既にOpenAIがGPT-5で系統的に実施済みで(arXiv:2511.16072)、Erdős問題の一部も解決済みだと分かった。同じ土俵で戦っても勝ち目は薄い。
選んだ戦場 OEIS(30万件超の数列データベース)には、投稿者が経験的に見つけたが証明していない小さな「Conjecture:」コメントが大量にある。数論・組合せ論の初等的な主張が多く、LLM+数値検証で現実的に前進できる規模。
方法: 数値検証→証明→敵対的査読→改訂(最大3周)
OEIS検索APIで候補を収集(159件)→有名未解決問題や自己言及的な数列を除外(45件)→各問題について以下のパイプラインを回した:
1. teai/maxが証明を試みる(捏造禁止・証明できなければ正直に「できなかった」と書く指示)
2. 別呼び出しのteai/maxが敵対的に査読(論理の飛躍・誤りを探す)
3. 査読が「証明として成立していない」と判定したら、批評を渡して改訂させる(最大3周)
4. 3周してもダメなら「未解決のまま」として記録
実測結果(45問完走)
| 判定 | 件数 |
|---|
| VALID_CANDIDATE(自動査読が「証明として成立」と判定) | 2 |
| FLAWED(誠実に「証明できなかった」) | 43 |
総コスト(数値検証・ブレインストーミング・全試行込み): 約$25。予算$1,000の2.5%。VALID_CANDIDATE=自動査読の判定であり、専門家レビューの合格を意味しない(下記参照)。
証明候補: A196020(2018年から"Conjecture:"のまま)
OEIS A196020は「T(n,k)は、n以下の正整数をちょうどk個の連続正整数の和として表す方法の総数f(n,k)を使うと、T(n,k) = f(n,k)² − f(n−1,k)² と書ける」という2018年2月にOmar E. Pol氏が投稿した予想。この記事執筆時点でも、A196020のページ上ではこのコメントは"Conjecture:"のまま、証明の追記は一切ない。teai/maxが以下の初等的な証明を組み立てた:
f(n,k)の明示式(floor関数)を導出
→ 差分の二乗 f(n,k)² - f(n-1,k)² を「隣接階段の差」として場合分け
→ n が階段の変化点でなければ差分0(=T(n,k)=0と一致)
→ n が変化点なら差分が (j+1)² - j² = 2j+1(=T(n,k)の値と一致)
→ 証明終わり
この証明の帰結を、OEISページに掲載されている実際の生データ(24行)と直接突き合わせて検算し、全て一致することを確認した(自分で書いた検証コードに対してではなく、公開されている実データそのものに対して)。数値検証としてはこれ以上ないくらい直接的だが、これはあくまで自分たちによる検算であり、第三者の数学者によるレビューではない。
調べて分かった複雑な経緯 A196020と関連の深い別の数列A237048のページには、著者Omar Pol氏自身が2018年10月10日付で、数学的に同値な式(A237048の部分和の二乗の差)をシグマ関数の公式の中で証明なしに使っている記述があった。つまり著者は同じ事実を4ヶ月後には別ルート(A236104経由)で確信していた可能性が高いが、A196020の元のコメントを"Conjecture:"から"証明済み"に更新することは(2026年8月時点で)一度もしていない。teai/maxの証明が新しいのは「n以下の整数を連続k整数の和で表す方法の数」という第一原理の組合せ論的定義から直接導いた点であり、「世界初の未知の発見」ではなく「著者が別ルートで確信していたが正式に埋めていなかった一文を、初めて第一原理から埋めた」というのが正確な位置づけだ。
OEISへの掲載を申請中(アカウント登録・メール確認は完了、編集者によるレビュー待ち。承認されるかどうか、この記事の時点では確定していない)。
2分で分かる動画版(音声解説つき)
上のA196020証明候補の要点を、音声(KOEナレーション)とスライドで2分ちょっとにまとめた。正直な注記2枚(A237048の経緯・「世界初ではない」という位置づけ)も省略せずそのまま入れてある。
正直に失敗した2件(自分で見つけたバグ)
- A180291「新規発見」の誤検出 — 敵対的査読はVALID_CANDIDATEと判定したが、OEISのコメント欄をよく読むと、別の数学者(Luca Ferrigno氏)が2023年に同じコメント欄で本質的に同じ証明を既に書いていた。teai/maxは既知の議論を再現しただけで、新規の貢献ではない。フィルタリングの見落とし(証明が予想コメントと同じ塊に埋め込まれていて検出できなかった)が原因。新規成果としてカウントしていない。
- 「証明放棄」を「VALID_CANDIDATE」と誤判定するバグ — A259899でteai/maxが正直に「証明できない、理由はこう」と書いた文書を、敵対的査読が「論理的な矛盾がない」という理由だけでVALID_CANDIDATEと判定してしまった。「矛盾が無いこと」と「証明として成立していること」は別物なのに、査読プロンプトがその区別を明示していなかったのが原因。査読プロンプトを修正し、既に処理済みの17件を再監査して確認(該当1件のみ訂正、他は変更なし)。
正直な注記 このバグ発見自体、LLMベースの自動査読パイプラインの落とし穴を示している。「敵対的検証」を入れても、判定基準の設計が甘いと簡単にすり抜ける。人間(または、より厳しく設計された別のチェック)による最終確認が引き続き必要。
この実験の限界
これは社会的インパクトの大きい発見ではない。A196020は有名な問題ではなく、地味な組合せ論の恒等式で、しかも上述の通り「著者が別ルートで既に確信していた事実の第一原理からの穴埋め」という位置づけだ。OEIS編集者のレビューが通るかどうかもこの記事の時点では分からない。誇張はせず、実データとの検算という自分たちにできる範囲の裏取りと、その限界を正直に書いた。$1,000の予算のうち98%以上が未使用のまま残っており、この方式(数値検証→証明→敵対的査読→改訂)自体は今後もっと大きな規模で試せる。
teai.ioを無料で試す
クレジットカード不要・クーポン「WELCOME」で100クレジット。モデル名に teai/max と書くだけです。
無料で始める
他の記事を見る