AI発の証明は、人が消化した版を経て数学になる

Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, Melanie Matchett Wood, “Remarks on the disproof of the unit distance conjecture”（arXiv:2605.20695, 2026年5月20日投稿）。査読前のプレプリントである。要旨は「OpenAIが生成した単位距離予想への反例の、短く消化され、人手で検証された版と、それについての一連の考察を提示する」と書き、この議論は「少なくとも振り返ってみればEllenberg-Venkatesh、Golod-Shafarevich、Hajir-Maire-Ramakrishnaに帰属しうるアイデアに決定的に依拠している」とする。要旨自体は証明が正しいと宣言する文を含まないが、本文はそこで止まっていない。§1.4 に逐語 In Section 2 we give a complete proof of Theorem 1.1.。本稿が引く考察は、いずれも名前つきの節にある。§4 トーマス・ブルーム（p.9）: 逐語 while the original proof produced by AI was completely valid, it was significantly improved by the human researchers at OpenAI and the many other mathematicians involved in the present paper. The human still plays a vital role in discussing, digesting, and improving this proof, and exploring its consequences.。§11 メラニー・マチェット・ウッド（p.17）: 逐語 there is a history of closely related ideas in the literature, some of which are mentioned above, but which are not appropriately referenced in Chat GPT's paper. および Chat GPT is in some sense "familiar" with all the previous work。同節の冒頭には逐語 the mathematicians would have found a counterexample と without the claimed proof by Chat GPT, there is no particular reason anyone would have tried to look for a counterexample、続けて This result does not show us all the times AI has claimed to have a proof of something and been wrong.、その2文あとに In many cases, it will be easier for AI to convince humans it has a proof than to come up with a correct mathematical argument, and I believe that we as mathematicians are not sufficiently prepared for this.。§10 ヴィクター・ワン（p.16）: 逐語 made the verification process relatively smooth および Had the final digested argument been a bit longer, the process may have been trickier, as participants may have been less willing to invest time in checking details.、直後に It will be interesting to see how formalization progresses alongside AI.（formaliz は全文でこの1件）。§6 ダニエル・リット（p.12）: 逐語 After an internal model at OpenAI produced a solution, I was asked to check its correctness by Mark Sellke and Mehtaab Sawhney at OpenAI。§11 のウッドは推定の根拠を逐語 since our professional norms require us to cite previous work whose ideas influenced our work と書く。§5 W. T. ガワーズ（p.9）: 逐語 a famous (in my mathematical circles at least) open problem および with no human intervention once it had been trained and then given the problem to solve。補題2.2の着想については §1 に逐語 along the lines of an idea of Michel, Soundararajan, Ellenberg, and Venkatesh recorded in [10]（[10] は Ellenberg-Venkatesh, Reflection principles and bounds for class group torsion）。予想は §1.1 で上界 n^(1+o(1)) として述べられ（逐語 was conjectured by Erdős）、反例は §1 の Theorem 1.1 が点集合の列として述べる（逐語 There exists a sequence of point sets Pi in R2 such that |Pi | → ∞）。https://arxiv.org/abs/2605.20695 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹ ↩¹² ↩¹³ ↩¹⁴ ↩¹⁵ ↩¹⁶ ↩¹⁷ ↩¹⁸ ↩¹⁹ ↩²⁰ ↩²¹ ↩²² ↩²³ ↩²⁴ ↩²⁵

OpenAI, “Planar Point Sets with Many Unit Distances”（18ページ、日付表示なし）。AIが出した証明そのものを載せた技術論文であり、査読を経ていない。要旨は逐語 This disproves the well-known unit distance conjecture from [Erd46].。本文と参考文献にGolod-ShafarevichとHajir-Maire-Ramakrishnaを引く（逐語 This is the Hajir–Maire class-field-tower method, in an unramified pro-3 setting および the same tower-cutting mechanism developed further by Hajir, Maire, and Ramakrishna [HMR21]）。全文に対し Ellenberg Venkatesh Michel Soundararajan はいずれも0件（行末ハイフネーションを避けるため部分文字列でも照合した）。末尾は逐語 Below we also reproduce verbatim the original solution output by the internal model, before any automated grading or rewriting was performed. として採点も書き直しも通していないモデル出力を載せる。発表ページ https://openai.com/index/model-disproves-discrete-geometry-conjecture/ は直接の取得では403を返す（本稿は Internet Archive の保存版で本文を確かめた）。PDFはCDNから取得できる。https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf ↩ ↩² ↩³

Gil Kalai, 「Amazing: Erdős’ Unit Distance Problem was Disproved! It was achieved by AI!」（Combinatorics and more, 2026年5月21日）。数学者本人による個人ブログの記事であり、査読を経た論文ではない。OpenAIの社内モデルが単位距離予想への反例を見つけたと書き、構成は代数的整数論に依拠しているとする。その反例は、n点の間にn^(1+ε)を超える数の単位距離が現れる配置である。証明は9人の論文で「提示され、説明され、論じられている」と紹介する。以下の二つは記事本文ではなくコメント欄にある。カライ自身の返信（2026年5月24日）に、4CTからの50年を振り返って逐語 still in the past 50 years the role of computers in pure mathematics is rather restricted。カライ自身の別の返信（同5月28日）に、逐語 Checking is a major bottleneck so this is a great service.。ヨゼフ・ソリモシの評は、9人論文の共著者でもある Victor Wang がコメント欄に寄せたもので（同6月7日）、ハンガリー語の記事（ematlap.hu）の機械翻訳である。逐語 several of us have tried to construct a counterexample, from this perspective [the new result] is not surprising および The result is fantastic, I was most surprised by the depth of the solution.（いずれもカライの記述ではない）。1.0318 への改善の担い手については、読者 Stephan Lauermann の書き込み（同5月22日）に逐語 ChatGPT improved Will Sawin‘s point substantially, it seems. と improved the bound (not point) to 1.0318, it seems.（これもカライの記述ではない）。記事末尾の Updates には、逐語 Will Sawin proved a lower bound of に続けて数式画像 n^{1.014}; と n^{1.0318}、および Sawin also proved in the same paper a limit 1.2143 for the new method.（数式は <img alt> で描かれる）、続けて Following the OpenAI result, Anthropic reported being able to autonomously disprove the unit-distance conjecture (in its strongest form) with its system.。カライは本文に OpenAI の発表ページと技術論文へのリンクを置いており、後者は cdn.openai.com の PDF を指す。https://gilkalai.wordpress.com/2026/05/21/amazing-erdos-unit-distance-problem-was-disproved-it-was-achieved-by-ai/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹

OpenAI, “An OpenAI model has disproved a central conjecture in discrete geometry”（発表ページ, 2026年5月20日）。企業の発表文であり、査読を経ていない。直接の取得では403を返すため、Internet Archive の 2026年5月20日 19:35 UTC の保存版で本文を確かめた。見出し直下に Read the companion remarks のリンクを置き、本文に逐語 The proof has been checked by a group of external mathematicians. They have also written a companion paper explaining the argument and providing further background and context for the significance of the result.。https://web.archive.org/web/20260520193524id_/https://openai.com/index/model-disproves-discrete-geometry-conjecture/ ↩ ↩² ↩³ ↩⁴

Francesco Fournier-Facio, “A torsion-free non-sofic group”（arXiv:2608.02025, 2026年8月3日投稿）。査読前のプレプリントである。「2026年8月1日、OpenAIは数学の10件の主要な未解決問題への解法を発表した」と記録し、「8月1日のOpenAIの発表における『主結果について少なくとも10年間進展がなかった』という主張とは対照的に、この主張は8月3日に削除された」と書く（逐語は This claim has been redacted on 3 August.）。著者はLeavitt代数を使わずに非ソフィック群を構成する方法をProposition 1.2を使ったまま示し、「この証明がより易しい、より優れている、あるいはより初等的だとは主張しない」と述べる。v1 は2026年8月3日投稿、v2 は8月14日改訂（arXiv の Comments 欄は 5 pages. v2: small changes after several comments on the first version）。本稿が引く記述のうち、「soficity conjecture」への訂正（逐語 I do not think it was ever conjectured that all groups are sofic）、有限生成の仮定への訂正（逐語 The statement in [Ope26] insists that Γ and G be finitely generated, but all property に続けて性質(T)の群がそうだと述べる。括弧はPDFのテキスト層で機械照合できない）、および最初のドラフトで知ったという句（逐語 unlike the connection between Leavitt algebras and Thompson groups, which I learned about by reading the first draft。v2 でも括弧の前半 (unlike the connection between Leavitt algebras and Thompson groups) は残る）は v1 にあり、v2 では削られている。v2 で足された一文は逐語 To the best of my knowledge, this connection between Leavitt algebras and Thompson groups was first observed independently by Birget [Bir04] and Nekrashevych [Nek04].。v2 の謝辞に逐語 On 31 July 2026 I saw an early version of [Ope26] と I posted the first version of this note on my homepage on the evening of 1 August 2026, the day of the announcement.、続けて Goulnara Arzhantseva and Marcin Kotowski pointed to missing citations と This is an essential part of the process of doing mathematics。新規性の所在については両版に逐語 As it often happens with these things, the novelty is not so much in the proof と experts aware of [KT19] would probably have been able to prove Proposition 1.2, but they might not have thought of this statement.、続けて There are myriad possible statements strengthening [KT19], many of which are surely false, and many of which might be true but have no application. と AI models are not inconvenienced by constraints of time and resources, so they get to throw things at the wall and see what sticks.。https://arxiv.org/abs/2608.02025 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹ ↩¹² ↩¹³ ↩¹⁴ ↩¹⁵ ↩¹⁶

「Leiden Declaration on Artificial Intelligence and Mathematics」（2026年6月2日公表）。研究論文ではなく、擁護のための宣言文である。国際数学連合（IMU）の支持を受け、副会長Ulrike Tillmannの推薦文を掲載し、署名者数は2026年8月7日時点で3,461人だった。「現在の自動化技術は、もっともらしいが信頼できない、あるいは誤った議論を生成しうる」と書き、査読前の発表や帰属の失敗を脅威として名指しし（逐語 In many cases this leads to simplifications in reporting, such as overemphasizing the significance of automated tools and undervaluing the prior human contributions which have made those tools possible.）、「議論と結果の正しさおよび妥当性についての責任は、もっぱら人間の著者に残る」と勧告する。脅威の一つ目には続けて逐語 This applies not only to informal arguments, but also to formalizations, where the difficulty lies in the translation between computer-encoded and human presentations of concepts.。勧告は4節あり、第4節は商用AI宛て（逐語 Recommendations for commercial artificial intelligence および One is through the use of mathematics to advertise the capabilities of commercial artificial intelligence systems in public communications and public relations campaigns.）。宣言は自らを逐語 The Declaration reflects artificial intelligence technologies and mathematical practice as of May 2026. と時点で切っている。https://leidendeclaration.ai/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹ ↩¹² ↩¹³

OpenAI, “Ten advances in mathematics and theoretical computer science”（発表ページ, 2026年8月1日）。企業の発表文であり、査読を経ていない。直接の取得では403を返すため、Internet Archive の保存版2本で本文を確かめた。8月1日 09:08 UTC の版に逐語 These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate、および We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness, while the mathematical arguments themselves were generated by our system.、冒頭に have seen no progress on the main result for at least a decade。同じ版の「Responsibility to the mathematical community」節に逐語 including the signers of the Leiden declaration on AI and Mathematics と claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.。8月3日 06:56 UTC の版では同じ位置が逐語 each of which resolves or makes substantial progress on a long-standing open problem で、decade の語は無い。https://web.archive.org/web/20260801090839id_/https://openai.com/index/ten-advances-in-mathematics/ https://web.archive.org/web/20260803065650id_/https://openai.com/index/ten-advances-in-mathematics/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶

Gary Marcus, “OpenAI’s amazing — but vastly oversold — new model Astra”（本人のブログ, 2026年8月2日）。査読を経ない意見記事である。評者たちが個別の成功を全領域の卓越性と混同する合成の誤謬を指摘し、Ernie Davisの指摘として、選定に至るまでの試行数が非公開であること、OpenAI が自ら掲げた計算コスト2,000ドル（原典の逐語は OpenAI brags loudly that this was done for a total computation cost of $2000）が関係者の給与を含まないことを紹介する。「249ページの論文」にモデルの仕組みや検証方法についての記述が「1ページもない」と書きつつ、「Astra……は驚くべきものだ」とも書く。書き方については地の文に逐語 it appears that Astra's proofwriting is not on par with the proofs themselves。ヘンリー・ユエンの評（逐語 I am disappointed by the writeup of this proof）は、この記事の地の文ではなく、記事に埋め込まれたツイートである。Part III の地の文には逐語 Yesterday's tweet and blog were marketing, not science. Neither of those nor the 249-page math article that went with them give any information about how this was accomplished。2,000ドルの出所も同じ記事に埋め込まれた Greg Brockman のツイート（2026年8月1日）で、逐語 solved using an internal version of Astra, our next major model, for a total cost of about $2000 at Sol API prices。https://garymarcus.substack.com/p/openais-amazing-but-vastly-oversold ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹

Thomas F. Bloom, Will Sawin, Carl Schildkraut, Dmitrii Zhelezov, “The sum-product conjecture is false for real numbers”（arXiv:2605.28781, 2026年5月27日投稿）。査読前のプレプリントである。§1 末尾の「The role of AI in this proof」に逐語 The authors were inspired to revisit the possibility of disproving the sum-product conjecture using number fields of large degree by the recent OpenAI counterexample to the unit distance conjecture (see [2]).（[2] は9人の論文 arXiv:2605.20695）、続けて GPT-5.5 Pro was used as a sounding board in the early stages of the development of this proof, but the final proof, including all the main ideas, was almost entirely human-generated (the exception being the suggestion of Lemma 3.4, which replaced a more complicated result of Schinzel with a short elementary argument). Everything in this paper was written by the authors.。https://arxiv.org/abs/2605.28781 ↩ ↩²