English · 日本語
tkmt-lab
滝本竜彦（Tatsuhiko Takimoto）の研究室 · AI のチームで数学と科学を研究しています
信頼できる研究を地道に。
これまでの研究者の仕事への敬意をもって、社会に貢献する。
このページは日本語の要約です。正確な主張と、何をどこまで確かめたかは、英語のページと各リポジトリに書いています。
研究
フラーレンは、五角形と六角形でできた、サッカーボールのようなかご形の炭素の分子です（C60 がいちばん有名です）。ここで調べた「経路」は、ある五角形から別の五角形まで、六角形がまっすぐ一列に並んだ道のことで、かごの形を組み替える「一般化 Stone–Wales 変形」が働く場所です。十二面体から作る、ねじれたかごの無限の族 GC(k,l)[C20]（k > l > 0）について、どのかごにこの経路があるかを決める、割り算の余りを使った簡単な法則を見つけ、証明しました。小さいかごを単に拡大しただけではないかごの中で、経路のない最初のかごは、炭素原子 7,980 個です。
この問いは A. Bille、V. Buchstaber、E. Spodarev がフラーレンの未解決問題の一覧で定義したものです。この分類は Lean 4 で証明され、計算機が証明の全段階を確かめています。
論文1は一つの族について答えを出しました。この論文では、一般の定理を証明しました。決まった数の平らな格子の面を貼り合わせ、その大きさが一定の割合で大きくなっていくフラーレンの族なら、どれでも、かごを大きくしていくと「経路はあるか」の答えが、いずれ決まった周期でくり返します。Graver の目録の11の族に一度に当てはまり、一つの定理で無限に多くのかごが分かります。定理の形式版は Lean で証明されています。証明は周期があることを示しますが、一般には周期そのものを計算しません。族 K3 と C1 については、規則がはっきり分かっています。
この定理の形式版は Lean 4 で証明されています。ただし、論文の図形から形式版へ移す一段は、Lean ではなく文章による証明です。J. E. Graver の目録にある族 K3 と C1 については、その一段も含めて、すべて Lean で証明されています。族 O2 についても、直線上の結果と、二つのパラメータがどちらも2以上なら経路がないことを、族 D14 についても直線上の結果を、同じく Lean で証明しました。
どう確かめているか
- 形式証明：Lean 4 という証明の検査系が、証明の全段階を機械で確かめます。その証明が、別の者が先に書いておいた主張文と同じことの証明であることも、Comparator という道具で確かめています。
- 独立な導出：別のチームが、もう一方の証明を見ずに、別の証明を書きました。
- AI による点検：AI が文章の証明を読み、計算し直しました。
- 有限の計算：範囲を決めて、すべてを計算で調べました。
人間の専門家による査読は、まだ受けていません。結果が新しいかどうかも、確かめ切れていません。各リポジトリでは、主張ごとに、何を確かめ、何を確かめていないかを書いています。
研究の進め方
AI（OpenAI の Codex と Anthropic の Claude Code）が、探索、独立な検証、文献の調査、形式化を、別々のチームとして担っています。私（滝本竜彦）が方向を決め、判断し、公開するものとその限界の書き方に責任を持ちます。AI は著者に入れていません。
元になった研究への感謝
これらの結果は、この分野を切り開いてきた研究者の方々の仕事の上にあります。問いは、A. Bille、V. Buchstaber、E. Spodarev による未解決問題の一覧から生まれました。調べた形は、M. Goldberg と H. S. M. Coxeter の名を冠した構成と、それを広げた M. Dutour Sikirić と M. Deza の仕事、そして J. E. Graver の目録によるものです。K. Kutnar と D. Marušič によるフラーレンの辺連結性の研究、J. R. Büchi、C. C. Elgot、B. A. Trakhtenbrot による論理と有限オートマトンを結ぶ定理、Lean 4 と mathlib、Comparator と独立な検査器を作った方々の仕事も使わせていただきました。心から感謝します。この小さな仕事が、この分野にわずかでも新しいものを付け加えられたなら幸いです。
出典は各論文にすべて挙げています。
もう一つの仕事
小説家：滝本竜彦
連絡
質問や誤りのご指摘、関連する研究のお知らせは、research@tatsuhikotakimoto.com か、各リポジトリの GitHub の Issue でお願いします。
お知らせと研究室の日誌は X で：@tkmt_lab（英語）。
ライセンス
このサイトの文章は CC BY 4.0 で公開しています。各リポジトリのライセンスは、それぞれに書いています。