待翻譯：Examples for use of AI and especially LLMs in major mathematical developments

AI 服務暫時不可用，以下為來源正文，待恢復後補全翻譯。

big list - Examples for the use of AI and especially LLMs in major mathematical developments - MathOverflow Asked 9 months ago Modified today Viewed 28k times 108 $\begingroup$ The purpose of this question is to collect examples where large language models (LLMs) like ChatGPT have led to major mathematical developments. Please only post verified major achievements in which AI led to the solution. The emphasis in this question is on LLMs, but answers about other machine-learning tools are also welcome. Edit (July '26): in view of recent developments and to keep the question useful I would like to make some restrictions: First the question refers now to major developments and not merely notable ones. (If in doubt contribute a comment.) Second the question refers to cases where AI led to the solution. Third, please post VERIFIED major achievements. This question complements two questions that I asked before: Experimental mathematics leading to major advances (January 2010) and The use of computers leading to major mathematical advances II (June 2021). I think it will be useful to keep track of mathematical achievements based on LLMs or assisted by LLMs since it is considered a serious possibility that LLM's have the potential to change (and automatize) or at least assist research in mathematics. A related question specifically about Deep Mind is this: What mathematical problems can be attacked using DeepMind's recent mathematical breakthroughs? ; Another related question referring to deep learning is What are possible applications of deep learning to research mathematics? . big-list machine-learning experimental-mathematics artificial-intelligence Improve this question edited Jul 28 at 9:10 community wiki 14 revs, 7 users 61% Gil Kalai $\endgroup$ 19 – Sam Hopkins ♦ 2025-10-26 17:43:38 +00:00 Commented Oct 26, 2025 at 17:43 – LSpice 2025-10-26 20:27:21 +00:00 Commented Oct 26, 2025 at 20:27 – Gil Kalai 2025-10-27 19:59:04 +00:00 Commented Oct 27, 2025 at 19:59 – LSpice 2025-10-28 14:57:16 +00:00 Commented Oct 28, 2025 at 14:57 – D.R. 2026-05-12 19:13:04 +00:00 Commented May 12 at 19:13 Sorted by: Reset to default 1 2 Next 70 $\begingroup$ As already mentioned elsewhere on MO, the Jacobian conjecture has been disproved, by Claude-Fable-prompted-by-Alpöge-and-Mathew (July 2026): $$((1+xy)^3 z + y^2 (1+xy) (4+3xy),\\ y + 3 x (1+xy)^2 z + 3 x y^2 (4+3xy),\\ 2 x - 3 x^2 y - x^3 z): \mathbb{C}^3\to \mathbb{C}^3$$ has Jacobian determinant $-2$, and sends $(0, 0, -1/4)$, $(1, -3/2, 13/2)$, and $(-1, 3/2, 13/2)$ to $(-1/4, 0, 0)$ EDIT: Connell and Van den Dries have shown that if the Jacobian conjecture is false, then there is a counterexample with integer coefficients and Jacobian determinant 1. I asked ChatGPT 5.6 Sol Max if it could construct such a counterexample from the given counterexample, and it said to set $u := 1+ 4xy$ and to define $G : \mathbb{C}^3 \to \mathbb{C}^3$ by $$\eqalign{G_1(x,y,z) &:= x - 6x^2y - 4 x^3z \cr G_2(x,y,z) &:= y + 6xu^2z + 12 xy^2( 4 + 12xy) \cr G_3(x,y,z) &:= u^3z + 2y^2u(4 + 12xy)\cr}$$ Link to ChatGPT conversation. (Actually, I see now that someone else is a faster prompter than I am.) Improve this answer edited Jul 27 at 19:48 community wiki 4 revs Timothy Chow $\endgroup$ 11 – darij grinberg 2026-07-20 14:39:40 +00:00 Commented Jul 20 at 14:39 – Timothy Chow 2026-07-20 15:50:39 +00:00 Commented Jul 20 at 15:50 – Lazzaro Campeotti 2026-07-20 15:58:22 +00:00 Commented Jul 20 at 15:58 – Timothy Chow 2026-07-20 17:41:52 +00:00 Commented Jul 20 at 17:41 – Timothy Chow 2026-07-21 20:23:21 +00:00 Commented Jul 21 at 20:23 69 $\begingroup$ A counterexample to Erdős's unit distance conjecture has been found by an internal OpenAI model. This is by far the most famous problem solved by an AI (as of May 2026). An exposition of the proof (along with commentary from some prominent mathematicians) is available here. OpenAI has produced a short marketing video. DISCLAIMER: The link is provided here for the convenience of those who think that OpenAI's statements are relevant to the discussion. It is not an endorsement of OpenAI's views or their products. Improve this answer edited Jul 14 at 17:24 community wiki 4 revs, 3 users 71% Alf $\endgroup$ 23 – Carlo Beenakker 2026-05-20 21:08:08 +00:00 Commented May 20 at 21:08 – Timothy Chow 2026-05-21 02:38:24 +00:00 Commented May 21 at 2:38 – Jochen Glueck 2026-05-22 11:35:45 +00:00 Commented May 22 at 11:35 – Jochen Glueck 2026-05-28 12:45:57 +00:00 Commented May 28 at 12:45 – Jochen Glueck 2026-05-28 12:52:56 +00:00 Commented May 28 at 12:52 44 $\begingroup$ Boris Alexeev and Dustin Mixon posted in Oct. 2025 their paper Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof, where they had an LLM generate the Lean formalization of their proof. In my view this is one of the promising uses of LLMs, because the verifier naturally guards against hallucinations. The problem is notable: they give a counterexample to a $1000 Erdős problem (as well as noting that Marshall Hall had published a counterexample before Erdős made the conjecture). My caveat: a human must still verify that the definitions and the statement of the main theorem are correct, lest the LLM generate a correct proof, but of a different theorem. (update: It's verified.) Improve this answer edited Jul 31 at 17:23 community wiki 3 revs, 3 users 82% Lior Silberman $\endgroup$ 5 – Timothy Chow 2025-10-31 14:32:08 +00:00 Commented Oct 31, 2025 at 14:32 – Timothy Chow 2025-10-31 14:39:16 +00:00 Commented Oct 31, 2025 at 14:39 – NooneAtAll3 2025-11-07 02:12:26 +00:00 Commented Nov 7, 2025 at 2:12 – Kevin Buzzard 2025-11-08 01:57:39 +00:00 Commented Nov 8, 2025 at 1:57 – user1079 2025-11-09 13:32:48 +00:00 Commented Nov 9, 2025 at 13:32 37 $\begingroup$ ChatGPT Sol, prompted by Akhil Mathew, found an example of a group scheme of order $4$ where the $4$-th power map is not equal to the trivial map. This shows that a basic finite group theory result, that $g^{|G|}=1$, does not hold in group schemes, answering a question of Grothendieck. Formalized here in Lean; I learned about it from Kevin Buzzard's blog. Everything that follows is just an exposition of what I learned from the Lean write up, and particularly from Kevin Buzzard's comments on it. Let $$R = \mathbb{Z}[a,b]/\langle a^3, b^3, a^2b-2 \rangle.$$ This is a commutative ring with $512$ elements, a nilpotent thickening of $\mathbb{F}_2$. Every element of the ring can be written uniquely as $\sum_{i,j=0}^2 c_{ij} a^i b^j$ for $c_{ij} \in \{ 0,1 \}$, but it is not an $\mathbb{F}_2$-algebra, we have $2 = a^2b \neq 0$ and $2b = a^2b^2 \neq 0$. However, $2a=2 b^2 = 4=0$. Let $$A = R[U,V]/\langle U^2 - ab U + b^2 V, V^2 - a^2 V \rangle.$$ Every element of $A$ can be written uniquely as $\sum_{k,\ell=0}^1 r_{k\ell} U^k V^{\ell}$ for $r_{k \ell} \in R$, so this is free of rank $4$ as an $R$-module. Define $\Lambda \in A$ to be $1+aU+bV+abUV$. Our coproduct $\Delta : A \to A \otimes_R A$ is $$ \begin{array}{lcl} \Delta(U) &=& U \otimes 1 + \Lambda \otimes U \\ \Delta(V) &=& V \otimes \Lambda + 1 \otimes V\\ \end{array}.$$ The counit is $\epsilon(U) = \epsilon(V) = 0$. A computation which I have no insight into checks that the above map is well defined, and that $\Delta(\Lambda) = \Lambda \otimes \Lambda$. Therefore, $$\Delta^{(4)}(U) = U \otimes 1 \otimes 1 \otimes 1 + \Lambda \otimes U \otimes 1 \otimes 1 + \Lambda \otimes \Lambda \otimes U \otimes 1 + \Lambda \otimes \Lambda \otimes \Lambda \otimes U$$ so the $4$-th power map, $\nabla^{(4)} \circ \Delta^{(4)}$, sends $U$ to $(1+\Lambda+\Lambda^2+\Lambda^3) U$. In contrast, the trivial map sends $U$ to $\epsilon(U) = 0$. If we reduce modulo $a^3$, $b^3$ and the quadratics in $U$ and $V$, we get $1+\Lambda+\Lambda^2+\Lambda^3 = 4 + 6 a U + 6 b V - 4 a^2 b^2 V + 14 a b U V$. If we then further quotient by $4=2a=2b^2=0$, we get $1+\Lambda+\Lambda^2+\Lambda^3 =2bV=a^2 b^2 V$. So $(1+\Lambda+\Lambda^2+\Lambda^3) U = a^2 b^2 UV \neq 0$, showing that the $4$th power map isn't trivial. It's hard to know which breakthroughs are important enough for this thread, but this is a problem which Deligne, Grothendieck and Tate all worked on and which, more personally, my friends and I talked about a lot in grad school, so it seems worth noting. Improve this answer edited Jul 31 at 17:26 community wiki 6 revs, 2 users 99% David E Speyer $\endgroup$ 1 – David E Speyer 2026-08-01 01:17:13 +00:00 Commented Aug 1 at 1:17 28 $\begingroup$ Here is an Oct. 2025 example Counterexample to majority optimality in NICD with erasures From the abstract: We asked GPT-5 Pro to look for counterexamples among a public list of open problems (the Simons ``Real Analysis in Computer Science'' collection). After several numerical experiments, it suggested a counterexample for the Non-Interactive Correlation Distillation (NICD) with erasures question: namely, a Boolean function on 5 bits that achieves a strictly larger value of E|f(z)| than the 5-bit majority function when the erasure parameter is p=0.40. In this very short note we record the finding, state the problem precisely, give the explicit function, and verify the computation step by step by hand so that it can be checked without a computer. In addition, we show that for each fixed odd n the majority is optimal (among unbiased Boolean functions) in a neighborhood of p=0. We view this as a little spark of an AI contribution in Theoretical Computer Science: while modern Large Language Models (LLMs) often assist with literature and numerics, here a concrete finite counterexample emerged. Improve this answer edited Jul 14 at 20:33 community wiki 2 revs, 2 users 93% Sudipta Roy $\endgroup$ 26 $\begingroup$ OpenAI announced on July 10, 2026 that their latest model, GPT 5.6 Sol Ultra, proved the cycle double cover conjecture, a major open problem in graph theory that has been open for about 40 years. There is also an accompanying proof in Lean, which of course does not automatically rule out the possibility of a subtle misformalization somewhere, but which greatly reduces the chances of an incorrect argument. EDIT: See also Thomas Bloom's comments (link posted by Sam Hopkins elsewhere on MO). The "Sol" and "Ultra" terms are slightly confusing. ChatGPT now has separate "Chat" and "Work" modes, and I think "Ultra" is available only in "Work" mode, and is not simply the maximum setting, because there is also a "Max" setting. According to ChatGPT itself: Max is a reasoning-effort setting above Extra High/xhigh. It gives GPT‑5.6 more time to explore alternatives, check work, and revise its approach. Ultra is a multi-agent mode. It coordinates four agents in parallel by default, which can finish suitably divisible complex work faster but generally consumes more tokens or credits. "Sol" on the other hand is in contrast to "Terra" and "Luna". Again, according to ChatGPT, Sol is the flagship tier, Terra is the balanced tier, and Luna is the fastest and most economical tier. Improve this answer edited Jul 14 at 19:02 community wiki 3 revs, 2 users 95% Timothy Chow $\endgroup$ 8 – Jim Conant 2026-07-11 16:51:40 +00:00 Commented Jul 11 at 16:51 – Timothy Chow 2026-07-11 18:07:14 +00:00 Commented Jul 11 at 18:07 – Gordon Royle 2026-07-12 03:22:11 +00:00 Commented Jul 12 at 3:22 – Gordon Royle 2026-07-12 04:13:18 +00:00 Commented Jul 12 at 4:13 – Jérôme JEAN-CHARLES 2026-07-21 19:44:59 +00:00 Commented Jul 21 at 19:44 26 $\begingroup$ Anthropic announced a paper which shows that over 2/3rds of the zeros of the Riemann zeta function lie on the critical line. The preprint is here. [truncated for AI cost control]