Nivat予想：AIが見つけたLeanの証明は何を確かめ、「理解」は何を加えるのか

2026年10月28日、数学者のBryna KraはポッドキャストLife, Automated¹で、面識のない人々からNivat予想の証明が送られてくるようになったと語りました。Nivat予想は、Kraが2012年にVan Cyrとともに主要な部分的結果の1つを証明した問題です。エピソードの書き起こしによれば、彼女は「しかも、それが正しいように見えるんです」と述べ、「問題は解けました。でも、そこに何が入っていたのかを、まったく理解しないままです」と続けました。

少なくとも1つの証明の候補が公開されています。GitHubリポジトリboonsuan/nivat³には、論文と、議論全体のLeanによる形式化が置かれています。READMEにはこうあります。「証明は、私のプロンプトに応えて、すべてGPT-6 Proが見つけた」、そして「Leanによる形式化とそれに付随する文書は、Codex上のGPT-6 Astra Ultraが作成した」。形式化は9月14日に、Leanの形式化の登録簿であるPalomarに登録されました。¹⁰READMEは、まだ起きていないことについても率直です。論文は「人間によって数学的に消化されていない」としています。

ですから、問いははっきりしています。Leanの検査には通るが、誰も説明していない証明は、数学に何をもたらすのか。以下では、予想が何を述べ、以前に何が知られていたか、Kraが何を語り、何を書いたか、リポジトリに何があるか、そのLeanの証明が何を立証しているか、そして「理解」が何を加えるのかを順に紹介します。出典はすべて2026年10月30日に確認しました。名前の分かる専門家がこの証明を確認したという公表されたものは見つかっておらず、Papexもこの証明を評価しません。

Nivat予想とは何か#

局所的な多様性が少なければ、全体の繰り返しが必ず生じる、という予想です。Kraは9月、テレンス・タオのブログへの寄稿でこう説明しています。

「正方形のタイルを敷き詰めた無限の格子を想像してほしい。どのタイルも赤か青に塗られている。決まった大きさ、たとえば幅 n 枚、高さ m 枚の長方形の窓をあらゆる位置に置き、その窓に何通りの色のパターンが現れるかを数える。予想が述べるのは、そうしたパターンが多くとも nm 通りなら、格子をある決まった0でないシフトでずらしたとき、彩色全体が繰り返す、ということだ」²

色は有限個であれば何色でもかまいません。赤と青は例にすぎません。パターンの数は、パターン複雑度と呼ばれます。「繰り返す」とは、0でない1つのシフトで彩色全体が変わらないことで、2つの独立な方向に繰り返す必要はありません。

2つの小さな例から、境目がちょうど窓の面積のところにある理由が分かります。

• 縞模様。 列を赤と青に交互に塗ります。2枚以上のタイルからなる窓には、赤の列から始まるか青の列から始まるかによって、2通りのパターンしか現れません。この彩色は、1行上にずらすと繰り返します。
• 1枚だけ違うタイル。 1枚の赤いタイルを除いて、すべてのタイルを青に塗ります。窓は、赤いタイルを含まない（すべて青の1パターン）か、nm 個の位置のどれかに赤いタイルを含むかのどちらかです。それで nm + 1 通りのパターンになり、どのシフトも赤いタイルを動かしてしまうので、この彩色は決して繰り返しません。

つまり、面積より1つ多いだけで、決して繰り返さない彩色がすでにありえます。予想は、面積以下ではそれが起こりえないと述べています。

1次元では、対応する命題は古典的な定理です。CyrとKraの2012年の論文の要旨が振り返るように、Morse–Hedlundの定理（1938年）は、記号の無限の列が周期的であるのは、ある n について長さ n の異なるブロックが多くとも n 個しかないとき、かつそのときに限る、と述べています。¹³Nivat予想は、ブロックの代わりに長方形を使って、2次元で同じことを問うものです。Wikipediaによれば¹⁸、Maurice Nivatは1997年の国際会議ICALPでこの予想を提起しました。Jarkko KariとEtienne Moutotは、これを「1997年に述べられて以来、未解決」と書いています。¹⁶

2026年9月より前に何が知られていたのか#

2つの方向からの部分的な結果です。1つは力学系を通じたCyrとKraの方向、もう1つはKariとSzabadosの方向で、Kraの言葉では「組合せ論的な問いを代数的な対象とみなし、ある種の多項式を使って無限のパターンを見つける」ものでした。主な結果を、それぞれが最初に公開された年の順に挙げます。

年	結果	出典
2012	CyrとKra：パターンの数が面積の半分以下なら周期的、P(n, k) ≤ nk/2	arXiv:1208.409013
2016	KariとSzabados：漸近的な版。周期的でない配置の複雑度が低くなるのは、「有限個の異なる長方形の形についてだけ」	arXiv:1605.0592914、ICALP 2015の論文を拡張
2017	Szabados：2つの周期的な配置の和については予想が成り立つ	arXiv:1710.0536015
2019	KariとMoutot：一様再帰的な配置については予想が成り立つ	arXiv:1904.0126716
2026	ColleとGaribaldi：高さ4枚の長方形、P(4, n) ≤ 4n。高さ3以下についてのCyrとKraの結果を拡張	arXiv:2606.1019317

Kraの寄稿は、2つの方向がなぜ重要だったかを説明しています。「同じ問題に取り組む2つの異なる方法が、私たちに叫んでいるように思えた。両者のあいだの概念的な橋を見つけよ、と。私たちは試みたがうまくいかず、別の問題に移った」。²彼女の言葉では、「この予想は30年近く、私たちの努力をはねつけてきた」。

Bryna KraはLife, Automatedで何を語ったのか#

エピソード「Is Math a Canary in the AI Coal Mine? (with Bryna Kra)」（数学はAIの炭鉱のカナリアか）は、KQEDのサイトで10月28日付になっています。¹Life, Automated は、ノースウェスタン大学ケロッグ経営大学院のRyan Institute on Complexityが制作し、KQEDが配信しており、ホストはJess Loveです。Kraはノースウェスタン大学の数学者で、ページにあるとおり、アメリカ数学会の元会長です。ページには書き起こしが載っており、「これはコンピュータが生成した書き起こしである。私たちのチームが確認したが、誤りがあるかもしれない」という注記が付いています。以下の引用は、その書き起こしからのものです。

証明はどう届いたか：「数週間前、AI企業から新しいモデルが出たころから、この問題に取り組んできた私たちのもとに証明が届き始めました。送ってきたのは、私たちの誰も知らない人たちでした。それは素晴らしいことです。数学者は、新しい人がその分野に入ってくるのを歓迎するものですから」。

何が欠けていたか：「そうですね、結果がどこから来たのかをたどるのが、とても下手でした。つまり、以前の結果から何を使っているのか、です。何が新しいのかを強調していませんでした。ブレイクスルーに至ったなら、序論にぜひ『ここが新しい点です』と書きたいところなのに」。そして、「何もかもを同列に扱っているような感じです」。この記事の冒頭で引用した言葉は、この後に続きます。

著者に尋ねる：「この人たちに返事を書いて、『会って証明を説明してもらえませんか』と尋ねました。でも、いつも会えない理由がありました」。そして、「そのうちの1人は、AIを全面的に使ったことを開示していました。それはかまいません。自分たちが何をしたかを開示したのですから。彼らは、数学をあまりよく知らない学部生だと言っていました」。Kraの説明によれば、これは送り手のうちの1人のことです。エピソードは誰の名前も挙げず、どの証明へのリンクもありません。

彼女が恐れていること：「それがしたことは、この分野を閉ざすことでした。今となっては、誰かがそれを読み通して理解しようとする動機がどこにあるでしょう。それがどこか新しいところにつながるのでない限り」。

彼女は、AIを使うことを拒んでいるわけではありません。同じエピソードでこう語っています。「読んでいるもので分からないところがあれば、使います。『この命題からあの命題へ、どうやって進むのか説明して』というふうに尋ねるには、素晴らしい方法です。それが本当に得意なんです」。

9月にテレンス・タオのブログに何を書いたのか#

彼女の寄稿「Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system.」²（深い定理は希少で難しかったので、深い思考を見分ける有効な仕組みになった。AIはこの仕組みを壊した）は、9月13日に掲載されました。

「今週、この分野に初めて足を踏み入れた研究者たちから、予想全体の証明と称するものをいくつか受け取った。AIを使ったと認める人もいたが、英語を磨くためか証明を確認するためだけだという。著者たちに、Zoomで会って議論を説明してもらえないかと尋ねたが、誰も誘いに応じなかった」

彼女は、確認することと理解することを分けています。「しかし、AIの使用を開示することと証明の正しさを確認することは、どちらも不可欠ではあるが、それだけでは要点を外している。これらの結果が正しいとしよう。それは数学への貢献だ。だが、それはさらに多くの問いを開く。私たちは何を学んだのか。著者は何に貢献したのか。この結果はどんな影響を持つのか」。²

そして、証明が何のためにあるのかについて。「証明は、何かが正しいことを示す証明書以上のものだ。それは物語であり、絵であり、洞察であり、説明なのだ」。

寄稿は、AIが生み出す数学を歓迎し（「AIが生成した証明を歓迎するし、人間だけによる証明はまれになると考えている」）、何が評価されるかの変化を求めています。「論文を書くだけでは、もはや十分ではない。著者は、証明の仕組みと、どうやってそこにたどり着いたかを説明できなければならない。学術誌は、発見、証明、形式化、説明という役割を区別し、それぞれを評価する必要がある」。

2つの話は、1つの点で食い違っています。9月にKraは、AIの使用を認めた送り手はそれを「英語を磨くためか証明を確認するためだけ」に使ったと書きました。10月には、1人の送り手がAIを全面的に使ったことを開示したと語りました。¹どちらの出典も、2つが同じ証明の集まりについての話なのかどうかを述べていません。

boonsuan/nivatのリポジトリには何があるのか#

このリポジトリは、9月14日からGitHubで公開されています。中には、2026年9月14日付の13ページの論文「Pattern complexity and Nivat's conjecture」（パターン複雑度とNivat予想）があり、著者欄にはGPT-6 Proとあります。要旨は「私たちはNivat予想を証明する」で始まります。⁷ほかに、mathlibライブラリの上に築かれたLean 4による形式化（「29のライブラリモジュールに、377の明示的な宣言が含まれる」）、メタデータのファイル formalization.yaml、検査のログがあります。9月27日からは「Nivat's conjecture: an exposition of the GPT-6 Pro proof」（Nivat予想：GPT-6 Proによる証明の解説）も置かれています。

リポジトリの記載による、誰が何をしたかは次のとおりです（モデル名はリポジトリの記載どおり）。

部分	担い手とされているもの	記載場所
証明の発見、論文の執筆	GPT-6 Pro	README3、論文7、formalization.yaml4
Leanによる形式化と文書	「Codex上のGPT-6 Astra Ultra」（メタデータのファイルでは「GPT-6 Astra」、フレームワークはCodex）	README3、formalization.yaml4
プロンプト、方向づけ、保守	Boon Suan Ho	README3、formalization.yaml4
提出前の確認	AIエージェント。状態は「agent-reviewed」（エージェントが確認済み）	formalization.yaml4
解説としての書き直し（9月27日）	Claude Opus 5.5	README3、解説8
人間の専門家による確認	主張なし	README3、formalization.yaml4

管理者は、自分の役割について率直です。「以下で強調するように、証明を見つけたのはGPT-6 Proであって、私ではない。私の役割は、モデルにプロンプトを与え、形式的な検証を手配することだった」。自分の限界についても同様です。「私はこの分野の専門家ではない。議論をきちんと消化したり、それにふさわしい解説を与えたりする資格が自分にあるとは考えていない」。READMEは、ほかの人を招いています。「証明を理解し、文脈に位置づけ、簡潔にし、説明したいと考える経験豊かな数学者は、大いに歓迎する」。³

人による確認について、9月27日の更新は、解説についてこう述べています。「元の論文と同じく、これはAIが書いたもので、人間の専門家による確認を受けていない。私の知る限り、人間が消化した証明の説明は今もない」。メタデータのファイルには、「人間の専門家による確認は、主張も記録もされていない」とあります。⁴記録そのものの限界にも触れています。「証明を生成した会話の記録は含まれていないので、帰属は、別途監査された履歴ではなく、管理者による開示である」。

時期について、9月14日付のREADMEの更新は、Kraの寄稿が「このリポジトリへの私の最初のコミットの約3時間前に掲載されたが、ここで報告する証明の生成と形式化の作業は、その寄稿を知る前に終えていた」としています。ブログのタイムスタンプは9月13日22:01（UTC）で、²GitHubは最初のコミットを9月14日01:44（UTC）と記録しています。⁹

これはKraが受け取った証明なのか#

分かりません。そう述べている出典も見つかりませんでした。Kraは、エピソードでも寄稿でも、送り手の名前を挙げず、証明へのリンクも示していません。READMEは、その証明がKraに送られたとは述べておらず、自らを「この分野の専門家ではない」とする管理者は、学生かどうかについて何も述べていません。Kraは、1週間で「証明と称するものをいくつか」受け取ったと書いています。²このリポジトリは公開されている候補の1つであって、Kraが語った学部生からの証明とは限りません。

Leanの証明は何を立証しているのか#

リポジトリは、Palomarの慣例に従い、命題を証明から切り離しています。READMEの言葉では、Challenge.lean は「証明のライブラリとは独立に、mathlibの概念だけを使って命題を述べ」、Solution.lean は「その同じ命題を証明する」。³平たく言えば、こうです。任意の有限のアルファベットと、整数格子の任意の彩色について、ある正の m と n に対して、すべての位置で数えた m×n の異なるパターンが多くとも mn 個しかないなら、ある0でないシフトで彩色は変わらない。

Palomarの記録によれば、機械的な検証は9月14日に通過しました。¹⁰PalomarのAboutページによれば、そのComparatorツールは、許された公理だけを使って「記録された形式的証明が、記録された形式的命題を証明していることを検証」し、証明はLeanのカーネルと、登録項目に記録された独立のカーネルで再実行されます。¹¹この登録項目では、NanoDaが挙げられています。READMEによれば、証明が使うのはLeanの3つの標準的な公理 propext、Classical.choice、Quot.sound だけです。

この種の検査に通ることが意味するのは、1つの特定のことです。形式的な命題が、Leanの基礎とmathlibの定義から導かれる、ということです。そのステップについては、13ページの論文も、それを書いたモデルも、誰も信用する必要はありません。これは、聞こえるより狭いことです。4つのことが人に残ります。

1. その命題はNivat予想か。 言語モデルが行うPalomarの自動の編集審査は、「選ばれた定理は、うたわれている有限アルファベットでの長方形複雑度の含意と、その単一の0でない大域的周期という結論を正確に表している」と判断しました。Palomarは、その審査が何であるかを率直に述べています。「これは結果を受理、承認、支持するものではない。Palomarは人間による編集の段階を加えない。ここでは、査読者のように数学を読む人は誰もいない」。Palomarの報告によれば、Challenge.lean は40行で、専門家なら証明を読まずに読める短さです。専門家が読んだという公開の報告は見つかりませんでした。
2. 定義の細かい部分。 命題は、mathlibの Set.ncard でパターンを数えます。mathlib自身の説明によれば、これは「s が無限なら、ジャンク値として0を取る」。¹²Challengeのファイルは、それがここでは問題にならない理由を説明しています。「アルファベットが有限で長方形も有限なので、このパターンの集合は有限であり、その自然な濃度は意図した数え上げの意味を持つ」。⁶こうした細部を確かめるのが命題の監査で、READMEは「独立した命題の監査」を求めています。
3. 論文。 メタデータにはこうあります。「Leanの命題の形式的な検査は、非形式的な原稿のすべての文を妥当と認めるものではない」。⁴
4. 何が新しく、それが誰のものか。 メタデータは「人間の専門家による独自性や先取権の評価は主張していない」としており、GPT-6 Proへの帰属は管理者の開示に基づいています。

また、Palomarが確認したのは1つのコミットだけで、Lean 4.33.0向けの9月14日のビルドです。Palomarはその保存版を保管していますが、mainブランチはその後変わっています。

これらのどれも、なぜ定理が正しいのかを読者に教えてはくれません。

「理解」は何を加えるのか#

READMEは、テレンス・タオの用語を借りています。「生成、検証、消化」です。³ページ自身の説明ではClaudeが草稿を書き、タオが確認したというタオの見解のまとめ¹⁹は、消化を「結果を理解し、文脈に位置づけ、説明すること」と定義しています。READMEは、プロジェクトをその枠組みの中に位置づけています。「このプロジェクトは最初の2つの活動を扱うもので、3つ目を終えたとは主張しない」。

Nivat予想の場合、消化とは、Kraが問い続けている問いに答えることです。

何が新しいのか：Kraは、受け取った証明が「何が新しいのかを強調していなかった」と語りました。¹GPT-6 Proの論文は、要旨で道筋を概説しています。アルファベットに有理数のラベルを付けた後、格子のシフトの多項式を適用しながら「長方形の面積について帰納法を用いる」。そして「帰納法により、予想は2つの差分作用素の積が c を零化する場合に帰着される。この場合はSzabadosが証明した」。⁷Szabadosの2017年の論文は、自身の言葉では「Kariと著者の代数的な手法を、CyrとKraの平衡集合と組み合わせる」ものです。¹⁵新しい議論が、KraとCyrが探した「概念的な橋」なのか、それとも別の道筋なのかは、専門家が答えるべき問いです。公の答えは見つかりませんでした。

それはどこから来たのか：Kraは、受け取った証明が「結果がどこから来たのかをたどるのが、とても下手だった」と語りました。このリポジトリは出典を記録しています。メタデータは、KariとSzabadosの論文とSzabadosの論文を「手を加えて用いた」研究、CyrとKraの論文を「背景」としています。⁴その記述が正しいかどうかも、やはりその分野を知る人が判断することです。

誰が質問に答えられるのか：Kraは寄稿の中で、「質問に答える能力」を、人間が著者であることの意味の一部に数えています。²管理者は、自分には証明を消化する資格がないとしています。AIが書いた解説はありますが、モデルの説明が消化の役目を果たせるかどうかは未解決の問いです。Kra自身もステップの説明にAIを使っており、同時に「この数学を人間が理解し、人間が使うことの役割は、きわめて重要だ」とも述べています。

誰がそれを行うのか：彼女の寄稿は、障害をはっきり挙げています。「注意深い検証と見事な解説は、その仕事に報いがなければ行われない」。

主張、検証、説明：今どこにあるのか#

以前の記事では、発見、検証、説明が今では別々に、違う人やツールから、違う日付で届くことを述べました。10月30日時点で、出典の記述によれば次のとおりです。

	状態	出典
主張	完全な証明。9月14日付で、著者欄にGPT-6 Proとある論文。Kraは、受け取った証明が「正しいように見える」としている。	リポジトリ、KQEDの書き起こし1
機械による確認	Leanによる形式化。9月14日、Palomarの機械的な検証に通過し、自動の審査も妨げとなる問題を見つけなかった	Palomarの登録項目10
人による確認	リポジトリは何も主張していない。名前の分かる専門家による公表された確認は見つからなかった。	README3、formalization.yaml4
説明	管理者の知る限り、人間が消化した説明はない（9月27日）。AIが書いた解説はあるが、人間の専門家による確認は受けていない。	README3

どこで追うか#

Nivat予想は、Papexが追っている未解決問題の一覧には入っておらず、私たちはこの予想についての主張を加えていません。Papexが追っている問題についてのAIを使った主張は、papex.org/ai-claims（英語）に、それぞれ出典の記述どおり、リンクとともに載せています。Nivat予想について注目すべき場所は、命題の監査と解説を求めているリポジトリ³と、そのPalomarの登録項目¹⁰です。

残る問い#

この件が提起する問いのうち、まだ定まった答えがないと私たちが考えるものを挙げます。

• AIが見つけた証明の形式的な命題は、誰が読むべきか。そして、ほかの人が頼れるように、その読解はどこに記録されるべきか。
• AIが書いた解説は消化と見なせるのか。それとも消化には、証明について質問に答えられる人が必要なのか。
• プロンプトを与えた人、証明の発見と形式化を担ったとされるモデル、そしていずれそれを説明する人の間で、功績はどう分けられるべきか。
• 生成の記録が残されていないとき、帰属は、このリポジトリの言葉では「別途監査された履歴ではなく、管理者による開示」になる。作業の時点で、何を残しておくべきか。

このリポジトリは、モデルが何をしたか、管理者が何をしたか、検査が何を対象としているか、そしてまだ誰も何をしていないかを率直に示しています。最後の点がなぜ重要なのかは、Kraの寄稿が述べています。「私たちが数学を前進させるのは、書くものによってではなく、学び、確かめ、応用し、他者に教えるものによってである」。²

出典#

1. Is Math a Canary in the AI Coal Mine? (with Bryna Kra), Life, Automated（KQED、2026年10月28日）、ページとコンピュータが生成した書き起こし、2026年10月30日確認 ↩ a b c d e
2. Bryna Kra, "Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system."（Terence Taoのブログへの寄稿、2026年9月13日）、2026年10月30日確認 ↩ a b c d e f g h
3. boonsuan/nivat、README（GitHub）、2026年10月30日確認 ↩ a b c d e f g h i j k l
4. boonsuan/nivat、formalization.yaml、2026年10月30日確認 ↩ a b c d e f g h i
5. boonsuan/nivat、STATUS.md、2026年10月30日確認
6. boonsuan/nivat、Challenge.leanとSolution.lean、2026年10月30日確認 ↩
7. Pattern complexity and Nivat's conjecture（paper/nivat.tex、2026年9月14日付、著者欄はGPT-6 Pro）、2026年10月30日確認 ↩ a b c
8. Nivat's conjecture: an exposition of the GPT-6 Pro proof（paper/exposition.tex、2026年9月27日付、著者欄はClaude Opus 5.5）、2026年10月30日確認 ↩
9. boonsuan/nivat、コミット履歴（GitHub）、2026年10月30日確認 ↩
10. Palomarの登録項目PALOMAR-2026-09-14-000003、バージョン1と、その登録記録、公開された審査、2026年10月30日確認 ↩ a b c d
11. About Palomar（Palomar registry）、2026年10月30日確認 ↩
12. Mathlib, Mathlib/Data/Set/Card.lean（GitHub）、2026年10月30日確認 ↩
13. Van Cyr and Bryna Kra, Nonexpansive Z^2 subdynamics and Nivat's conjecture（arXiv:1208.4090、2012年）、2026年10月30日確認 ↩ a b
14. Jarkko Kari and Michal Szabados, An Algebraic Geometric Approach to Nivat's Conjecture（arXiv:1605.05929、2016年）、2026年10月30日確認 ↩
15. Michal Szabados, Nivat's conjecture holds for sums of two periodic configurations（arXiv:1710.05360、2017年）、2026年10月30日確認 ↩ a b
16. Jarkko Kari and Etienne Moutot, Decidability and Periodicity of Low Complexity Tilings（arXiv:1904.01267、2019年）、2026年10月30日確認 ↩ a b
17. C. F. Colle and E. Garibaldi, A Modular Structure Theorem for Minimal Periodic Decompositions and Periodicity of Configurations with P(4,n) ≤ 4n（arXiv:2606.10193、2026年6月）、2026年10月30日確認 ↩
18. Nivat's conjecture（Wikipedia）、二次資料、2026年10月30日確認 ↩
19. Terence Tao on AI in mathematics (and beyond), a living summary（tao-web、最終更新2026年10月28日）、2026年10月30日確認 ↩