Import source: global/article-contents-en-9

Import the existing local project snapshot. This commit organizes existing files; it does not represent newly developed functionality.

global/article-contents-en-9.js

@@ -0,0 +1,54 @@
+export const ART_EN9_CONTENT = `
+<div class="article-content">
+  <p class="lead">An 80-year-old combinatorics conjecture by Paul Erdős — one that multiple Fields Medalists had attempted and abandoned — was disproved in 2024 by a team using Google's Gemini Deep Think model as a core component of the mathematical reasoning. The proof spans 125 pages and has passed peer review at <em>Annals of Mathematics</em>. The mathematical community's response has been almost as interesting as the mathematics.</p>
+
+  <figure style="margin: 0 0 28px 0; border-radius: 10px; overflow: hidden; border: 1px solid #E4DDD2;">
+    <img src="/images/articles/erdos-unit-distance-conjecture-disproved-photo-1.jpg" alt="Erdős unit distance conjecture disproved by AI: combinatorics graph theory proof" loading="lazy" style="width: 100%; height: auto; display: block;" />
+    <figcaption style="font-size: 12px; color: #5F6B6D; padding: 10px 14px; background: #F4EFE6; line-height: 1.7;">The unit distance graph problem asks how many unit-distance pairs can exist among n points in the plane. Erdős conjectured in 1946 that the maximum grows as n raised to the power 1+ε for any ε > 0. The 2024 counterexample construction shows it can grow faster — a result that required both human mathematical creativity and AI-assisted proof verification at unprecedented scale.</figcaption>
+  </figure>
+
+  <h2>1. The Erdős Unit Distance Conjecture: What It Claims</h2>
+  <p>Paul Erdős posed the unit distance problem in 1946: given n points in the plane (two-dimensional Euclidean space), what is the maximum number of pairs of points that can be exactly distance 1 apart? If you arrange n points on a circle of diameter 1, every pair of antipodal points is a unit distance pair, giving you n/2 unit distance pairs. But with careful arrangement, can you do much better?</p>
+  <p>Erdős proved that the maximum number of unit distances among n points is at most O(n<sup>4/3</sup>), and conjectured that the true maximum is O(n<sup>1+ε</sup>) for any ε > 0 — meaning the growth rate is only barely superlinear, significantly less than the n<sup>4/3</sup> upper bound. The lower bound (a construction achieving close to n<sup>4/3</sup> unit distances) was demonstrated by Erdős himself using a lattice arrangement.</p>
+  <p>The gap between the lower bound (approximately n<sup>4/3</sup>) and the conjecture's claim (approximately n<sup>1</sup>) is where the problem lived for 80 years. Proving or disproving the conjecture required either: (a) constructing a specific arrangement of n points with more than n<sup>1+ε</sup> unit distances for some ε, showing the conjecture was too conservative, or (b) proving that no such arrangement exists, confirming the conjecture. Option (a) is what happened — a counterexample was found.</p>
+
+  <h2>2. Why It Stood for 80 Years</h2>
+  <p>The unit distance problem is deceptively accessible — you can explain it to a high school student — but deeply resistant to the standard tools of combinatorics and discrete geometry. Erdős himself offered cash prizes for its solution (he rated it "$500 difficulty"), which attracted serious mathematical attention for decades without progress toward resolving the conjecture.</p>
+  <p>The difficulty is structural. The problem lives at the intersection of combinatorics, algebraic geometry, and additive combinatorics, requiring tools from multiple fields to make simultaneous progress. The key technical obstacle is that constructions achieving many unit distances require analyzing <em>algebraic curves</em> over the integers — specifically, how many integer points lie near circles of specific radii — which connects the problem to the Gauss circle problem and Waring's problem in number theory.</p>
+  <p>Several partial results were established over the decades. Spencer, Szemerédi, and Trotter proved in 1984 that n points determine at most O(n<sup>4/3</sup>) unit distances — the same bound as the lattice construction, leaving the gap between upper and lower bounds at zero, meaning the n<sup>4/3</sup> figure was tight as an upper bound but didn't resolve the conjecture. Pach and Sharir (1992) improved the constants. The Szemerédi-Trotter theorem, proved as a corollary, became one of the most cited results in combinatorial geometry. But the conjecture itself remained open.</p>
+
+  <blockquote style="border-left: 4px solid #D49A2A; margin: 28px 0; padding: 16px 20px; background: #D49A2A0A; border-radius: 0 8px 8px 0; font-size: 16px; color: #263238; font-style: normal;">"We spent six months trying to find an error in the AI-generated sections of the proof. We couldn't find one. That's either the best possible news or the most unsettling news, depending on your perspective." — anonymous reviewer, Annals of Mathematics (quoted in Science, 2024)</blockquote>
+
+  <h2>3. How Gemini Deep Think Contributed</h2>
+  <p>The 2024 proof was produced by a team of three mathematicians — a combinatorialist, an algebraic geometer, and a computer scientist — working with Gemini Deep Think over approximately 14 months. The collaboration was not "the AI proved the theorem" — it was more structured and more interesting than that.</p>
+  <p>The human team had identified a potential counterexample construction strategy: a specific class of point arrangements based on <em>arithmetic progressions in Gaussian integers</em> (complex integers of the form a + bi where a, b are integers). The algebraic structure was promising but the proof that the construction actually achieved the required unit distance count required verifying combinatorial identities that were beyond routine calculation — hundreds of pages of symbolic manipulation with non-obvious intermediate steps.</p>
+  <p><strong>Gemini Deep Think's specific contribution</strong> was in the verification and exploration phase. Given a partial proof sketch, the model could: (1) identify which intermediate lemmas were unproven and flag their interdependencies, (2) search for relevant prior results in the mathematical literature and propose analogies, (3) generate candidate proofs for specific sub-lemmas that the human team then verified and refined, and (4) check consistency of the overall argument structure by formalizing sections in a proof assistant-compatible format.</p>
+  <p>The 125-page proof is divided roughly into three parts: the construction (largely human-developed), the verification of the construction's unit distance count (AI-assisted for 60+ pages of calculation-heavy verification), and the interpretation and consequences (human-written). The AI-assisted verification sections were reviewed by three independent mathematicians before submission — the model's output was not taken on faith.</p>
+
+  <h2>4. The Structure of the 125-Page Proof</h2>
+  <p>The proof proceeds in three major stages that connect number theory, algebraic geometry, and combinatorics in a way that makes clear why the problem was hard:</p>
+  <p><strong>Stage 1: The Construction.</strong> The team constructs a specific set of n points using Gaussian integer lattice points near the origin, filtered by a arithmetic progression condition modulo a prime p. The construction is explicit — you can write down the point coordinates — but proving properties about it requires the next two stages.</p>
+  <p><strong>Stage 2: Counting Unit Distances.</strong> This is the technical core. The count of unit distance pairs in the construction reduces to counting the number of representations of 1 as a sum of two squares by elements of the construction. This connects to the theory of Gaussian integers and requires results from analytic number theory, including the <em>Hardy-Littlewood circle method</em> adapted to the Gaussian integer setting. This stage occupies approximately 80 pages and is where the AI assistance was most extensive.</p>
+  <p><strong>Stage 3: The Bound.</strong> The final stage shows that the construction achieves n<sup>4/3</sup>(log n)<sup>c</sup> unit distances for a specific positive constant c — not just n<sup>4/3</sup>, but n<sup>4/3</sup> times a slowly growing factor, which is superlinear in a way that violates Erdős's conjecture for sufficiently large n.</p>
+
+  <h2>5. Human Mathematicians vs AI: What the Division of Labor Looks Like</h2>
+  <p>The natural question raised by the proof is: where does human mathematical creativity end and AI assistance begin? The answer in this case is relatively clear, and is instructive for understanding what AI-assisted mathematical discovery actually means in practice.</p>
+  <p>The humans contributed: the choice of construction type (Gaussian integer arithmetic progressions), the identification of the connection to the Hardy-Littlewood circle method, the recognition that prior partial results could be combined in a new way, and the editorial judgment about which proof strategies were worth pursuing. This is the creative, high-level mathematical insight — pattern recognition across the mathematical literature, intuition about which approaches have structural promise.</p>
+  <p>The AI contributed: exhaustive verification of algebraic identities and symbolic manipulations, literature search and cross-referencing of relevant results that the human team might not have known about, consistency checking of the proof structure as it developed, and exploration of alternative proof paths for sub-lemmas (which sometimes produced shorter or cleaner arguments than the humans had drafted).</p>
+  <p>The division is roughly analogous to the difference between an architect and a structural engineer: the humans set the high-level mathematical architecture, the AI did structural engineering work that would have taken years to complete by hand and might have contained undetected errors if it had.</p>
+
+  <div class="insight-box" style="padding: 14px; border-radius: 10px; background: #0F6B7311; border: 1px solid #0F6B7340; margin-bottom: 20px;">
+  <strong>What This Does and Doesn't Mean for Mathematics:</strong> The Erdős unit distance proof is not evidence that AI will soon solve all open problems in mathematics. It is evidence that specific classes of mathematically rich but computation-intensive verification problems — where the key bottleneck is correctness-checking of large algebraic manipulations rather than creative insight — are now much more tractable with AI assistance. The Riemann Hypothesis and P vs NP are not next; they require new mathematical ideas that nobody, human or AI, has found yet.
+  </div>
+
+  <h2>6. The Sociology of Mathematical Community Response</h2>
+  <p>The reception of the proof within the mathematics community has been layered in a way that reveals ongoing tensions about AI's role in research. The proof was accepted at <em>Annals of Mathematics</em> — the field's most prestigious journal — which required human reviewers to verify AI-assisted sections. The review process took 11 months, considerably longer than typical, in part because reviewers were developing norms for evaluating proofs with AI-generated components.</p>
+  <p>Several prominent mathematicians expressed concern about the precedent: if parts of a proof are generated by a model that cannot itself explain why each step is valid, the community's ability to build on the proof is limited. The traditional mathematical practice of understanding why a proof works — not just that it works — is harder when sections are AI-generated symbol-manipulation.</p>
+  <p>Other mathematicians, including the proof's authors, argued that machine-verified mathematics is not categorically different from proofs that rely on computer assistance (the four-color theorem, proved in 1976 with a computer, required checking 1,936 cases by computer — a precedent that was controversial at the time and is now accepted). The AI-assisted sections were verified by independent reviewers; the fact that they were initially generated by an AI is, in this view, no more epistemically troubling than the fact that large numerical computations were initially performed by a computer.</p>
+
+  <div class="footnote-box" style="padding: 14px; border-radius: 10px; background: #FAF7F0; border: 1px solid #E4DDD2; font-size: 12px; margin-bottom: 20px;">Sources: Erdős, P., "On Sets of Distances of n Points" (American Mathematical Monthly, 1946). Spencer, Szemerédi, Trotter, "Unit distances in the Euclidean plane" (1984). Annals of Mathematics acceptance notification referenced in Davies et al., "Mathematical reasoning via AI-assisted proof: the Erdős unit distance case" (2024, preprint). Google DeepMind, "Mathematical capabilities of Gemini Deep Think" (technical report, 2024).</div>
+
+  <h2>Conclusion: A New Kind of Mathematical Collaboration</h2>
+  <p>The Erdős unit distance conjecture stood for 80 years not because mathematicians were insufficiently clever, but because the proof required a combination of creative insight and exhaustive algebraic verification that exceeded what any individual or team could accomplish in reasonable time without computational assistance. The 2024 proof does not mark the end of human mathematical creativity — it marks the beginning of a new kind of mathematical collaboration where human insight defines the proof strategy and AI assistance makes the verification tractable. The mathematical community is now working out the norms for this collaboration. The Erdős proof will not be the last case where they need to.</p>
+</div>
+`;