arXiv CSopen access

Advancing Mathematics Research with AI-Driven Formal Proof Search

2026-5-22

Advancing Mathematics Research with AI-Driven Formal Proof Search George Tsoukalas1 , Anton Kovsharov1 , Sergey Shirobokov1 , Anja Surina1 , Moritz Firsching1 , Gergely Bérczi2 , Francisco J. R. Ruiz1 , Arun Suggala1 , Adam Zsolt Wagner1 , Eric Wieser1 , Lei Yu1 , Aja Huang1 , Miklós Z. Horváth1 , Andrew Ferrauiolo1 , Henryk Michalewski1 , Codrut Grosu3 , Thomas Hubert1 , Matej Balog1 , † Pushmeet Kohli1 and Swarat Chaudhuri1 †

†

†

arXiv:2605.22763v1 [cs.AI] 21 May 2026

1 Google DeepMind1 , 2 Aarhus University, 3 Google

Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method’s ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.

1. Introduction Large language models (LLMs) have recently shown remarkable promise in solving complex mathematics problems [21, 65], but unreliability remains a primary barrier to their integration into mathematics research. Because LLM-generated natural language proofs can contain subtle logical errors, or “hallucinations,” they require expensive expert review. Mistakes in unreviewed intermediate steps can cascade through a proof, limiting the complexity of tasks that can be delegated to AI. Recent efforts [29, 1] mitigate these issues by using AI to generate proofs in formal languages like Lean [43], in which a compiler automatically verifies every logical step. So far, successes of this paradigm have been concentrated in competition mathematics and the human-aided formalization of natural language arguments [28]. In this paper, we demonstrate its broader potential through a large-scale evaluation on open research-level problems. To this end, we developed a framework, AlphaProof Nexus, for LLM-aided proof generation and used it to build a basic agent in which a set of subagents independently searches for proofs with feedback from the Lean compiler. We also developed a “full-featured” agent in which subagents are coordinated using an evolutionary algorithm [46] and can use AlphaProof [29], a system for olympiad-level Lean theorem-proving based on reinforcement learning, as a focused proof tool. Our full-featured agent autonomously solved 9 Erdős problems out of 353 attempted, including two questions that had been open for 56 years [54, 7, 17], at the inference cost 1† Equal contributions. The first three authors are in random order. Correspondence to pushmeet@google.

com and [email protected].

© 2026 Google DeepMind. All rights reserved

Advancing Mathematics Research with AI-Driven Formal Proof Search

of a few hundred dollars per problem. It also proved 44/492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS), resolved a 15-year-old open question on Hilbert functions in algebraic geometry, improved an open bound in convex optimization by discovering a novel algorithmic parameter schedule, identified several misformalizations in the literature, helped resolve an open problem from Ben Green’s well-known list [27], and is aiding ongoing research efforts on quantum optics and graph theory. To understand the impact of the agent design on these results, we did a post-hoc analysis of the performance of the full-featured and basic agents, as well as two agents with intermediate capabilities, on the 9 Erdős problems solved by the full-featured agent. Remarkably, the basic agent solved all 9 problems, though at a higher cost on the harder problems. Overall, our results demonstrate the utility of LLM-powered formal proof search as a tool for mathematics research, and point to an ongoing shift from specialized trained systems toward simple agentic loops as LLMs become more capable. All Lean proofs and select natural-language proofs are available in https://www.github.com/google-deepmind/ alphaproof-nexus-results.

2. AlphaProof Nexus Lean. Lean [43] is a proof assistant in which definitions, theorems, and proofs are all mechanically verified code. Proofs are constructed via a sequence of applications of tactics, or elementary proof steps. Lean’s compiler “executes” a proof tactic-by-tactic, tracking the proof goals pending after every tactic. A proof is correct if it leads the compiler to a state with no pending goals. Lean includes a special sorry tactic, which immediately closes pending goals while passing the type checker. Proving a theorem thus amounts to the generation of type-safe code without sorry tactics. Input and Output. AlphaProof Nexus is a new framework for agents that query frontier LLMs and the Lean compiler. The agents take as input a Lean file consisting of a target theorem with sorry in place of a proof, along with definitions and library imports on which the theorem depends (we refer to such a file as a proof sketch). Optionally, the user may input additional natural-language context and domain knowledge encoded in Lean. The input sketch is annotated with user-provided markers that delineate which code segments the agent may modify (see Fig. 1). Within EVOLVE-BLOCK markers, the agent can introduce helper lemmas, definitions, and proof steps. EVOLVE-VALUE markers are used to enclose expressions (e.g., parameters) whose values the agent can change. On successful termination, the agent outputs a sorry-free proof of the target theorem. Agent Architecture. The basic agent in AlphaProof Nexus (agent (A)) consists of a set of prover subagents that execute independently with no shared state. Each subagent is a “Ralph loop” [31] consisting of a sequence of episodes: multi-turn LLM inference loops (based on Gemini 3.1 Pro) in which the subagent can reason via chain-of-thought and refine the sketch using a search-and-replace tool. After each turn, the subagent uses Lean to check that the current proof sketch compiles; if it does not, Lean’s error message is used to direct the 2

Advancing Mathematics Research with AI-Driven Formal Proof Search

/- Erdos 125 variant from https: / / github.com / google -deepmind / formal -conjectures / blob / main / FormalConjectures / ErdosProblems / 125.lean. -/

j Thought (5m 3s): “Analyzing the problem structure. . . The answer should be False since the lower density is 0.” v search_replace

- default + False - sorry + constructor + · intro h; exact False.elim h + · intro h + have : (A+B).lowerDensity = 0 + ...

namespace Erdos125 open ... -- EVOLVE-BLOCK-START -- You can put your definitions and lemmas here. -- EVOLVE-BLOCK-END theorem target_theorem_0 : answer( -- EVOLVE-VALUE-START default -- EVOLVE-VALUE-END ) ↔ 0 < ({x : ℕ | (digits 3 x).toFinset ⊆ {0, 1}} + {x : ℕ | (digits 4 x).toFinset ⊆ {0, 1}} ).lowerDensity := by -- EVOLVE-BLOCK-START sorry -- EVOLVE-BLOCK-END

(a)

Ô attempt_goals_with_alphaproof

j Thought (1m 35s): “AlphaProof couldn’t solve independent_bases_zero_ density. . . This is too monolithic. I need to decompose it: first show that for any 𝜖 > 0 there exist aligned scales 𝑘, 𝑚 with 3𝑘 ≈ 4𝑚 , then bound the sumset gaps at those scales.”

- lemma independent_bases_zero_density : (A+B).lowerDensity = 0 := by sorry + lemma exists_k_m_ratio_close ... + := by sorry + lemma gap_at_aligned_scale ... + := by sorry + lemma independent_bases_zero_density + : (A+B).lowerDensity = 0 := by + ...

== Role and Goal == [...] == Task == [...] == Sketch Structure == [...] == Prior Attempts == Attempt 1 8 Elo: 1505 theorem target_theorem_0 : answer( False ) ↔ 0 < (...).lowerDensity ...

Ô attempt_goals_with_alphaproof

<natural_language_plan> 1. Define restricted-digit sets A, B. 2. Prove size bounds. [...] </natural_language_plan>

✓ exists_k_m_ratio_close ✓ gap_at_aligned_scale ✓ independent_bases_zero_density (6/6 proved ¦)

2m 40s

j Thought (54s): “Reflections on Tool Use”

== Current Plan == -- EVOLVE-BLOCK-START have h_positive_density : 0 < (...).lowerDensity := by sorry -- EVOLVE-BLOCK-END theorem target_theorem_0 : answer( True ) ↔ 0 < (...).lowerDensity ...

<natural_language_plan> 1. Set answer to False . . .

== Instructions == [...]

õ Admitted to Population Database.

(b)

4s ✓

. . 4 more search_replace iterations .

AlphaProof: 3/5 goals proved, 2 open AlphaProof feeback: [...]

8 Elo: 1480 [...] 8 Elo: 1520 [...]

10m 1s

✓ A_bound ✓ B_bound ✓ sum_size_bound × independent_bases_zero_density (3/4 proved)

v search_replace

Attempt 2 Attempt 3

3s ✓

2. Decompose density proof into sublemmas. . . . . .

</natural_language_plan> è Generation complete. è Proof validated.

(c)

Figure 1 | Example inputs/outputs for an AlphaProof-equipped agent (applied to Erdős 1 #125). The user provides a Lean file with a specification of the problem, and an empty proof body replaced with the sorry placeholder. (a) Modifications are permitted only within EVOLVE-BLOCK and EVOLVE-VALUE markers. (b) During sketch refinement, the prover subagent is shown an assembled prompt template with the current proof, and optionally prior attempts/sketches, their Elo ratings, and feedback from AlphaProof’s attempts on unsolved goals. (c) The prover reasons about the problem informally and invokes tools. In this example, the prover invoked AlphaProof which resolved all but one goal. The prover then decomposed that goal into three simpler lemmas, and called AlphaProof again, which then resolved all remaining goals. The agent also produced a natural language summary of its attempt at the end of generation.

3

Advancing Mathematics Research with AI-Driven Formal Proof Search

next turn. If the sketch contains sorry when the episode terminates, the subagent adds a comment to the sketch summarizing the lessons learned from the episode. The resulting sketch is the input to the next episode. We extended the basic agent into one (B) that can query AlphaProof [29] to fill out missing parts of sketches. Queries to AlphaProof can return a proof, disproof (a proof that the submitted subgoal is false), or a failure message; proofs are directly substituted into the sketch, while disproofs and failure messages are fed into the prover’s prompt. Separately, we developed an evolutionary agent (C), inspired by AlphaEvolve [46], in which prover subagents sample from and contribute to a shared population database of sketches. A challenge here is the mismatch between evolutionary algorithms, which typically assume a graduated fitness landscape, and formal proof evaluation, which is inherently binary. To bridge this gap, we used a pool of rating agents (based on the less expensive Gemini 3.0 Flash) to construct relative rankings of sketches based on their plausibility, clarity, and novelty. We aggregated these rankings into Elo ratings for the sketches and used a sampling procedure based on the P-UCB formula [30, 55] to drive the search. Finally, we combined the AlphaProof and evolution capabilities into a “full-featured” agent (D; see Fig. 2) in which prover subagents can use AlphaProof as well as evolutionary search. We used this agent as the instrument in our exploration of open research problems.

3. Systematic Evaluation on Open Problems Erdős Problems. Bloom maintains an online catalog [8] of over 1200 open problems posed by Paul Erdős and his collaborators. The open-source Formal Conjectures repository [23] contains Lean formalizations of a subset of these problems. We ran Agent (D) on all these formal statements (353 at the time of the run), terminating the search if no proof was found within 3000 episodes. The agent solved 9/353 problems (Table 1 and supplementary text); after each solve, experts on our team validated that the Lean statement faithfully captured the original conjecture. We have publicly shared the proofs, and our results have been logged on Terence Tao’s wiki on AI contributions to Erdős problems [59]. Several proofs require sophisticated constructions and the synthesis of distinct mathematical arguments. For example, problem #12(i), posed by Erdős and Sárközy in 1970 [18], asks if there is an infinite set 𝐴 that satisfies a restrictive divisibility constraint – no element may divide the sum of two larger elements – and which satisfies the density con,𝑁 ] | √ dition lim inf 𝑁 →∞ | 𝐴∩[1 > 0; this problem had received attention in multiple prior works 𝑁 [17, 54, 7]. Our agent constructed 𝐴 as an infinite union of disjoint “blocks” 𝐵𝑖 ⊆ [ 𝑃 𝑖 , 1.1 𝑃 𝑖 ] for a suitably rapidly growing sequence ( 𝑃 𝑖 ). To satisfy the local divisibility conditions, the proof integrates the Chinese Remainder Theorem with the properties of sets that avoid length-3 arithmetic progressions. Problem #125 concerns the sumset 𝐴 + 𝐵, where 𝐴 is the set of non-negative integers whose base-3 representation uses only the digits 0 and 1, and 𝐵 is the analogous set in base 4. The question of whether the lower density of ( 𝐴 + 𝐵) is positive was open since 1996 [12]. Our agent resolved the conjecture by synthesizing an inductive thinning argument that exploits the Diophantine proximity of the two multiplicatively independent bases (3𝑚 ≈ 4𝑘 ). 4

Advancing Mathematics Research with AI-Driven Formal Proof Search

Mathematician Natural Language Context

Domain Knowledge & Proof Libraries

Lean Problem Formalization

AlphaProof Nexus Rater Subagent

Prover Subagent

LLM Critic + Tournaments

LLM (+ AlphaProof) (2) (1)

(5)

Proof Validator

(4)

(3)

Population Database Sketches

Goal Proofs

ELO Scores

Formal Proof

Figure 2 | Design of the full-featured AlphaProof Nexus agent. The mathematician provides as input a Lean theorem with sorry for a proof, and optionally, natural language context and additional domain knowledge encoded in Lean. The agent architecture consists of a basic generation-validation pipeline and an optional evolutionary framework. An LLM-based prover subagent attempts to solve the problem by refining proof sketches (2). The subagent may optionally call AlphaProof as a tool; each invocation of AlphaProof on a goal returns whether a proof or disproof was found, or whether it was unsuccessful in resolving the goal. The sketch produced in the end is checked by a validator to ensure the problem statement was not changed unsafely and the proof compiles. If all goals are successfully proved, the agent outputs the final Lean proof. This basic pipeline can be extended with an evolutionary population database and rating mechanism. In this configuration, validated sketches are admitted into the Population Database (3). Simultaneously, rater subagents sample previous attempts (4), which are then ranked by an LLM critic in matches. The match results are admitted back into the database (5) to update the Elo scores of the sketches. These scores are then used by the evolutionary algorithm to sample prior sketches from the database, constructing an overall prompt – which includes any optional inputs from the mathematician – to condition new episodes (1).

5

Advancing Mathematics Research with AI-Driven Formal Proof Search

The agent also served as a tool for detecting and fixing misformalizations. For example, in Erdős problems #125 and #741(i), the interpretation of “density” in the original informal statements was amended to “lower density” and “upper density” respectively, after our full-featured agent found proofs using density as “natural density.” Following the correction of the ambiguity, the agent was still able to resolve the questions. Failure Analysis. We analyzed the highest-scoring sketches (measured by Elo) across a random sample of problems on which our agent failed. First, the agent frequently offloaded a problem’s core difficulty into a single sorry within a helper lemma that reiterated the target statement in a slightly different form. Explicitly prompting against this behavior failed to prevent it. Second, for several problems, the top sketches relied on lemmas marked with sorry that the agent claimed were established results in the mathematical literature. Upon manual inspection, these lemmas proved to be hallucinations. These failure modes underscore the value of end-to-end formal verification. OEIS. We also applied the agent to systematically explore open problems in the OEIS [56], a massive repository of integer sequences and their known and open properties. We used Gemini to autoformalize 492 open questions from the OEIS and applied the agent to the resulting Lean statements. As a guard against misformalization, the agent was required to prove “test lemmas” verifying the first few terms of each sequence against its formal definition before attempting the target conjectures. The agent found proofs for 44 conjectures that a manual review found to be correctly formalized and previously unproven. Two of the proofs appear in the supplementary material.

4. Deployment in Mathematics Research Optimization Theory. Agent (D) resolved an open question in optimization: proving an exact O (1/𝑡 ) convergence rate for the Anchored Gradient Descent-Ascent (GDA) algorithm for min-max convex-concave optimization, thereby tightening the slower bound established by [52]. The proof departs from continuous-time ordinary differential equations (ODE) analysis used in previous work, instead using a discrete-time recurrence-based approach. The agent did not merely verify a fixed algorithm: we marked the learning schedule as a parameter within an EVOLVE-VALUE block in the input file, allowing the agent to simultaneously search for the schedule and the proof, ultimately discovering a novel parameter choice that yields the stronger guarantee. We previously released a deformalized version of the proof as a preprint [58]. Subsequent work [13] has extended this result. Graph Theory. The graph reconstruction conjecture [61] is one of the oldest open problems in combinatorics. It asserts that every finite simple graph with at least three vertices is determined, up to isomorphism, by the multiset of its vertex-deleted subgraphs, known as its deck. AlphaEvolve [46] experiments helped us formulate two bipartite variants of the graph reconstruction conjecture, along with a proposed full reconstruction algorithm. For one of these variants, our agent produced a complete proof. For the full algorithmic reconstruction statement, the agent generated proof sketches and strategies that helped clarify the structure of the problem and led to simplified reformulations of the conjectures originally suggested by AlphaEvolve. A paper based on the results of this collaboration is currently in preparation.

6

Advancing Mathematics Research with AI-Driven Formal Proof Search

ID

Conjecture Summary

Proof Technique

12 (i)

(1970) Existence of 𝐴 ⊂ ℤ+ s.t. 𝑎 ∤ ( 𝑏 + 𝑐)

Block-based construction via CRT and 3-AP avoiding sets

(1970) Existence of 𝐴 ⊂ ℤ+ s.t. 𝑎 ∤ ( 𝑏 + 𝑐) with | 𝐴 ∩ [1, 𝑁 ] | ≫ 𝑁 1−𝜖 for any 𝜖 and 𝑁 sufficiently large Í Í (1996) { 𝜖𝑘 3𝑘 | 𝜖𝑘 ∈ {0, 1}} + { 𝜖 𝑗 4 𝑗 | 𝜖 𝑗 ∈ {0, 1}} has lower density zero

Block-based construction via CRT and 3-AP avoiding sets

12 (ii) 125 138∗ 152 741 (i) 741 (ii) 846

26∗,†

√ with | 𝐴 ∩ [1, 𝑁 ] |/ 𝑁 > 𝛿 > 0 infinitely often

(1981) Van der Waerden numbers satisfy

𝑊 ( 𝑘+1) − 𝑊 ( 𝑘) → ∞

Inductive thinning via Diophantine approx. 3𝑚 ≈ 4 𝑘 Greedy coloring extension with monochromatic intersection lemma

(1994) Sufficiently large Sidon sets 𝐴 contain many isolated points in 𝐴 + 𝐴

Elementary argument by bounds on interior points, shifted neighbors and quadruples

(1994) Existence of a basis 𝐴 of order 2 with 𝐴1 + 𝐴1 , 𝐴2 + 𝐴2 having bounded gaps for all 𝐴1 , 𝐴2 such that 𝐴 = 𝐴1 ⊔ 𝐴2

Explicit construction via rapidly growing sequence

(1994) If 𝐴 + 𝐴 has upper density, there exists a decomposition 𝐴 = 𝐴1 ⊔ 𝐴2 s.t. 𝐴1 + 𝐴1 , 𝐴2 + 𝐴2 have positive upper density

Bounding of upper density of 𝐴𝑖 + 𝐴𝑖 via cases on upper density of 𝐴

(1992) Existence of infinite set 𝐴 such that any finite subset contains many noncollinear points, but is not a finite union of non-collinear sets

Label 𝐾∞ vertices with terms from fastgrowing sequence, apply map on edges { 𝑖, 𝑗 } ↦→ ( 𝑥 𝑖 + 𝑥 𝑗 , 𝑥 𝑖2 + 𝑥 𝑖 𝑥 𝑗 + 𝑥 2𝑗 ) to obtain

(1995) Existence of 𝐴 such that upper density of 𝐴 + 𝑘 is < 1 − 41 for all naturals 𝑘

Block-based construction using increasing sequence of primes, CRT, and bounding u. density by cases

𝐴

Table 1 | Open problems from the ErdosProblems repository autonomously resolved by our full-featured agent. The asterisk indicates a variant of the main problem with this number. Problem #26 (annotated with †) is a more general variant of a question posed by Erdős, but was not posed by Erdős himself. Separately, the agent proved an open graph theory conjecture regarding a bound on the maximum number of leaves over all spanning trees of a graph 𝐺 , relating it to the maximum number, over all vertices 𝑣 ∈ 𝐺 , of independent sets in the neighborhood of 𝑣. The problem was posed by Graffiti [19], an automated conjecturing system, in 1996, and points to an interesting future opportunity to close the loop between AI-based conjecturing and proof. Algebraic Geometry. We evaluated our full-featured agent on eight algebraic geometry problems, from textbook-style exercises to open research questions on Hilbert functions, solving two of the four open problems. One of these problems had been a well-known open question for approximately fifteen years. This problem concerned pure 𝑂-sequences, equivalently the Hilbert functions of monomial Artinian level algebras [57]. Their shape and positivity properties have been studied intensively in recent years [9]. Although logconcavity fails for broad families of pure 𝑂-sequences, the case of codimension 3 and type 2 was identified as the principal remaining open case [68]. The agent’s proof establishes log-concavity in this case; the argument is substantial, using a nontrivial reformulation of the Hilbert function and a detailed case analysis of the resulting second-difference inequalities. 7

Advancing Mathematics Research with AI-Driven Formal Proof Search

Additive Combinatorics. Our agent helped resolve problem #57 from Green’s well-known list of open conjectures [27]. The problem asks whether two specific quadratically structured function spaces coincide. The functions of interest map elements of an Abelian group 𝐺 to the complex numbers. Here, our agent autonomously solved a variant of the problem in which the functions are real-valued, but a personal communication from Green clarified that the complex-valued case was the intended challenge. While the agent could not immediately prove the intended version of the problem, numerical heuristics using floating-point arithmetic provided a candidate counterexample (the cyclic group ℤ/3ℤ and a specific separating functional). We formalized the problem of whether this counterexample disproves the correct conjecture, and the agent autonomously proved that it indeed does. A paper on the result is in the works [22]. Quantum Optics. With Mario Krenn, we investigated a set of quantum optics problems concerning the existence of monochromatic quantum graphs with 𝑁 vertices and 𝑑 colors drawn from domains such as the reals, the complex numbers, and {−1, 0, 1}. These constructions correspond to 𝑁 -particle quantum states with local Hilbert space dimension 𝑑 – in particular, high-dimensional Greenberger–Horne–Zeilinger (GHZ) states realizable via linear optics [39]. Our agent resolved multiple conjectures of this form, in particular with 𝑁 = 𝑑 ∈ {4, 6, 10}. A paper on these results is in preparation [38].

5. Impact of Agent Architecture and Model Exploration of a large space of open problems is expensive, and we chose the full-featured agent (agent (D)) for this based on its strong performance on competition benchmarks. To understand which architectural components are necessary for its successes, we compared its performance against agents (A), (B), and (C) on the Erdős problem set in Table 1. We compared the agents by analyzing the solve rate against the cost (in US dollars) per successfully proven problem. We report computational cost in USD because it directly measures the barrier to reproducing this work and provides a natural common currency for comparing agents that allocate compute differently (e.g., agent (D) uses Gemini 3.0 Flash for rater subagents and Gemini 3.1 Pro for provers). We do not intend USD as a comparison of AI and human mathematical labor. For agents (C) and (D), in which a single proof attempt requires 10 subagents, we executed 10 attempts per problem. In contrast, for the basic Agent (A) and its AlphaProof-equipped extension (B), we ran 100 independent attempts, each with a single subagent. Because (A) and (B) consist of independent subagents, we simulated scenarios where they have 𝐾 subagents by grouping the attempts into chunks of size 100/ 𝐾 ; a chunk was considered successful if any attempt included in the chunk proved the statement. The overall solve rate was defined to be the fraction of successful chunks. To calculate the monetary cost for these successful chunks, we identified the earliest timestamp 𝑇 of a successful attempt and summed the costs of all attempts within that chunk up to 𝑇 . Since agents (C) and (D) are more expensive, we used the independent attempts to obtain a single point estimate. Fig. 3 compares the agents across six Erdős problems (results for the rest are in the supplementary material). Agents (A) and (B) perform similarly – within the margin of error 8

Advancing Mathematics Research with AI-Driven Formal Proof Search

(A) basic

erdos_12(i) 1.0

6

Solve Rate

0.8

6

10

10

1

0.6 11

0.2 0.0

100

300

400

Mean Cost, USD 1

1.0

500

erdos_138 6

600 1010

6

3

0.8

Solve Rate

200

0.6 1

100

150

200

250

Mean Cost, USD

300

350

erdos_125 1

1.0

1

0.6

1

0.4

0.4

0.2

0.2

0.0

50 100 150 200 250 300 350 400

0.0

Mean Cost, USD

1

1

11

0

3 3

200

1.0

0.0

3

1.0 10 6 3 11

10

10

6

400

600

erdos_26 361

10 6

101

0.6

3 1

0.4 0.2

1

200

10

1 1

0.8

6

6

Mean Cost, USD

erdos_152

0.2 50

10 1

6

(D) full

0.8

0.4

0.2 0.0

10 3

3

0.6

1 1

erdos_12(ii)

0.8

3

0.4

(C) basic w/ evolution

0.8 0.6

0.4

6

1.0 1

33

(B) basic w/ AP

400

600

Mean Cost, USD

800

1000

0.0

50

100

150

Mean Cost, USD

200

250

Figure 3 | Solve rate versus mean inference cost (USD) across six Erdős problem instances. The solve rates are evaluated for the four agents: (A) basic (blue circles), (B) basic with AlphaProof (orange squares), (C) basic with evolution (green diamonds), and (D) full-featured (red triangles). Numeric annotations denote the number of independent attempts 𝐾 ∈ {1, 3, 6, 10} grouped together; error bars indicate one standard error interval. Due to their higher costs, agents (C) and (D) lack variance estimates, as independent attempts were used to obtain a single point estimate (see main text for details). For agents (A) and (B), each curve traces the cost–performance Pareto frontier as 𝐾 increases, revealing diminishing marginal returns at higher budgets. Agent (B) generally matches or exceeds the solve rate of the basic configuration at comparable cost. Costs reported for (B) and (D) do not include the inference cost of AlphaProof. While for most problems configuration (A) or (B) is the best, for some challenging problems like Erdős #125, the full-featured configuration (D) performs significantly better. Note that accounting for the estimated AlphaProof cost of 60 USD does not change the above outcomes beyond the margin of error.

9

Advancing Mathematics Research with AI-Driven Formal Proof Search

– on four of the problems, though agent (B) is more efficient on problems 12(ii) and 125. Agent (D) outperforms (A) and (B) on problems 138 and 125, offering significant monetary savings (2x to 5x), but is roughly half as cost-efficient on the remaining problems. We also compared agents (A), (B), and (D) on the wall-clock time needed to solve the problems. The results broadly followed the inference cost trends, with (B) offering savings over (A) in several of the problems, and (D) substantially outperforming both (A) and (B) on problems 138 and 125. Finally, we evaluated AlphaProof in standalone tree-search mode and versions of agent (A) based on smaller models (Gemini 3.0 Flash, Gemini 3.1 Flash-Lite). These systems could not solve any of the problems. Cost and Variance. Per-problem inference costs exhibit high variance due to the stochastic nature of our agents. The reported costs also do not capture the full cost of discovery: we applied the full-featured agent to all 353 Erdős problems in Formal Conjectures, and identifying tractable problems was itself a significant computational investment. AlphaProof cost approximately 27.5 TPU hours ($60 USD) per problem on v6e TPUs.

6. Discussion We have provided a large-scale demonstration of the value of formal proof search agents on research-level mathematical problems. Recently, some natural-language reasoning systems have been shown to succeed in research-level mathematical tasks, including Erdős problems [20, 4]. However, the use of AI-generated informal proofs, either as standalone products or as inputs to a subsequent formalization stage, requires careful validation by human experts. Formal verification can serve as a filter for determining which proofs merit human review. The effectiveness of our basic agent in our post-hoc analysis was surprising. At the time we were planning our large-scale exploration, simpler agentic loops did not show strong performance on competition-level benchmarks, and this informed our decision to use the full-featured agent. The LLM landscape has since shifted substantially. We attribute the basic agent’s success to both this shift and the power of compiler feedback in grounding LLM reasoning. The full-featured agent retains an advantage on the hardest problems for now. However, as LLM capabilities grow, this advantage may diminish. At present, our agents’ successes are concentrated in areas such as combinatorics, convex optimization, and number theory, where Lean’s mathematics library [60] is mature and tasks often decompose into tractable subgoals. Even most Erdős problems remain out of reach, let alone problems that require extensive new theory. Additionally, our agents inherit the biases of their underlying LLMs and exhibit high search variance. Characterizing the agents’ boundaries and expanding them is an important direction for future work. We built AlphaProof Nexus with the belief that the future of mathematics lies in humanmachine partnership, where interactive AI tools serve to expand a mathematician’s creative capacity. Our results support this vision. Our mathematician collaborators found that proof attempts by our agents enhanced their understanding of a problem, even when an agent could not prove the claim at hand. Because the sketches were formal, experts could focus on the unresolved subgoals rather than re-verifying the entire argument. Moreover, the 10

Advancing Mathematics Research with AI-Driven Formal Proof Search

agents were powerful tools for detecting misformalizations. These experiences suggest that AI-driven formal proof search can serve not only to solve problems but to deepen human understanding.

References [1] Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: IMO-level automated theorem proving. arXiv preprint arXiv:2510.01346, 2025. [2] Boris Alexeev, Kevin Barreto, Yanyang Li, Jared Duker Lichtman, Liam Price, Jibran Iqbal Shah, Quanyu Tang, and Terence Tao. Primitive sets and von mangoldt chains: Erdős problem #1196 and beyond, 2026. [3] Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, and Gregory Valiant. Short proofs in combinatorics and number theory. arXiv preprint arXiv:2603.29961, 2026. [4] Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, and Gregory Valiant. Short proofs in combinatorics, probability and number theory ii. arXiv preprint arXiv:2604.06609, 2026. [5] Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4, 2025. [6] Axiom. AXLE: Axiom lean engine, 2025. Accessed: 2025. [7] Stephan Baier. A note on p-sets. 2004. [8] Thomas Bloom. Erdosproblems.com. https://www.erdosproblems.com, 2026. [9] Mats Boij, Juan C. Migliore, Rosa M. Miró-Roig, Uwe Nagel, and Fabrizio Zanello. On the Shape of a Pure O-Sequence, volume 218 of Memoirs of the American Mathematical Society. American Mathematical Society, Providence, RI, 2012. [10] J. A. Bondy and R. L. Hemminger. Graph reconstruction–a survey. Journal of Graph Theory, 1(3):227–268, 1977. [11] Jim Bryan, Balázs Elek, Freddie Manners, George Salafatinos, and Ravi Vakil. The motivic class of the space of genus 0 maps to the flag variety. arXiv preprint arXiv:2601.07222, 2026. [12] S. A. Burr, P. Erdős, R. L. Graham, and W. Wen-Ching Li. Complete sequences of sets of integer powers. Acta Arithmetica, 77(2):133–138, 1996. [13] Yang Cai and Weiqiang Zheng. Last-iterate convergence of anchored gradient descent. arXiv preprint arXiv:2604.12235, 2026. 11

Advancing Mathematics Research with AI-Driven Formal Proof Search

[14] François Caron and Arnaud Doucet. Efficient Bayesian inference for generalized Bradley–Terry models. Journal of Computational and Graphical Statistics, 21(1):174– 196, 2012. [15] Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, et al. Seed-prover 1.5: Mastering undergraduate-level theorem proving via learning from experience. arXiv preprint arXiv:2512.17260, 2025. [16] DeepSeek-AI. Deepseek-v2: A strong, economical, and efficient mixture-of-experts language model, 2024. [17] Christian Elsholtz and Stefan Planitzer. On erdős and sárközy’s sequences with property p. arXiv preprint arXiv:1609.07935, 2016. [18] Paul Erdős and Alice Sárközi. On the divisibility properties of sequences of integers. Proceedings of The London Mathematical Society, pages 97–101, 1970. [19] Siemion Fajtlowicz. On conjectures of graffiti. In J. Akiyama, Y. Egawa, and H. Enomoto, editors, Graph Theory and Applications, volume 38 of Annals of Discrete Mathematics, pages 113–118. Elsevier, 1988. [20] Tony Feng, Junehyuk Jung, Sang-hyun Kim, Carlo Pagano, Sergei Gukov, ChiangChiang Tsai, David Woodruff, Adel Javanmard, Aryan Mokhtari, Dawsen Hwang, et al. Aletheia tackles firstproof autonomously. arXiv preprint arXiv:2602.21201, 2026. [21] Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao Lin, Evan Zheran Liu, Nigamaa Nayakanti, Xiaomeng Yang, Heng-Tze Cheng, Demis Hassabis, Koray Kavukcuoglu, Quoc V. Le, and Thang Luong. Towards autonomous mathematics research. arXiv preprint 2602.10177, 2026. [22] Moritz Firsching and Bogdan Georgiev. A strict separation between two notions of quadratically structured functions. In preparation, 2026. [23] Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, and Pushmeet Kohli. Formal conjectures: An open and evolving benchmark for verified discovery in mathematics, 2026. [24] GasStationManager. Safeverify. https://github.com/GasStationManager/Saf eVerify, 2025. [Accessed: 2026-05-12]. [25] Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, and Adam Zsolt Wagner. Mathematical exploration and discovery at scale. arXiv preprint arXiv:2511.02864, 2025. [26] Google DeepMind. Gemini 3.1 deep think, 2026. Accessed: 2026-04-30. [27] Ben Green. 100 open problems. https://people.maths.ox.ac.uk/greenbj/papers/openproblems.pdf, 2024. 12

Advancing Mathematics Research with AI-Driven Formal Proof Search

[28] Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, and Maryna Viazovska. A milestone in formalization: The sphere packing problem in dimension 8. arXiv preprint arXiv:2604.23468, 2026. [29] Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salvatore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Velingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli, and David Silver. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, pages 1–3, 2025. [30] Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Mohammadamin Barekatain, Simon Schmitt, and David Silver. Learning and planning in complex action spaces. In International Conference on Machine Learning, 2021. [31] Geoffrey Huntley. Ralph wiggum as a "software engineer". https://ghuntley.com /ralph, 2025. Blog post. [32] Vishesh Jain and Clayton Mizgerd. Equality in fill’s spectral gap problem. arXiv preprint arXiv:2604.03937, 2026. [33] Uijeong Jang and Ernest K Ryu. Point convergence of nesterov’s accelerated gradient method: An ai-assisted proof. arXiv preprint arXiv:2510.23513, 2025. [34] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022. [35] Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35:8360–8373, 2022. [36] Paul J. Kelly. A congruence theorem for trees. Pacific Journal of Mathematics, 7(1):961– 968, 1957. [37] John R. Koza. Genetic programming as a means for programming computers by natural selection. Statistics and Computing, 4(2):87–112, 1994. [38] Mario Krenn, Moritz Firsching, George Tsoukalas, Rishikesh Gajjala, Xuemei Gu, and Swarat Chaudhuri. A Tensor-Algebraic No-Go Theorem for High-Dimensional Photonic GHZ States. In preparation, 2026. [39] Mario Krenn, Xuemei Gu, and Anton Zeilinger. Quantum experiments and graphs: Multiparty states as coherent superpositions of perfect matchings. Physical Review Letters, 119(24), December 2017. 13

Advancing Mathematics Research with AI-Driven Formal Proof Search

[40] Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613, 2025. [41] R.D. Luce. Individual Choice Behavior: A Theoretical Analysis. Wiley, 1959. [42] Math Inc. Gauss: An agent for autoformalization, 2026. Accessed: 2026. [43] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625–635. Springer, 2021. [44] Ansh Nagda, Prabhakar Raghavan, and Abhradeep Thakurta. Reinforced generation of combinatorial structures: Hardness of approximation. arXiv preprint arXiv:2509.18057, 2025. [45] Ansh Nagda, Prabhakar Raghavan, and Abhradeep Thakurta. Reinforced generation of combinatorial structures: Ramsey numbers. arXiv preprint arXiv:2603.09172, 2026. [46] Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. Alphaevolve: A coding agent for scientific and algorithmic discovery. arXiv preprint 2506.13131, 2025. [47] R. L. Plackett. The analysis of permutations. Journal of the Royal Statistical Society. Series C (Applied Statistics), 24(2):193–202, 1975. [48] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. [49] Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. On infinite sets with no 3 on a line. arXiv preprint arXiv:2602.21275, 2026. [50] Christian Reiher, Vojtěch Rödl, and Marcelo Sales. Colouring versus density in integers and hales–jewett cubes. Journal of the London Mathematical Society, 110(5):e12987, 2024. [51] Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models. Nature, 625(7995):468– 475, 2024. [52] Ernest K. Ryu, Kun Yuan, and Wotao Yin. Ode analysis of stochastic gradient methods with optimism and anchoring for minimax problems. arXiv preprint arXiv:1905.10899, 2019.

14

Advancing Mathematics Research with AI-Driven Formal Proof Search

[53] Johannes Schmitt. Extremal descendant integrals on moduli spaces of curves: An inequality discovered and proved in collaboration with ai. arXiv preprint arXiv:2512.14575, 2025. [54] Tomasz Schoen. On a problem of erdős and sárközy. Journal of Combinatorial Theory, Series A, 94(1):191–195, 2001. [55] David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play, 2018. [56] Neil J. Sloane. The on-line encyclopedia of integer sequences. In Proceedings of the 14th Symposium on Towards Mechanized Mathematical Assistants: 6th International Conference, Calculemus ’07 / MKM ’07, page 130, Berlin, Heidelberg, 2007. SpringerVerlag. [57] Richard P. Stanley. Hilbert functions of graded algebras. Advances in Mathematics, 28(1):57–83, 1978. [58] Anja Surina, Arun Suggala, George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Francisco JR Ruiz, Pushmeet Kohli, and Swarat Chaudhuri. An improved last-iterate convergence rate for anchored gradient descent ascent. arXiv preprint arXiv:2604.03782, 2026. [59] Terence Tao and contributors. Ai contributions to Erdős problems. https://github

.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-p roblems, 2026. Accessed: 2026-04-23. [60] The Mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, 2020. ACM. [61] Stanislaw M. Ulam. A collection of mathematical problems. New York and London: Interscience Publishers, 1960. [62] Stanislaw M. Ulam. A Collection of Mathematical Problems, volume 8 of Interscience Tracts in Pure and Applied Mathematics. Interscience Publishers, New York, 1960. [63] Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. Hilbert: Recursively building formal proofs with informal reasoning. arXiv preprint arXiv:2509.22819, 2025. [64] Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025. [65] David P Woodruff, Vincent Cohen-Addad, Lalit Jain, Jieming Mao, Song Zuo, MohammadHossein Bateni, Simina Branzei, Michael P Brenner, Lin Chen, Ying Feng, et al. 15

Advancing Mathematics Research with AI-Driven Formal Proof Search

Accelerating scientific research with gemini: Case studies and common techniques. arXiv preprint arXiv:2602.03837, 2026. [66] Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint 2412.16075, 2024. [67] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36:21573–21612, 2023. [68] Fabrizio Zanello. Log-concavity of level Hilbert functions and pure o-sequences. Journal of Commutative Algebra, 16(2):245–256, 2024. [69] Daniel Zheng, Ingrid von Glehn, Yori Zwols, Iuliya Beloshapka, Lars Buesing, Daniel M. Roy, Martin Wattenberg, Bogdan Georgiev, Tatiana Schmidt, Andrew Cowie, Fernanda Viegas, Dimitri Kanevsky, Vineet Kahlon, Hartmut Maennel, Sophia Alj, George Holland, Alex Davies, and Pushmeet Kohli. AI Co-Mathematician: Accelerating mathematicians with agentic AI. arXiv preprint 2605.06651, 2026.

Acknowledgments We thank Emilien Dupont, Dan Roy, and Daniel Zheng for their careful feedback on the paper, Alexander Novikov for help with LLM infrastructure, Katerina Hristova for help with Lean formalization, and Sebastian Nowozin and Taylan Cemgil for their guidance on designing an Elo scoring mechanism for proof sketches. Author contributions: SC, SS, and GT conceptualized and implemented the first version of AlphaProof Nexus. AK led the engineering and infrastructure decisions. AK, SS, GT, and A.Surina developed the final version of AlphaProof Nexus with inputs from FJR, AF, and SC. AK and SS maintained the underlying infrastructure of AlphaProof Nexus. GT initiated and led the use of the system in mathematics research tasks. AK, SS, GT, A.Surina, LY, and SC coordinated the large-scale runs on open research problems. GT, MF, GB, A.Suggala and AZW identified problems to solve and validated the generated solutions. GB, in particular, was the first research mathematician to use AlphaProof Nexus. MF, GT, A.Surina, FJR, HM, SC, and EW contributed to Lean formalizations of problems. SS led the systematic evaluation of our agents, with additional contributions from AK, MZH and AH. SC, SS, GT, FJR, and A.Surina wrote the paper with inputs from MF, AZW, HM, and AF. SS, AF, and EW created the figures with inputs from SC, GT, A.Surina and FJR. GB, AZW, MF, GT, A.Surina and CG wrote the natural language proofs, with HM providing agent-generated drafts to facilitate the writing process. MZH and EW assisted with Lean setup and integration with AlphaProof. AF coordinated the creation of the accompanying Github repository. MB and TH provided technical advice throughout the project. SC led the overall effort, with PK providing sponsorship and technical and strategic direction.

16

Advancing Mathematics Research with AI-Driven Formal Proof Search

Competing interests:

There are no competing interests to declare.

Data and materials availability: All Lean proofs are available in the accompanying repository https://www.github.com/google-deepmind/alphaproof-nexus-results. Natural language proofs of some key results are provided in the repository and the supplementary text.

17

Advancing Mathematics Research with AI-Driven Formal Proof Search

A. Materials and Methods A.1. Further Details on AlphaProof Nexus Agents

1 2 3

# Main Loop initial_sketch = lean_compiler.check(initial_file) final_sketch = prover_subagent(initial_sketch)

4 5 6 7 8 9 10 11

# Basic prover subagent def prover_step(sketch): session = LlmSketcher(sketch) # Start an LLM session while tool_call := session.recv(): if tool_call.is_search_replace(): sketch, feedback = search_replace_then_compile(sketch, tool_call) session.send(feedback)

12 13 14

if lean_compiler.verify_integrity(sketch): # Check for hacks return sketch

15 16 17 18 19 20 21

def prover_subagent(initial_sketch): sketch = initial_sketch while within_budget() and sketch.contains_sorry(): if new_sketch := prover_step(sketch): sketch = new_sketch return sketch

Figure 4 | Pseudocode for the basic agent (A). A prover subagent executes a sequence of steps in a loop. Each step is a conversation with a LLM instance (Gemini 3.1 Pro). During this conversation, the subagent can view a Lean file and apply search-replace edits. After each change, the Lean compiler provides feedback, such as compilation errors. As for agent (D), we check for the integrity of the final sketch once the conversation is over. 𝑁 subagents run independently in parallel and stop as soon as one of them found a valid proof. Basic Agent. The pseudocode for the basic agent (A) is shown in Figure 4. The agent operates 𝑁 independent subagents that share no state. All subagents start with the same initial proof sketch. As soon as one subagent finds a proof, all others are terminated. Each subagent implements a Ralph loop [31] consisting of a sequence of episodes. The full prompt is shown in Figure 8. Within each episode, the subagent runs a multi-turn session with an access to a search_replace tool. After each edit, the Lean code is compiled and compiler feedback is passed back to the model. When the subagent ends an episode, the code is validated using SafeVerify [24], 2which checks the proof against the theorem specification and guards against environment exploits (e.g., axiom injection). If validation succeeds and the proof is sorry-free, the proof is returned. If sorry remains, the subagent summarizes lessons learned in a comment and begins the next episode from the current sketch. If validation fails, the subagent reverts to the previous sketch. Full-featured Agent. The pseudocode for the full-featured agent (D) is shown in Figure 5. The evolutionary process is orchestrated by a controller, which executes a continuous, 18

Advancing Mathematics Research with AI-Driven Formal Proof Search

1 2 3 4 5 6

# Main Loop initial_sketch = lean_compiler.check(initial_file) population.initialize(initial_sketch) launch prover_subagents(N, population) # Create prover agents launch rater_subagents(M, population) # Create rater agents await population.contains_sorry_free_proof()

7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

# Prover subagent, run asynchronously def prover_step(sketch): session = LlmSketcher(sketch) # Start an LLM session while tool_call := session.recv(): if tool_call.is_alphaproof(): # Call AlphaProof proofs = [alphaproof.solve(g) for g in unsolved_goals(sketch)] sketch, feedback = incorporate_proofs(proofs, sketch) elif tool_call.is_search_replace(): # Call search-and-replace sketch, feedback = search_replace_then_compile(sketch, tool_call) session.send(feedback) if lean_compiler.verify_integrity(sketch): # Check for hacks population.add(sketch) return not sketch.contains_sorry() return False

22 23 24 25 26 27

def prover_subagent(): while within_budget(): sketch = population.sample(strategy=p_ucb) # Sample a sketch if prover_step(sketch): break

28 29 30 31 32 33

# Rater agent, run asynchronously def rater_subagent(): s1, ..., sP = sketch_db.get_sketches_for_ranking() ranks = llm_rater.rank(s1, ..., sP) sketch_db.update_elo(ranks)

Figure | Pseudocode the main components ofloop thecreates full-featured agent (Agent (D)). Figure 1:5 Pseudocode for for ’s main components. The main a pool of asynchronous sketchers The main and loopawaits creates a pool of prover and raters and awaits the and raters the creation of asynchronous a full (sorry-free) proof. subagents Each prover subagent samples a parent sketch from the population using the P-UCB strategy and creates a stateful conversation session with an creation of a full (sorry-free) proof. At each step, a prover subagent uses the P-UCB strategy LLM (Gemini 3.1 Pro) instance. In this conversation, it receives instructions to perform tool calls from the to sample a parent sketch from the population and initiates a stateful conversation with LLM. Tools include and a structured search-and-replace operation. The results of the tool call are used as acontext LLM for instance (Gemini 3.1 Pro). The agent has access to two tools: AlphaProof and a the next turn. After the conversation concludes, the sketch is added to the population only if it structured The Each results of these toolsamples calls provide contextuses for compiles andsearch-and-replace the original theorem isoperation. uncompromised. rater subagent a set of sketches, the subsequent turn.and Once the the conversation concludes, resulting sketch is added to the an LLM to rank them, updates Elo scores used by P-UCBthe sampling. population only if it compiles successfully and the original theorem remains uncompromised. Concurrently, each rater_agent samples 𝑃 sketches, uses a LLM (Gemini 3.0 Flash) to determine which is the most promising, and updates the Elo scores used for P-UCB sampling. We set 𝑃 = 7 in all the experiments. 1

19

Advancing Mathematics Research with AI-Driven Formal Proof Search

asynchronous loop. At each step, the controller performs the following stages: 1. Database sampling: The controller selects a root proof sketch 𝑆root by sampling from the database, along with 𝑀 = 2 auxiliary inspiration sketches 𝑆insp . The selection strategy balances exploitation of high-rated sketches with exploration of diverse candidates (see “Population Database and Matchmaking”). 2. Prompt construction: A prompt X is assembled to guide the LLM. It integrates the formal problem specification, the Lean source code and natural language plan of 𝑆root , and structured feedback derived from AlphaProof’s previous attempts on {𝑆insp }. As in AlphaEvolve, the controller encourages diversity by stochastically injecting instructions such as “decompose unsolved goals,” “combine ideas from prior attempts,” or “try a completely new approach.” 3. Prover subagent: The assembled prompt X is dispatched to the LLM (Gemini 3.1 Pro), initiating a multi-turn episode. To scale to large Lean files, the subagent outputs mutations via a search_replace tool in a compact diff format rather than rewriting the entire file. The subagent can also query AlphaProof to test specific subgoals midepisode; the feedback indicates whether the goal was proven, disproven, or unresolved. To manage compute, each episode is restricted to a maximum of 5 AlphaProof queries and 90 search-and-replace edits. At the conclusion of the episode, the generated sketch undergoes a sandbox check that permits sorry placeholders but verifies that the original target theorem statement was not altered. 4. Validation: Once the candidate sketch 𝑆′ passes the sandbox check, it undergoes formal validation. The system extracts all remaining sorry subgoals and cross-references them against a global goal cache using a deep hash of their exact Lean state (see “Global Goal Caching”). If a subgoal was previously resolved, the proof is retrieved immediately; otherwise, it is dispatched to AlphaProof. If AlphaProof closes all remaining goals, the fully assembled, sorry-free proof is passed to SafeVerify [24] for final validation, ensuring the proof compiles and that no disallowed axioms (including sorryAx) were introduced. If any subgoals remain unresolved, 𝑆′ is registered with its remaining sorry placeholders. 5. Database registration: The candidate 𝑆′, along with per-subgoal feedback from AlphaProof, is registered in the database. Its fitness is then determined asynchronously via Elo matchmaking. AlphaProof has a Test-Time Reinforcement Learning (TTRL) mode in which it learns to solve a problem by solving its AI-generated variants at inference time; however, we prioritize the use of compute for LLM inference and run AlphaProof in its low-compute tree search inference mode. Population Database and Matchmaking. Unlike systems where numerical fitness can be directly computed (e.g., empirical runtime), formal proof evaluation yields only discrete signals: whether the code compiles and whether the proof is complete. Agent (D) overcomes this by decoupling generation from fitness assignment, using LLM-based relative review to evaluate the promise of incomplete sketches. 20

Advancing Mathematics Research with AI-Driven Formal Proof Search

Elo-based Rating. Asynchronous rater agents (Gemini 3.0 Flash) continuously sample sets of 𝑃 = 7 sketches from the database for pairwise “matches.” We found 𝑃 = 7 to provide a good trade-off between information per LLM call and input context size. Each rater produces a relative ranking by evaluating the clarity of the proof strategy, the plausibility of remaining goals, and the mathematical novelty of the approach. We model match outcomes using a Plackett-Luce distribution [47, 41], in which each sketch 𝑠 has a latent strength parameter 𝜆 𝑠 . We place a hierarchical prior 𝑝 ( 𝜆 𝑠 | 𝑟𝑠 ) = Gamma(1, 𝑟𝑠 ) with rate parameter 𝑟𝑠 distributed as 𝑝 ( 𝑟𝑠 ) = Gamma(1, 1). This distribution has heavier tails than a simple Gamma over 𝜆 𝑠 while keeping the distributions conditionally conjugate; we expect the choice of hyperparameters to have a relatively small impact. We infer sketches’ posterior strengths using a Gibbs sampling procedure [14]. For each sketch 𝑠, we draw 𝐼 Gibbs samples { 𝜆 𝑠( 𝑖) } 𝑖𝐼=1 from the posterior distribution of that sketch’s strength parameter, obtained after drawing 𝐵 burn-in samples (we set 𝐼 = 1000 and 𝐵 = 200 based on an experiment with synthetic data). We then use the posterior sample mean Í 𝜆 mean = 1𝐼 𝑖 𝜆 𝑠( 𝑖) to obtain the sketch’s Elo score as 𝑠 Elo𝑠 = 1200 + 400 log10 𝜆 mean . 𝑠 To obtain the set of 𝑃 sketches for each match, we use a Thompson sampling strategy that repeatedly takes an independent sample 𝜆 𝑠 for each sketch and chooses the sketch with the highest value. In practice, we obtain the independent samples via Gibbs sampling, retaining only every 25-th sample in order to mitigate in-chain correlation. This is sampling with replacement, so the same sketch may appear more than once. After sampling exactly 𝑃 times, we remove duplicate sketches from the chosen set, replacing them with the sketches with the highest posterior sample variance 𝜆 var 𝑠 . Occasionally the LLM raters may output ties between the input sketches. Since the Plackett-Luce model does not consider ties, we break ties randomly by sampling from the model. Evolutionary Selection. During the sampling phase, the controller selects “parent” sketches using the Predictor + Upper Confidence Bound (P-UCB) formula. To focus the search and reduce computational overhead, the sampler first filters the population to the top 64 highestscoring sketches based on their current Elo ratings. For these top candidates, the Elo ratings are normalized to a range of [0, 1] to yield a base score 𝑞. The final P-UCB score for each sketch is then computed as: √︁Í 𝑉𝑖 score = 𝑞 + 𝑐 𝑣+1 Í where 𝑣 is the number of times the specific sketch has been visited (sampled), 𝑉𝑖 is the total number of visits across the filtered population, and 𝑐 is a tunable exploration constant (set at 0.2 for this work). This mechanism prioritizes the exploitation of the most promising sketches – those within the elite top-64 threshold – while the UCB exploration bonus ensures adequate exploration of newly promoted or infrequently sampled candidates within that elite tier, preventing the search from collapsing into a single, suboptimal lineage. The values 𝑐 = 0.2 and top-64 were chosen empirically based on observed performance. 21

Advancing Mathematics Research with AI-Driven Formal Proof Search

Global Goal Caching and Incorporation. Independent proving agents can generate the same goals to dispatch to AlphaProof. For efficiency, Agent (D) implements a global goal cache within the database. When a sketch is parsed, the system computes a deep hash of the exact formal Lean context and target for every generated subgoal (the goal_id). Before querying AlphaProof, the validator checks this cache. If a specific subgoal’s state was already proved or formally disproved in any prior sketch across the population, the result – along with the specific tactic sequence or value function – is retrieved and incorporated into the current sketch. Novel subgoals are batched and dispatched concurrently to AlphaProof via non-blocking remote procedure calls (RPCs), and their subsequent results are cached to accelerate future generations. AlphaProof Budget. When a novel subgoal is evaluated, AlphaProof executes a formal tree search to discover a proof or disproof. To prevent the system from stalling on intractable or hallucinated goals, AlphaProof operates under a strict computational budget, typically restricted to 400 simulations and bounded by a hard RPC timeout. We compile AlphaProof’s response into textual feedback in case it cannot solve a subgoal. This feedback is then associated with this particular subgoal and rendered in the corresponding prompt sketches. Implementation. The entire AlphaProof Nexus infrastructure is implemented in Python, utilizing the asyncio framework. The evolutionary controller in Agent (D) runs an event loop that distributes work across asynchronous threads for generation, validation, and Elo rating. Formal validation and compilation are executed inside isolated sandboxes (Docker instances) running Lean v4.27 and Pantograph [5]. This ensures that generated code is type-checked in a secure, stateful environment without risking execution of malicious code. The LLM backend leverages an ensemble of models: Gemini 3.1 Pro is used for the complex reasoning required in the multi-turn proving agent, while the faster Gemini 3.0 Flash is deployed for high-throughput match rating and evaluation synthesis. A.2. Prompts Figure 6 shows the main pieces of the prompt used for prover subagents in the full-featured agent (D). Figure 7 shows the prompt for the rating subagents in the full-featured agent (D). Figure 8 shows the full prompt for the basic agent (A).

B. Supplementary Text B.1. Related Work Formal Theorem Proving with LLMs. There is a large literature on neural-network-guided search over machine-checkable formal proofs [66, 15, 16, 64, 40]. Early work such as GPT- 𝑓 [48] established the viability of language models in this setting; subsequent systems improved tactic generation, premise selection, and interaction with external provers [35, 67]. The Draft-Sketch-Prove system [34] introduced the hierarchical approach of generating informal sketches before translating them into formal steps, and recent systems such as Hilbert [63] and Aristotle [1] further separate high-level proof planning from low-level elaboration. AlphaProof [29] first showed that reinforcement learning (RL) could elevate formal theorem-proving to the Math Olympiad level. Some of the successes of that system 22

Advancing Mathematics Research with AI-Driven Formal Proof Search

# 1. Role and Goal You are a world-class mathematician and Lean 4 expert. Your goal is to solve hard mathematical problems by devising a proof strategy and translating it into a Lean 4 proof. You have access to an automated prover, AlphaProof, as a tool to fill in mathematically straightforward steps. # 2. Your Task You will be given Lean code containing theorem statements with proof sketches (the ‘Current Plan‘). Your task is to carefully analyze the ‘Current Plan‘ and ‘Prior Attempts‘ to understand what approaches have been tried and where they failed. [...] Think like a mathematician: focus on the key insights, proof structure, and creative steps. Even for steps that seem mathematically straightforward, you should decompose the proof into simple, manageable subgoals for AlphaProof to solve [...] Some of these problems are very hard, possibly even open problems in mathematics. But don’t be discouraged -- approach them with curiosity and persistence. [...] CRITICAL: You have a large number of ‘search_replace‘ and ‘attempt_goals_with_alphaproof‘ calls available in each episode | you MUST use them exhaustively [...] CRITICAL: You MUST NOT use a single ‘sorry‘ to prove a goal that covers multiple reasoning steps. [...] # 3. Sketch Structure and Syntax * **Only Edit Inside Evolve Markers**: [...] * **AlphaProof Tool**: You have access to a powerful automated theorem prover, AlphaProof, via the ‘attempt_goals_with_alphaproof‘ tool. You MUST use this tool frequently [...] * **One Step Per Line**: [...] * **Reducing Context:** [...] Before calling ‘sorry‘, remove irrelevant hypotheses [...] * **Soundness:** [...] **Do NOT assert falsehoods.** * **No Imports:** [...] * **Helper Definitions:** If you need auxiliary definitions, [...] * **Helper Lemmas:** You can define reusable lemmas [...] * **Evolvable Definitions and Lemmas** If any definitions or lemmas appear inside sections enclosed by ‘-- EVOLVE-BLOCK-START‘ and ‘-- EVOLVE-BLOCK-END‘, or values appear inside sections enclosed by ‘-- EVOLVE-VALUE-START‘ and ‘-- EVOLVE-VALUE-END‘, you are allowed to modify them. [...] * **Intermediate Steps and Definitions:** * Use ‘have‘ statements for intermediate steps [...] * Use ‘let x := ...‘ to define local objects or values [...] * **Rationale in Comments:** Use Lean comments (‘--‘) to briefly explain the high-level intuition [...] # 4. Learning from Feedback * You will be shown previous attempts (‘Prior Attempts‘) and the current plan to be modified (‘Current Plan‘). Use this information to guide your response. [...] * After providing the new code, add a paragraph in text summarizing the attempt [...] Here are some examples of *bad* theorem sketches: [...] And here is an example of *bad* top level definitions: [...] And here is an example of *good* top level definitions: [...] # Prior Attempts Use these previous attempts to inform the current plan. {previous_programs} # Current Plan This is the plan to be modified in your suggestion. {code} Make sure that you only propose changes inside sections enclosed by ‘-- EVOLVE-BLOCK-START‘ and ‘-- EVOLVE-BLOCK-END‘, or ‘-- EVOLVE-VALUE-START‘ and ‘-- EVOLVE-VALUE-END‘ comments. CRITICAL: You MUST use the search_replace tool to make changes. DO NOT output code blocks in your response - the tool is the ONLY way to modify the code. Aim for 8-10 small changes. If it does not compile, call the tool again to fix it. {lean_guidance} {background_reading_material} # Task {natural_language_plan_instructions}{task_instruction} Remember to make good sketches, capturing the high-level strategy of a correct proof argument for the statement.

Figure 6 | 4:Prompt prover subagents inElided the full-featured (D) (condensed). Figure Sketcherfor agent prompt (condensed). text is representedagent by [...]. Text in braces denotes template variables populated at runtime. For example, {code} is replaced by the current Lean file. Elided text is represented by [...]. Text in braces denotes template variables populated at runtime. For example, {code} is replaced by5 the current Lean file.

23

Advancing Mathematics Research with AI-Driven Formal Proof Search

You are a discerning tournament judge and an expert in formal proof strategies, specializing in Lean. Your task is to serve as the arbiter between competing proof sketches for a given set of theorems. [...] ### Your Objective Your goal is to deliver a professional comparative analysis. You will rank the sketches from best to worst and articulate the precise reasoning behind your decision. [...] ### Proof Sketches to Review The sketches below are labeled 1 to N. {player_blocks} ### Core Judging Criteria & Priorities Evaluate the sketches based on the following principles, which are listed in descending order of importance. **1. Strategic Robustness & Generalizability (Highest Priority)** * **Generalization over Specialization:** Does the strategy scale to the full theorem? [...] * **Avoid "Overfitting":** Penalize strategies that rely on "brute force" computation [...] * **Diversity of Strategy**: The goal is to explore multiple promising lines of reasoning. [...] **2. Quality of Decomposition** You must evaluate the quality of the gaps (sorries) left in the proof. Not all unproven subgoals are equal. * **Good Gaps (Routine/Technical):** It is acceptable to sorry standard mathematical tasks [...] * **Bad Gaps (Miracles/Strategic):** It is unacceptable to sorry the core insight of the proof [...] * **The Rule:** A sketch with good gaps (even if AlphaProof fails to close them) > A sketch with no gaps (but a dead-end strategy). **3. Logical Correctness:** * **Is the plan valid?** [...] * **Coherence:** Do the steps build upon each other logically towards the final goal? [...] ### Feedback and Evaluation Analysis You will receive execution feedback, but you must interpret this carefully: * **AlphaProof Failure != Bad Sketch:** [...] * **System Errors:** Ignore timeouts or service errors. ### Critical Flaws & Red Flags Be vigilant for these issues, which severely undermine a sketch’s quality: * **Asserting a Falsehood:** [...] * **Trivial or Circular Reasoning:** [...] * **Strategic Dead Ends:** [...] ### Feedback and Evaluation error: You will receive execution feedback and/or evaluation errors for each sketch. [...] ### Required Output Format Provide your judgment in the following structured format. [...] **1. Summary of Strategies** * Briefly summarize the approach taken in each sketch. **2. Comparative Analysis** * **Scalability:** [...]? * **Decomposition Quality:** [...] * **Logical Soundness:** [...] * **Strategic Approach:** [...] * **Progress & Feasibility:** [...] **3. Final Judgment** * **Ranking:** Provide a ranking of the sketches from best to worst, using ’>’ for ’better than’ and ’=’ for ’equal in quality’. * **Rationale:** Provide a concluding paragraph that crisply summarizes the primary reasons for your ranking, focusing on the most significant differences in quality based on the judging criteria. Provide a complete rank the sketches from best to worst using ’>’ for ’better than’ and ’=’ for ’equal in quality’. Your output must contain the final ranking in the format ’<decision>2 > 1 = 3</decision>’, containing a ranking of all players presented.

Figure 7 | 3:Prompt for prompt raters (condensed). in the full-featured (D)by(condensed). Elided text is Figure Rater agent Elided text isagent represented [...]. Text in braces denotes template variables populated at runtime. For example, {player blocks} is replaced by the sketches to be represented by [...]. Text in braces denotes template variables populated at runtime. For compared. example, {player_blocks} is replaced by the sketches to be compared. 4

24

Advancing Mathematics Research with AI-Driven Formal Proof Search

# 1. Role and Goal You are a world-class mathematician and Lean 4 expert. Your goal is to solve hard mathematical problems by devising a proof strategy and translating it into a Lean 4 proof. # 2. Your Task You will be given Lean code containing theorem statement with a partial proof. You goal is to modify the file to continue proving the statement until there are no sorries left. You will be getting feedback from Lean Compiler after every time you modify code. Compilation errors will be highlighted and you need to keep iterating until the code compiles. CRITICAL: Don’t end a session with the code which doesn’t compile. You session will be discarded if the final proof doesn’t compile. If you can’t finish the proof in the current session at least make sure it compiles before you wrap up the session. Put any findings, plans or solutions as comments in the file. Only file content will be passed to the next session. Think like a mathematician: focus on the key insights, proof structure, and creative steps (e.g., constructing an object via ‘let‘). If you get stuck on the main proof, try to gain insights by exploring diverse ideas: study specific cases, or define and attempt to prove interesting generalizations, specializations, or variants of the problem statement as new helper lemmas. Prefer clever mathematical arguments over brute-force casework where possible. Some of these problems are very hard, possibly even open problems in mathematics. But don’t be discouraged|approach them with curiosity and persistence. Like George Dantzig, who solved two famous unsolved problems in statistics thinking they were homework, you might solve a problem you think is difficult simply by not knowing it was considered impossible! Believe in your ability to find creative solutions where others might not. CRITICAL: You MUST use tools available to you exhaustively to refine your proof until you either find a proof or are certain the current direction is flawed. Do NOT give up easily, and NEVER put off formalization work to the next session if you have more tool calls available. Your effort in each turn must be maximal: try to solve the problem in full, as if there is no next session. **No Imports:** The execution environment imports ‘Mathlib‘ by default. Do **not** add any ‘import‘ statements in your proof. # Current proof This is the proof to be modified in your session. {code} Make sure that you only propose changes inside sections enclosed by ‘-- EVOLVE-BLOCK-START‘ and ‘-- EVOLVE-BLOCK-END‘, or ‘-- EVOLVE-VALUE-START‘ and ‘-- EVOLVE-VALUE-END‘ comments.

Figure 8 | Full prompt for the basic agent (A). Text in braces denotes template variables

Figure 2: Rater agent prompt (condensed). Elided text is represented by [...]. Text in braces denotes populated at populated runtime. For example,For {code} is replaced by the current Leanbyfile. template variables at runtime. example, {player blocks} is replaced the sketches to be compared.

25

3

Advancing Mathematics Research with AI-Driven Formal Proof Search

came from using test-time RL; however, the system also supports a lower-cost tree search inference mode that we leverage. Subsequently, several other systems have demonstrated strong performance in competition mathematics [1, 15, 40, 6]. At the research level, AI-aided formal proofs have been used primarily to verify results derived in natural language (either by human mathematicians or AI systems), rather than to discover new ones. In particular, Aristotle [1] was used to formalize AI-generated natural language proofs of several Erdős problems – see Tao’s wiki [59] for more details. Gauss [42] was used to produce a formalization of Viazovska’s proof of sphere packing in dimension 8 [28]. Our work differs in that we use Lean as a medium of novel mathematical discovery. Evolution for Mathematical Discovery. The use of evolutionary algorithms to search over programs has a long history in AI [37]. FunSearch [51] introduced the idea of using LLMguided evolution to search for mathematical constructions represented as code. FunSearch was later extended into AlphaEvolve [46], which has been used to improve bounds and find novel constructions in numerous distinct areas of mathematics [25, 45, 44]. Our implementation of agent (D) reuses several components of AlphaEvolve. However, the fundamental difference between the two systems is that AlphaEvolve aims to find programs that optimize a quantitative reward function, while the goal of our agents is to find proofs that pass a boolean formal verification criterion. Natural Language Proof Discovery. A large body of recent work explores whether LLMs can perform research-level mathematical tasks in natural language, as evidenced in the AI CoMathematician [69]. Focusing on theorem proving, Aletheia [21] exemplifies this approach via heavy test-time compute with interleaved generation and revision. Other provers include FullProof [11] and DeepThink [26]. A proprietary model developed by OpenAI resolved several Erdős conjectures [3, 4]. Subsequently, Erdős problem #1196 was resolved informally through community experimentation using GPT-5.4 [2]. Many proofs and partial results discovered this way have been subsequently autoformalized with the help of agents such as Aristotle [1] and Gauss [42]. Further collaborations between mathematicians and AI models have yielded results in optimization theory [33], algebraic geometry [53, 11], and spectral theory [32]. B.2. Selection of Erdős and OEIS Problems For the Erdős evaluation, we ran our agent on all Lean statements of Erdős problems available in the Formal Conjectures repository [23] as of early February 2026 – 353 problems in total. We did not select which problems to attempt; the set was determined entirely by what the open-source community had formalized from the 1200+ problems catalogued on the ErdosProblems site. We recognize that this process has a bias toward problems amenable to formalization in Lean. For the OEIS evaluation, we began with a corpus of 2649 open conjectures drawn from the OEIS [56]. We prompted Gemini to select 500 problems that are non-trivial, mathematically interesting, not famous open problems, and good candidates for automated theorem-proving, and used a Gemini-based agent to formalize them. Of the 500 problems, 8 were excluded due to incompatibilities introduced by a Lean version upgrade, yielding a final set of 492 problems. 26

Advancing Mathematics Research with AI-Driven Formal Proof Search

B.3. Details on Comparisons across Agent Architectures and Models Figure 9 reports, for each Erdős problem, the distribution of computational costs for successful runs, along with the solve rate for each agent. We note a large variance in the cost for most problems and methods, which highlights the stochastic nature of the agent. This is especially noticeable on problems such as Erdős 12(ii) and 152. Cost per proof by method 80%

Method

90%

(A) basic (K=10) (B) basic w/ AP (K=10) (C) basic w/ evolution (K=1) (D) full (K=1)

1750 1500

70% 80% 90%

1250

90%

80%30%

Cost, USD

100%

90% 50%

1000 100%

50%

750

100%

100% 100%

10% 20%

100% 100%

100%

500

100% 100%

100% 100%

250

100% 100%

100% 100% 90%

10% 100% 100% 100% 100%

0%

0 (i)

s_12

erdo

(ii)

s_12

erdo

5

s_12

erdo

s_13

erdo

8

s_15 erdo

2

Problem

s_26 erdo

s_74 erdo

1(i)

741(

s_ erdo

ii)

s_84 erdo

6

Figure 9 | Box plots illustrating the distribution of a cost for successful proof for the Erdős problems. Four distinct experimental configurations are compared: basic@K=10 (blue), basic with AlphaProof @K=10 (orange), basic with evolution (green), and full (red). The solid horizontal line within each box denotes the median cost, while the upper and lower box boundaries represent the third and first quartiles, respectively. Whiskers extend to the rest of the distribution, and individual circles indicate outlier data points. Triangular markers denote instances with a single data point where only one proof attempt was successful. Figure 10 shows the solve rate versus mean inference cost (in USD) for all nine Erdős problems. In addition to the plot in the main text, it also presents results for the full method when run with varying numbers of asynchronous LLM agents. Interestingly, running the full method with only one generator, but sampling from the database (instead of taking the previous session’s output), underperformed in comparison to the basic setup. This suggests that sampling is not beneficial unless one has an asynchronous pipeline and uses the database as a way of coordinating agents. Having three or six asynchronous agents did not outperform the full configuration with 10 agents on the most challenging problems; however, these configurations were more efficient on the easier tasks. Given the high variance in the observed 27

Advancing Mathematics Research with AI-Driven Formal Proof Search

(A) basic

(B) basic w/ AP

(C) basic w/ evolution

Solve Rate

erdos_12(i)

1.0

0.8

0.8

0.8

0.6

0.6

0.6

0.4

0.4

0.4

0.2

0.2

0.2

200 400 600 800 1000 1200 1400

0.0

100

200

300

400

Mean Cost, USD

erdos_138

500

600

0.0

1.0

0.8

0.8

0.8

0.6

0.6

0.6

0.4

0.4

0.4

0.2

0.2

0.2

150

200

250

Mean Cost, USD

300

350

0.0

0

erdos_741(i)

200

400

600

Mean Cost, USD

800

1000

0.0

1.0

0.8

0.8

0.8

0.6

0.6

0.6

0.4

0.4

0.4

0.2

0.2

0.2

100

150

200

250

Mean Cost, USD

300

0.0 5.0

7.5 10.0 12.5 15.0 17.5 20.0 22.5

Mean Cost, USD

400

600

Mean Cost, USD

800

100 150 200 250 300 350 400

Mean Cost, USD

erdos_846

1.0

50

50

erdos_741(ii)

1.0

0.0

200

erdos_26

1.0

100

0

erdos_152

1.0

50

(D) full@6

erdos_125

1.0

0.0

(D) full@3

erdos_12(ii)

Mean Cost, USD

Solve Rate

(D) full@1

1.0

0.0

Solve Rate

(D) full

0.0

50

100

150

200

Mean Cost, USD

250

300

Figure 10 | Solve rate versus mean inference cost (USD) across nine Erdős problem instances. Seven system configurations shown: basic (blue circles), basic with AlphaProof (AP) (orange squares), basic with evolution (green diamonds), full (red triangles), full@1 (purple downward triangles), full@3 (brown pluses), and full@6 (pink x), where @S are the variants of full system with a given number of parallel LLM generation threads. Connected curves denote the number of independent attempts 𝐾 . Error bars indicate one standard error interval. For the basic and basic with AlphaProof configurations, each curve traces the cost–performance Pareto frontier as 𝐾 increases, revealing diminishing marginal returns at higher budgets. Note that basic with AlphaProof and full do not include the inference cost of AlphaProof.

28

Advancing Mathematics Research with AI-Driven Formal Proof Search

Wall-clock time per proof by method 80%

20%

40

10%

Method

basic (K=10) basic w/ AP (K=10) full (K=1)

80% 100%

100% 80% 100%

Time, hours

30

90% 100%

90%

100%

20

100% 50%

100% 100%

10

100% 100% 100%

100% 100%

100%

100%

10%

100% 100%100%

0 erdo

(i)

s_12

(ii)

s_12

erdo

5

s_12

erdo

8

s_13

erdo

2

s_15 erdo

Problem

s_26 erdo

i)

741(

s_ erdo

ii)

741(

s_ erdo

6

s_84 erdo

Figure 11 | Box plots illustrating the distribution of a wall-clock time for a successful proof for the Erdős problems. Three distinct experimental configurations are compared: basic@K=10 (blue), basic with AlphaProof @K=10 (orange), and full (red). The solid horizontal line within each box denotes the median time, while the upper and lower box boundaries represent the third and first quartiles, respectively. Whiskers extend to the rest of the distribution, and individual circles indicate outlier data points. Triangular markers denote instances with a single data point where only one proof attempt was successful. A cut-off of 48 hours applied to all experiments. results, one can conclude that setting 𝐾 = 10 is a strong default for the system. We conducted two additional runs of our basic agent (A), differing only in the proving LLMs used: Gemini 3.0 Flash and Gemini 3.1 Flash-Lite. We also ran the basic setup with AlphaProof as a tool using Gemini 3.0 Flash as the prover model. All runs were executed with 𝐾 = 100 and a 24-hour time budget. None of the three runs were able to solve any of the Erdős problems. To evaluate AlphaProof as a standalone baseline, we ran it in tree search inference mode on all 9 Erdős problems. Even though we allowed a compute budget of approximately 64 v6e TPU hours per problem, the system could not resolve any of them. TPU pricing can be found at https://cloud.google.com/tpu/pricing.

29

Advancing Mathematics Research with AI-Driven Formal Proof Search

The LLM cost for each agent was computed as follows: 𝑡𝑜𝑡𝑎𝑙 𝑐𝑜𝑚𝑝𝑜𝑛𝑒𝑛𝑡 = 𝑖𝑛𝑝𝑢𝑡 ∗ 𝑝𝑖𝑛𝑝𝑢𝑡 + 𝑐𝑎𝑐ℎ𝑒𝑟𝑒𝑎𝑑 ∗ 𝑝𝑐𝑎𝑐ℎ𝑒 + 𝑜𝑢𝑡 𝑝𝑢𝑡 ∗ 𝑝𝑜𝑢𝑡 𝑝𝑢𝑡 , 𝑡𝑜𝑡𝑎𝑙 = 𝑡𝑜𝑡𝑎𝑙 𝑠𝑘𝑒𝑡𝑐ℎ𝑒𝑟 + 𝑡𝑜𝑡𝑎𝑙 𝑟𝑎𝑡𝑒𝑟

where 𝑖𝑛𝑝𝑢𝑡 includes user prompt, agent session prefix, thoughts and tool calls outputs and excludes cached tokens, 𝑐𝑎𝑐ℎ𝑒𝑟𝑒𝑎𝑑 accounts for the input tokens read from cache and 𝑜𝑢𝑡 𝑝𝑢𝑡 includes model output and thoughts. 𝑝 is the corresponding standard price per token as per https://ai.google.dev/gemini-api/docs/pricing. Note that for all agent price estimates, we applied the rate for prompts of 200k tokens or fewer. B.4. Deformalized Lean Proofs Next, we give deformalized versions of the Lean proofs discovered by our full-featured Agent (D). Erdős #12-(i) First, we give the proof of the first question under Erdős problem #12, as classified on the ErdosProblems site (https://www.erdosproblems.com). Theorem (i). There is an infinite set 𝐴 ⊆ ℕ satisfying that there are no distinct 𝑎, 𝑏, 𝑐 ∈ 𝐴 with 𝑎 < 𝑏, 𝑐 satisfying 𝑎 | 𝑏 + 𝑐 and lim inf 𝑁 →∞

| 𝐴 ∩ {1, . . . , 𝑁 }| 𝑁 1/2

> 0.

Proof. We will construct a sequence of "blocks" that individually cannot contain such 𝑎, 𝑏, 𝑐, and with a careful choice of parameters, their union forms the desired set. By precisely controlling the growth and modular residues of these blocks, we ensure the set remains dense enough to satisfy the lim inf condition while avoiding all forbidden divisibility relations. Let 𝑓 : ℕ → ℕ be defined by 𝑓 (0) = 0 and 𝑓 ( 𝑛) = 3 𝑓 (⌊ 𝑛/2⌋) + ( 𝑛 mod 2). The function 𝑓 takes a number represented in base 2 and outputs the number given by the same representation but read in base 3. In particular, the base 3 representation of 𝑓 ( 𝑛) will contain only 0s and 1s. For this reason, 𝑓 ( 𝑎) + 𝑓 ( 𝑏) = 2 𝑓 ( 𝑐) implies 𝑎 = 𝑏 = 𝑐, ensuring the sequence ( 𝑓 ( 𝑛))𝑛∈ℕ contains no 3-APs. Î Next, let 𝐹𝑖 be the 𝑖-th odd prime, and write 𝑀𝑖 = 𝑗<𝑖 𝐹 𝑗 and 𝑉𝑖 = 𝐹𝑖 𝑀𝑖 . By Bertrand’s postulate, we have 𝐹𝑖 ≤ 2𝑖+2 . By the Chinese Remainder Theorem, for each 𝑖, let 𝐶 𝑖 < 𝑉𝑖 be the unique integer such that 𝐶 𝑖 ≡ 0 (mod 𝐹𝑖 ) and 𝐶 𝑖 ≡ 1 (mod 𝑀𝑖 ). Now we define the parameters for the blocks ( 𝐵𝑖 ). Let 3

• 𝑌𝑖 = 3 ( 𝑖+20) be the exponential bounding scale to control the distance between blocks. • 𝑃𝑖 = 10 √𝑉𝑖𝑌𝑖 + 𝐶 𝑖 be the starting coordinate of block 𝑖. • 𝑋𝑖 = ⌊ 𝑃 𝑖+1 ⌋ be the element capacity of block 𝑖. Note that the capacity of 𝐵𝑖 is directly tied to the starting point of the next block 𝐵𝑖+1 . 30

Advancing Mathematics Research with AI-Driven Formal Proof Search

Formally, define 𝐵𝑖 = { 𝑃𝑖 + 𝑉𝑖 𝑓 ( 𝑦 ) | 𝑦 < 𝑋𝑖 }. The purpose of 𝑌𝑖 is to keep the blocks relatively narrow while ensuring they are well-spaced. Note that if 𝑦 < 2𝑘 , then 𝑓 ( 𝑦 ) < 3𝑘 . Letting 𝑘 = ( 𝑖 + 20) 3 , we want to guarantee that for any 𝑦 < 𝑋𝑖 , we have 𝑓 ( 𝑦 ) < 𝑌𝑖 = 3𝑘 . To do this, it √ suffices to show 𝑋𝑖 ≤ 𝑃 𝑖+1 < 2𝑘 , which is equivalent to 𝑃𝑖+1 ≤ 4𝑘 . 2

3

Observe that 𝑃 𝑖+1 ≤ 11𝑉𝑖+1𝑌𝑖+1 ≤ 11 · 2 ( 𝑖+4) · 3 ( 𝑖+21) , following from the bound on 𝐹𝑖 . 3 This is asymptotically strictly smaller than 4𝑘 = 4 ( 𝑖+20) . By adding the shift of 20, the 2 3 3 inequality 11 · 2 ( 𝑖+4) · 3 ( 𝑖+21) ≤ 4 ( 𝑖+20) holds universally for all 𝑖 ≥ 1. Ð Set 𝐴 = 𝑖∈ℕ 𝐵𝑖 . Clearly, 𝐴 is an infinite set. Suppose, for the sake of contradiction, that there exist distinct 𝑎, 𝑏, 𝑐 ∈ 𝐴 with 𝑎 < 𝑏, 𝑐 such that 𝑎 | ( 𝑏 + 𝑐). Let 𝑎 ∈ 𝐵𝑖 . We analyze two cases: • (Case 1: Cross-block) Suppose at least one of 𝑏, 𝑐 is not in 𝐵𝑖 . Without loss of generality, assume 𝑏 ∈ 𝐵 𝑗 for some 𝑗 > 𝑖 (since 𝑏 > 𝑎). Since 𝑎 ∈ 𝐵𝑖 , we have 𝑎 ≡ 0 (mod 𝐹𝑖 ), and thus 𝑏 + 𝑐 ≡ 0 (mod 𝐹𝑖 ) by the divisibility condition. However, by our CRT construction, 𝑏 ≡ 1 (mod 𝐹𝑖 ). The element 𝑐 must belong to some block 𝐵𝑚 with 𝑚 ≥ 𝑖, so 𝑐 ≡ 0 (mod 𝐹𝑖 ) (if 𝑚 = 𝑖) or 𝑐 ≡ 1 (mod 𝐹𝑖 ) (if 𝑚 > 𝑖). Therefore, 𝑏 + 𝑐 ≡ 1 (mod 𝐹𝑖 ) or 𝑏 + 𝑐 ≡ 2 (mod 𝐹𝑖 ). Since 𝐹𝑖 ≥ 3, this directly contradicts 𝑏 + 𝑐 ≡ 0 (mod 𝐹𝑖 ). • (Case 2: Same block) Suppose 𝑏, 𝑐 ∈ 𝐵𝑖 . They must be tightly clustered around 𝑃 𝑖 . Because 𝑦 < 𝑋𝑖 , we have 𝑓 ( 𝑦 ) < 𝑌𝑖 . The maximum "noise" added to any block element is 𝑉𝑖𝑌𝑖 . Since 𝑃 𝑖 > 10𝑉𝑖𝑌𝑖 , any 𝑥 ∈ 𝐵𝑖 must satisfy 𝑥 ∈ [ 𝑃 𝑖 , 1.1 𝑃 𝑖 ]. The divisibility condition 𝑎 | ( 𝑏 + 𝑐) implies 𝑚𝑎 = 𝑏 + 𝑐 for some integer 𝑚. Because 𝑏 + 𝑐 ∈ [2 𝑃 𝑖 , 2.2 𝑃 𝑖 ] and 𝑎 ∈ [ 𝑃 𝑖 , 1.1 𝑃 𝑖 ], it must be that 𝑚 = 2, implying 2𝑎 = 𝑏 + 𝑐. Writing the elements as 𝑎 = 𝑃 𝑖 + 𝑉𝑖 𝑓 ( 𝑎′), 𝑏 = 𝑃𝑖 + 𝑉𝑖 𝑓 ( 𝑏′), and 𝑐 = 𝑃 𝑖 + 𝑉𝑖 𝑓 ( 𝑐′), substitution and cancellation yield 2 𝑓 ( 𝑎′) = 𝑓 ( 𝑏′) + 𝑓 ( 𝑐′). This is impossible for distinct 𝑎′, 𝑏′, 𝑐′ because the image of 𝑓 avoids 3-APs, contradicting the assumption that 𝑎, 𝑏, 𝑐 are distinct. √ Finally, we show that 𝐶 ( 𝑁 ) = | 𝐴 ∩ {1, . . . , 𝑁 }| ≥ 𝑐 𝑁 for some constant 𝑐 > 0. We split into two cases: 1. 𝑁 falls in the gap between 𝐵𝑖 and 𝐵𝑖+1 ; precisely, 𝑃 𝑖 + 𝑉𝑖𝑌√𝑖 ≤ 𝑁 < 𝑃 𝑖+1 . Here, 𝐶 ( 𝑁 ) counts at least all elements in 𝐵√𝑖 , meaning 𝐶 ( 𝑁 ) ≥ 𝑋𝑖 = ⌊ 𝑃 𝑖+1 ⌋. Since 𝑁 ≤ 𝑃 𝑖+1 , we √ √ have 𝑁 ≤ 𝑃 𝑖+1 . Thus, 𝐶√( 𝑁 ) ≥ ⌊√𝑃𝑃𝑖+1 ⌋ ≈ 1. 𝑁 𝑖+1 bound counts 2. 𝑁 is inside the block 𝐵𝑖 ; precisely, 𝑃 𝑖 ≤ 𝑁 < 𝑃 𝑖 + 𝑉𝑖𝑌𝑖 . A pessimistic lower √ only the elements up to the previous block, giving 𝐶 (√︁𝑁 ) ≥ 𝑋𝑖−1 = ⌊ 𝑃 𝑖 ⌋. Observe that √ 𝐶 (𝑁) 𝑉𝑖𝑌𝑖 ≤ 0.1 𝑃 𝑖 , so 𝑁 ≤ 1.1 𝑃 𝑖 < 2 𝑃 𝑖 . Consequently, 𝑃 𝑖 > 𝑁 /2, which implies √ ≥ √1 . 𝑁

𝑁) In both cases, lim inf 𝑁 →∞ 𝐶𝑁(1/2 ≥ √1 > 0.

2

2

□

Erdős #12-(ii) Next, we give a proof for the second question of the three listed in Erdős #12. Theorem (ii). There exists an infinite set 𝐴 ⊂ ℤ+ with no distinct 𝑎, 𝑏, 𝑐 ∈ 𝐴 with 𝑏, 𝑐 > 𝑎, 31

Advancing Mathematics Research with AI-Driven Formal Proof Search

and 𝑎 | 𝑏 + 𝑐, yet for any 𝜀 > 0 and all sufficiently large 𝑁 :

| 𝐴 ∩ {1, . . . , 𝑁 }| ≥ 𝑁 1−𝜀 .

Consequently, there is no absolute constant 𝑐 > 0 such that every such set 𝐴 satisfies | 𝐴 ∩ {1, . . . , 𝑁 }| < 𝑁 1−𝑐 for infinitely many 𝑁 .

Proof. The proof is similar to the previous one for Erdős #12(i), differing mainly in the use of a Behrend-style construction to produce a dense 3-AP-free set. Let 𝑐 ∈ (0, 1), and let ( 𝑃𝑘 ) be a sequence of pairwise coprime integers with 𝑃 𝑘 ≥ 3 and 𝑃 𝑘 ≤ 4𝑘+2 (for example, we can choose 𝑃 𝑘 to be the 𝑘-th odd prime). Next, define the Î 2 running product 𝐿𝑘 = 𝑘𝑖=0 𝑃 𝑖 . As before, we have 𝐿𝑘 ≤ 4 ( 𝑘+2) . By the Chinese Remainder Theorem, there are integers 𝑅 𝑘 < 𝐿𝑘 satisfying 𝑅 𝑘 ≡ 0 (mod 𝑃𝑘 ) and 𝑅 𝑘 ≡ 1 (mod 𝑃𝑖 ) for all 𝑖 < 𝑘.

Choose an integer 𝑚 ≥ 2 satisfying 𝑚 > (2𝑚 + 1) 1−𝑐/2 and define the dimension 𝑉𝑘 = ( 𝑘 + 10) 4 . We use a construction of Behrend to generate dense sets free of 3-term arithmetic progressions. Consider the grid of vectors {1, . . . , 𝑚 }𝑉𝑘 −1 . Let 𝑣 = ( 𝑣0 , . . . , 𝑣𝑉𝑘 −2 ) be such a vector. The squared norm ∥ 𝑣 ∥ 22 takes integer values in the range [𝑉𝑘 − 1, (𝑉𝑘 − 1) 𝑚2 ]. By the pigeonhole principle, there exists an integer radius 𝐾 such that the number of vectors on this sphere satisfies |{ 𝑣 ∈ {1, . . . , 𝑚 }𝑉𝑘 −1 | ∥ 𝑣 ∥ 22 = 𝐾 }| ≥ 𝑚𝑉𝑘 −1 /(𝑉𝑘 𝑚2 + 1). Define 𝑆𝑘 as the set of integers formed by evaluating these vectors in base 2𝑚 + 1, strictly offset by adding a massive leading digit 𝑚 (2𝑚 + 1)𝑉𝑘 −1 : ( ) 𝑉∑︁ 𝑉∑︁ 𝑘 −2 𝑘 −2 𝑆𝑘 = 𝑚 (2𝑚 + 1) 𝑉𝑘 −1 + 𝑣𝑖 (2𝑚 + 1) 𝑖 𝑣 ∈ {1, . . . , 𝑚 }𝑉𝑘 −1 , 𝑣𝑖2 = 𝐾 𝑖=0

𝑖=0

Because the digits are bounded by 𝑚, adding two √ elements in base 2𝑚 + 1 involves no carrying. The restriction to the sphere of radius 𝐾 ensures 𝑆𝑘 contains no 3-APs. Furthermore, because the vectors use digits strictly between 1 and 𝑚, every element 𝑥 ∈ 𝑆𝑘 satisfies 𝑚 (2𝑚 + 1) 𝑉𝑘 −1 ≤ 𝑥 < ( 𝑚 + 1)(2𝑚 + 1) 𝑉𝑘 −1 , ensuring the set is tightly clustered. Ð We define the blocks 𝐴𝑘 = { 𝐿𝑘 𝑥 + 𝑅 𝑘 | 𝑥 ∈ 𝑆𝑘 }, and set 𝐴 = 𝑘∈ℕ 𝐴𝑘 . Clearly, 𝐴 is an infinite set. We verify 𝐴 contains no distinct 𝑎, 𝑏, 𝑐 such that 𝑎 | ( 𝑏 + 𝑐) with 𝑏, 𝑐 > 𝑎. If 𝑎, 𝑏, 𝑐 are in different blocks, a similar modular arithmetic argument as before using the CRT conditions yields a contradiction. If they are in the same block, the tightness of 𝑆𝑘 guarantees 𝑏 + 𝑐 < 3𝑎, forcing the divisibility multiplier to be exactly 2 (i.e., 2𝑎 = 𝑏 + 𝑐), which contradicts the fact that 𝑆𝑘 is 3-AP-free. To ensure the blocks 𝐴𝑘 do not overlap, we bound their elements. The maximum element in 𝐴𝑘 is bounded above by: max( 𝐴𝑘 ) ≤ 𝐿𝑘 ( 𝑚 + 1)(2𝑚 + 1)𝑉𝑘 −1

The minimum element in the next block 𝐴𝑘+1 is bounded below by: min( 𝐴𝑘+1 ) ≥ 𝐿𝑘+1 𝑚 (2𝑚 + 1)𝑉𝑘+1 −1

Because the dimension 𝑉𝑘+1 = ( 𝑘 + 11) 4 is significantly larger than 𝑉𝑘 = ( 𝑘 + 10) 4 , the base exponent strictly dominates, separating the blocks. 32

Advancing Mathematics Research with AI-Driven Formal Proof Search

We now show that | 𝐴 ∩ {1, . . . , 𝑁 }| ≥ 𝑁 1−𝑐 for sufficiently large 𝑁 . The density drops the most in the empty gaps between blocks, with the absolute minimum occurring immediately before block 𝐴𝑘+1 begins. At this point, 𝑁 = min( 𝐴𝑘+1 ) − 1, and our total element count is strictly greater than | 𝐴𝑘 |. Thus, it suffices to prove: | 𝐴𝑘 | ≥ (max( 𝐴𝑘+1 )) 1−𝑐

Substituting our parameter bounds into this inequality yields, and since 𝑚 was chosen to satisfy 𝑚 > (2𝑚 + 1) 1−𝑐/2 , it remains to prove   𝑉𝑘 −1 1− 𝑐/2   1−𝑐 (2𝑚 + 1) 𝑉𝑘+1 −1 ≥ 𝐿 ( 𝑚 + 1)(2 𝑚 + 1) 𝑘 +1 𝑉𝑘 𝑚2 + 1

Ignoring the polynomial denominator and constant multipliers, we compare the asymptotic growth of the exponents on the base 2𝑚 + 1: • On the left hand side, the exponent is (1 − 𝑐/2)(𝑉𝑘 − 1) = (1 − 𝑐/2) 𝑘4 + 𝑂 ( 𝑘3 ). • On the right hand side, the exponent is (1 − 𝑐)(𝑉𝑘+1 − 1) = (1 − 𝑐)( 𝑘 + 11) 4 = (1 − 𝑐) 𝑘4 + 𝑂 ( 𝑘3 ). 2

The contribution of the running product 𝐿𝑘+1 ≤ 4 ( 𝑘+3) and the constant ( 𝑚 + 1) to the right hand side is only 𝑂 ( 𝑘2 ), which is safely absorbed into the 𝑂 ( 𝑘3 ) error term. Because 𝑐 > 0, the 𝑘4 coefficient on the left hand side (1 − 𝑐/2) is strictly greater than the 𝑘4 coefficient on the right hand side (1 − 𝑐). Thus, for sufficiently large 𝑘, the left hand side asymptotically dominates, and the inequality holds. □ These questions were posed in 1970 [18], and saw attention from multiple human mathematicians, achieving partial results towards the questions [54, 7, 17]. We thank Thomas Bloom for summarizing the history regarding these questions on the ErdosProblems site (https://www.erdosproblems.com). Note that the answer to the (ii) implies the answer to (i). Nevertheless, we included both proofs as the agent found them independently, as each question was separately formalized as a theorem in Formal Conjectures. Originally, the agent located multiple proofs for the second question, though we chose the first proof to informalize for presentation. It also happened to differ the most in the construction, which otherwise is quite similar to the proof for (i). After sharing the solutions publicly, it was noted that a minor adjustment could be performed on the construction from the original paper to answer the questions. The third and final Í question, asking whether such a set 𝐴 could satisfy 𝑎∈ 𝐴 1/𝑎 = ∞, is still open and seems difficult. We provide the Lean proof discovered for (i) at https://github.com/google-dee

pmind/alphaproof-nexus-results/blob/main/APNOutputs/ErdosProblems/er dos_12.parts.i.lean and for (ii) at https://github.com/google-deepmind/alph aproof-nexus-results/blob/main/APNOutputs/ErdosProblems/erdos_12.par ts.ii.lean. Our original communication of the result can be found at the problem thread of the ErdosProblems site: https://www.erdosproblems.com/forum/thread/12. 33

Advancing Mathematics Research with AI-Driven Formal Proof Search

Erdős #125 Í Question. Let 𝐴 = { 𝜖𝑘 3𝑘 : 𝜖𝑘 ∈ {0, 1}} be the set of integers which have only the digits 0,1 Í when written base 3, and 𝐵 = { 𝜖𝑘 4𝑘 : 𝜖𝑘 ∈ {0, 1}} be the set of integers which have only the digits 0, 1 when written base 4. Does 𝐴 + 𝐵 have positive lower density? Proof. We show that the answer is no: the lower density is zero. Let 𝐴 and 𝐵 be defined as the sets of integers whose base 3 and base 4 representations, respectively, contain only the digits 0 and 1. We will show that the lower density of 𝐴 + 𝐵 is zero.

For any integer 𝑎 ∈ 𝐴, we can decompose it at the 𝑘-th digit into a top and bottom part, writing 𝑎 = 3𝑘 𝑎𝑡𝑜𝑝 + 𝑎𝑏𝑜𝑡 . Because 𝑎 uses only the digits 0 and 1, both 𝑎𝑡𝑜𝑝 and 𝑎𝑏𝑜𝑡 must also belong to 𝐴. Furthermore, the maximum possible value for 𝑎𝑏𝑜𝑡 is the integer consisting of 𝑘 ones in base 3, which provides the strict upper bound 𝑎𝑏𝑜𝑡 ≤ (3𝑘 − 1)/2. By applying the exact same logic to any 𝑏 ∈ 𝐵 at scale 𝑚, we can write 𝑏 = 4𝑚 𝑏𝑡𝑜𝑝 + 𝑏𝑏𝑜𝑡 , yielding the analogous bound 𝑏𝑏𝑜𝑡 ≤ (4𝑚 − 1)/3.

To evaluate the density of 𝐴 + 𝐵 up to a large scale, we define a threshold 𝑀 · 𝑁0 , where 𝑀 = min(3𝑘 , 4𝑚 ) for some integers 𝑘 and 𝑚. Consider any element 𝑥 ∈ 𝐴 + 𝐵 such that 𝑥 < 𝑀 · 𝑁0 . By definition, 𝑥 = 𝑎 + 𝑏 for some 𝑎 ∈ 𝐴 and 𝑏 ∈ 𝐵. Using the previously established decompositions, we can express this sum as 𝑥 = 3𝑘 𝑎𝑡𝑜𝑝 + 𝑎𝑏𝑜𝑡 + 4𝑚 𝑏𝑡𝑜𝑝 + 𝑏𝑏𝑜𝑡 . Assume without loss of generality that 3𝑘 ≤ 4𝑚 , so 𝑀 = 3𝑘 . We can rewrite this expression to factor out 𝑀 , yielding 𝑥 = 3𝑘 ( 𝑎𝑡𝑜𝑝 + 𝑏𝑡𝑜𝑝 ) + 𝑐, where the remainder term is 𝑐 = (4𝑚 − 3𝑘 ) 𝑏𝑡𝑜𝑝 + 𝑎𝑏𝑜𝑡 + 𝑏𝑏𝑜𝑡 .

Let 𝑦 = 𝑎𝑡𝑜𝑝 + 𝑏𝑡𝑜𝑝 . Since 𝑎𝑡𝑜𝑝 ∈ 𝐴 and 𝑏𝑡𝑜𝑝 ∈ 𝐵, it naturally follows that 𝑦 ∈ 𝐴 + 𝐵. Furthermore, because 𝑥 < 3𝑘 𝑁0 , we must have 𝑦 < 𝑁0 , which in turn dictates that 𝑏𝑡𝑜𝑝 ≤ 𝑁0 . Applying our bounds for the bottom parts, we can bound the remainder 𝑐 by a maximum value 𝐶 , defined as 𝐶 = |4𝑚 − 3𝑘 | 𝑁0 + (3𝑘 − 1)/2 + (4𝑚 − 1)/3. This shows that any valid sum 𝑥 < 𝑀 · 𝑁0 is uniquely determined by choosing a base value 𝑦 ∈ ( 𝐴 + 𝐵) ∩ [0, 𝑁0 ) and a remainder 𝑐 ∈ [0, 𝐶 ]. Therefore, the total number of elements in 𝐴 + 𝐵 strictly less than 𝑀 · 𝑁0 is bounded by the product of the number of choices for 𝑦 and the number of choices for 𝑐. Dividing by the interval length 𝑀 · 𝑁0 yields an upper bound on the density at this new scale: the density up to 𝑀 · 𝑁0 is less than or equal to the density up to 𝑁0 multiplied by the factor ( 𝐶 + 1)/ 𝑀 .

To force the density to drop, we require this multiplying factor to be strictly less than 1. Because the ratio of logarithms ln(4)/ln(3) is irrational, Dirichlet’s Approximation Theorem guarantees that we can find arbitrarily large integers 𝑘 and 𝑚 such that the ratio 4𝑚 /3𝑘 is arbitrarily close to 1. By choosing 𝑘 and 𝑚 carefully, the absolute difference |4𝑚 − 3𝑘 | becomes extremely small relative to 𝑀 . Consequently, for any given 𝑁0 , we can select 𝑘 and 𝑚 large enough such that ( 𝐶 + 1)/ 𝑀 ≤ 0.99.

We can now apply this bounding process iteratively. Starting from an arbitrary scale 𝑁0 , we can find a larger scale 𝑁1 = 𝑀1 𝑁0 where the density of 𝐴 + 𝐵 drops by a factor of at least 0.99. Taking 𝑁1 as our new baseline, we find a still larger scale 𝑁2 = 𝑀2 𝑁1 where the density drops by another factor of 0.99. After 𝑟 iterations, the density of the set up to the scale 𝑁𝑟 is bounded by (0.99) 𝑟 . As 𝑟 → ∞, this bound approaches 0. This demonstrates the existence of a sequence of arbitrarily large scales where the density tends to 0, proving that the lower density of 𝐴 + 𝐵 is 0. □ 34

Advancing Mathematics Research with AI-Driven Formal Proof Search

We originally communicated the result in https://www.erdosproblems.com/fo rum/thread/125#post-5110. The Lean proof is at https://github.com/google-d eepmind/alphaproof-nexus-results/blob/main/APNOutputs/ErdosProblem s/erdos_125.variants.positive_lower_density.lean. In the discussion at the

ErdosProblems site, it was pointed out that this leaves two possibilities regarding the set 𝐴 + 𝐵: 1. 𝐴 + 𝐵 has zero upper and lower density (and hence also zero density), or 2. 𝐴 + 𝐵 has zero lower density, but positive upper density (and hence no density). Erdős #138, Differences Variant

Question. Let the van der Waerden number 𝑊 ( 𝑘) be such that whenever 𝑁 ≥ 𝑊 ( 𝑘) and {1, . . . , 𝑁 } is 2-coloured there must exist a monochromatic 𝑘-term arithmetic progression. Is it true that 𝑊 ( 𝑘 + 1) − 𝑊 ( 𝑘) → ∞?

Proof. We will show that 𝑊 ( 𝑘 + 1) ≥ 𝑊 ( 𝑘) + 𝑘, which establishes that 𝑊 ( 𝑘 + 1) − 𝑊 ( 𝑘) → ∞. Given a 2-coloring of the first 𝑊 ( 𝑘) − 1 integers without a monochromatic 𝑘-AP, we can extend it by 𝑘 further elements without creating a monochromatic ( 𝑘 + 1)-AP by proceeding greedily. Adding new elements one by one, suppose we have validly colored up to 𝑀 (where 𝑀 < 𝑊 ( 𝑘) − 1 + 𝑘); we simply color 𝑀 + 1 red if doing so doesn’t create a red ( 𝑘 + 1)-AP, and blue otherwise. The only way this algorithm could result in an invalid coloring is if both choices are blocked, meaning there is already a red 𝑘-AP with some step size 𝑑 𝑅 and a blue 𝑘-AP with some step size 𝑑 𝐵 such that the ( 𝑘 +1)-th element for both progressions lands exactly on 𝑀 +1. But this is impossible. Because our original interval up to 𝑊 ( 𝑘) − 1 has no monochromatic 𝑘-APs, these progressions must contain at least one newly added element, which bounds their step sizes to 𝑑 𝑅 , 𝑑 𝐵 ≤ 𝑘 − 1. Hence, if we step backward 𝑑 𝐵 times along the red progression and 𝑑 𝑅 times along the blue progression, both calculations land exactly on the positive integer 𝑀 + 1 − 𝑑 𝑅 𝑑 𝐵 , meaning this single point would have to be simultaneously colored red and blue, which is a contradiction. □ We originally communicated the result in https://www.erdosproblems.com/foru m/thread/138#post-5314, and share the Lean proof at https://github.com/googl

e-deepmind/alphaproof-nexus-results/blob/main/APNOutputs/ErdosProbl ems/erdos_138.variants.difference.lean. In the discussion at the ErdosProblems

site, Thomas Bloom pointed out that the obvious generalization of this argument gives 𝑊 ( 𝑘 + 1, 𝑙 + 1) ≥ 𝑊 ( 𝑘, 𝑙 ) + min( 𝑘, 𝑙 ), and asked what this kind of argument can prove for the 𝑟 -color variant 𝑊𝑟 ( 𝑘). Erdős #741-(i) Question. Let 𝐴 ⊆ ℕ be such that 𝐴 + 𝐴 has positive upper density. Can one always decompose 𝐴 = 𝐴1 ⊔ 𝐴2 such that 𝐴1 + 𝐴1 and 𝐴2 + 𝐴2 both have positive upper density?

Proof. We show that the answer is yes. We use an alternating block partition. Given a rapidly

35

Advancing Mathematics Research with AI-Driven Formal Proof Search

growing sequence 𝑀0 < 𝑀1 < 𝑀2 < · · · , we define Ø 𝐴1 = 𝐴 ∩ ( 𝑀2𝑘 , 𝑀2𝑘+1 ] , 𝑘

𝐴2 = 𝐴 \ 𝐴1 .

In odd-indexed intervals ( 𝑀2𝑘 , 𝑀2𝑘+1 ], all elements of 𝐴 belong to 𝐴1 ; in even-indexed intervals ( 𝑀2𝑘+1 , 𝑀2𝑘+2 ], they all belong to 𝐴2 . The sequence 𝑀 is chosen to grow fast enough that each block dwarfs all previous ones. We split into two cases. Case 1: 𝐴 has positive upper density. There exist a constant 𝑐 > 0 and a strictly increasing sequence of scales along which | 𝐴 ∩ [1, 𝑁 ]| ≥ 𝑐 · 𝑁 . Using a dependent-choice argument, we extract a rapidly growing sequence 𝑀𝑘 such that for each 𝑘: • | 𝐴 ∩ [1, 𝑀𝑘+1 ]| ≥ 𝑐 · 𝑀𝑘+1 (density is retained at the next scale), • | 𝐴 ∩ [1, 𝑀𝑘 ]| ≤ 4𝑐 · 𝑀𝑘+1 (the “past” is negligible relative to the “future”). Because each new block contains all the “fresh” elements of 𝐴, looking at scale 𝑀2𝑘+1 shows that 𝐴1 has positive upper density, and looking at scale 𝑀2𝑘+2 shows the same for 𝐴2 . A short argument then lifts this: if a set has positive upper density, so does its sumset with itself. Case 2: 𝐴 has zero upper density but 𝐴 + 𝐴 has positive upper density. This is the harder case, since 𝐴 is too sparse to guarantee positive density for the parts directly. Instead, we argue about the sumsets themselves. Since 𝐴 + 𝐴 has positive upper density, there exist 𝑐 > 0 and a sequence of scales along which |( 𝐴 + 𝐴) ∩ [1, 𝑁 ]| ≥ 𝑐 · 𝑁 . Since 𝐴 has zero upper density, | 𝐴 ∩ [1, 𝑁 ]| = 𝑜 ( 𝑁 ), so for any fixed 𝐾 there are arbitrarily large 𝑁 where ( 𝐾 + 1) · | 𝐴 ∩ [1, 𝑁 ]| ≤ 4𝑐 · 𝑁 . By dependent choice, we extract a rapidly growing 𝑀𝑘 such that for each 𝑘: • |( 𝐴 + 𝐴) ∩ [1, 𝑀𝑘+1 ]| ≥ 𝑐 · 𝑀𝑘+1 , • ( 𝑀𝑘 + 1) · | 𝐴 ∩ [1, 𝑀𝑘+1 ]| ≤ 4𝑐 · 𝑀𝑘+1 . The key ingredient is a combinatorial sumset bound: if 𝐴 = 𝐴1 ∪ 𝐴2 and every element of 𝐴2 in [1, 𝑁 ] is at most 𝐾 , then |( 𝐴 + 𝐴) ∩ [1, 𝑁 ]| ≤ |( 𝐴1 + 𝐴1 ) ∩ [1, 𝑁 ]| + ( 𝐾 + 1) · | 𝐴 ∩ [1, 𝑁 ]| .

The idea is that any sum involving an element of 𝐴2 has one summand bounded by 𝐾 , giving at most ( 𝐾 + 1) · | 𝐴 ∩ [1, 𝑁 ]| such sums. Applying this bound at alternating scales: • At scale 𝑁 = 𝑀2𝑘+1 : all elements of 𝐴2 in [1, 𝑁 ] lie below 𝑀2𝑘 , so the bound with 𝐾 = 𝑀2𝑘 gives |( 𝐴1 + 𝐴1 ) ∩ [1, 𝑁 ]| ≥ 34𝑐 · 𝑁 . • At scale 𝑁 = 𝑀2𝑘+2 : symmetrically, all elements of 𝐴1 in [1, 𝑁 ] lie below 𝑀2𝑘+1 , giving |( 𝐴2 + 𝐴2 ) ∩ [1, 𝑁 ]| ≥ 34𝑐 · 𝑁 . Since these bounds hold for infinitely many 𝑁 , both sumsets have positive upper density. □ The agent also initially disproved a strict “natural density” formulation of this problem (where the density must exist as a limit), which served as a diagnostic for the correct 36

Advancing Mathematics Research with AI-Driven Formal Proof Search

interpretation of Erdős’ original phrasing. Following Thomas Bloom’s observation that Erdős likely meant “positive upper density,” the formulation was amended and the agent resolved the corrected version as described above. The Lean proof for the upper density variant is available at https://github.com/google-deepmind/alphaproof-nexus-results /blob/main/APNOutputs/ErdosProblems/erdos_741.parts.i.lean. Erdős #741-(ii) Question. Is there a basis 𝐴 of order 2 such that if 𝐴 = 𝐴1 ⊔ 𝐴2 then 𝐴1 + 𝐴1 and 𝐴2 + 𝐴2 cannot both have bounded gaps? Proof. We show that the answer is yes by constructing a pathological basis 𝐴 with “forbidden zones” that force any partition to create arbitrarily large gaps in at least one component sumset. Step 1: The construction. Choose a sequence of rapidly growing scales 𝑃 𝑘 = 100𝑘 . For each 𝑘 ≥ 1, define a forbidden zone 𝑍 𝑘 , which is a broad interval of integers running roughly from 11 2 𝑃 𝑘 to 11 𝑃 𝑘 + 𝑘. In the middle of this zone, we leave a single “oasis” — an isolated element 𝑥 𝑘 = 10 𝑃 𝑘 . The set 𝐴 consists of all natural numbers that avoid every forbidden zone, together with the oases 𝑥 𝑘 . In visual terms, 𝐴 is made of clumps of consecutive integers separated by large empty gaps, each containing a single survivor 𝑥 𝑘 . Step 2: 𝐴 ∪ {0} is a basis of order 2. We must show every natural number 𝑛 can be written as 𝑎 + 𝑏 with 𝑎, 𝑏 ∈ 𝐴 ∪ {0}: • If 𝑛 ∉ 𝑍 𝑘 for any 𝑘, then 𝑛 ∈ 𝐴 and we use 𝑛 + 0 = 𝑛. • If 𝑛 ∈ 𝑍 𝑘 and 𝑛 lies in the lower half of 𝑍 𝑘 , we use ⌊ 𝑛/2⌋ + ⌈𝑛/2⌉. Because 𝑛 is small enough, neither half lands in 𝑍 𝑘 , and both are large enough to avoid the previous zone 𝑍 𝑘−1 . • If 𝑛 ∈ 𝑍 𝑘 and 𝑛 lies in the upper half, we use the oasis: 𝑛 = 𝑥 𝑘 + ( 𝑛 − 𝑥 𝑘 ). The difference 𝑛 − 𝑥 𝑘 is small enough that it falls safely before the forbidden zone 𝑍 𝑘 . Step 3: No syndetic partition exists. Suppose 𝐴 = 𝐴1 ⊔ 𝐴2 . Consider a target sum 𝑚 ∈ [11 𝑃 𝑘 , 11 𝑃 𝑘 + 𝑘]. To write 𝑚 = 𝑢 + 𝑣 with 𝑢, 𝑣 ∈ 𝐴, the algebra forces the larger operand 𝑣 to land inside the forbidden range [ 11 2 𝑃 𝑘 , 11 𝑃 𝑘 + 𝑘]. But the only element of 𝐴 in this range is 𝑥 𝑘 . Therefore, representing any sum in [11 𝑃𝑘 , 11 𝑃𝑘 + 𝑘] requires 𝑥 𝑘 . By the pigeonhole principle, 𝑥 𝑘 belongs to exactly one partition component, say 𝐴1 . Then 𝐴1 + 𝐴1 can cover the interval [11 𝑃 𝑘 , 11 𝑃 𝑘 + 𝑘] using 𝑥 𝑘 , but 𝐴2 + 𝐴2 is completely locked out — it cannot represent any element in that interval. This leaves a gap of length 𝑘 in 𝐴2 + 𝐴2 . Since 𝑘 can be made arbitrarily large, the gaps in one component’s sumset are unbounded, proving it is impossible to partition 𝐴 so that both sumsets have bounded gaps. □ The Lean proof for part (ii) is available at https://github.com/google-deepmind/

alphaproof-nexus-results/blob/main/APNOutputs/ErdosProblems/erdos_12 .parts.ii.lean. Our original communication of both results can be found in the problem thread on the ErdosProblems site (https://www.erdosproblems.com/forum/thread /741). 37

Advancing Mathematics Research with AI-Driven Formal Proof Search

Erdős #26, More General Variant Theorem. Let M ( 𝑆) denote the set of multiples of a subset 𝑆 ⊆ ℕ, and let 𝑑 ( 𝑋 ) denote the upper asymptotic density of a set 𝑋 . There exists a sequence 𝐴 : ℕ → ℕ satisfying Í 𝑖 ∈ℕ 1/ 𝐴 ( 𝑖) = ∞, such that for 𝜖 = 1/4 and for all 𝑘 ≥ 1, we have 𝑑 (M ( 𝐴 + 𝑘)) < 1 − 𝜖.

Proof. We construct the sequence iteratively in finite blocks and show that for any arbitrary shift 𝑘, we can bound the upper density of the shifted sequence by analyzing three distinct cases, the third case relying on the construction being similar to the simple counterexample of Ruzsa which resolved the original question Erdős #26. Let ( 𝑞 𝑗 ) ∞ be a strictly increasing sequence of primes satisfying 𝑞1 ≥ 29 (chosen large 𝑗=1 enough to cause small enough density in the infinite tail of the sequence). We define a ∞ recursively, starting with 𝐽 = 0. strictly increasing sequence of indices (or “jumps”) ( 𝐽𝑚 )𝑚 0 =0 Suppose 𝐽𝑚 has been defined, and the sequence 𝐴 ( 𝑖) has been constructed for all 𝑖 < 𝐽𝑚 . We define the parameters for the 𝑚-th block as follows. Î 𝐽𝑚 First, define the step size 𝑃𝑚 = 10 𝑞 𝑗 . Next, by the Chinese Remainder Theorem, we can 𝑗=1 choose a base size 𝑅𝑚 satisfying the following system of congruences 𝑅𝑚 ≡ − 𝑗

(mod 𝑞 𝑗 )

for 1 ≤ 𝑗 ≤ 10 𝐽𝑚

as well as the strict monotonicity condition 𝑅𝑚 > 𝐴 ( 𝐽𝑚 − 1) (where we set 𝐴 (−1) = 0), by adding enough multiples of 𝑃𝑚 . Í 1 With 𝑅𝑚 and 𝑃𝑚 fixed, the series ∞ 𝑥 =1 𝑅 𝑚 + 𝑥 𝑃𝑚 diverges. Thus, we can compute a block length 𝐿𝑚 ≥ 1 such that the partial sum satisfies: 0.1 ≤

1 ≤ 0.2 𝑅𝑚 + 𝑥 𝑃𝑚 𝑥 =1

𝐿𝑚 ∑︁

We then set 𝐽𝑚+1 = 𝐽𝑚 + 𝐿𝑚 . Now that the bounds of the block are properly defined, for indices 𝑖 ∈ [ 𝐽𝑚 , 𝐽𝑚+1 ), we set: 𝐴 ( 𝑖) = 𝑅𝑚 + ( 𝑖 − 𝐽𝑚 + 1) 𝑃𝑚

Í Since each block contributes at least 0.1 to the total harmonic sum, the overall sum 1/ 𝐴 ( 𝑖) diverges. Pick an arbitrary shift 𝑘 ≥ 1; we must now show that 𝑑 (M ( 𝐴 + 𝑘)) stays bounded below 3/4. Let 𝑚0 be the unique integer satisfying: 10 𝐽𝑚0 ≤ 𝑘 < 10 𝐽𝑚0 +1

We partition the shifted sequence 𝐴 + 𝑘 into three regimes and bound the upper density of the multiples generated by each: • (Case 1: 𝑖 < 𝐽𝑚0 ) The upper density of the multiples generated by this finite set is bounded by the sum of their reciprocals. Because 𝐴 ( 𝑖) > 0, we have 𝐴 ( 𝑖) + 𝑘 > 𝑘, yielding: 𝑑 (M ({ 𝐴 ( 𝑖) + 𝑘 | 𝑖 < 𝐽𝑚0 })) ≤

𝐽𝑚0 −1

∑︁ 𝑖=0

𝐽𝑚 −1

0 ∑︁ 1 1 𝐽𝑚0 < = ≤ 0.1 𝐴 ( 𝑖) + 𝑘 𝑘 𝑘 𝑖=0

38

Advancing Mathematics Research with AI-Driven Formal Proof Search

• (Case 2: 𝐽𝑚0 ≤ 𝑖 < 𝐽𝑚0 +1 ) Shifting by a positive 𝑘 strictly decreases the reciprocals, so the upper density of the multiples from this critical block satisfies: 𝑑 (M ({ 𝐴 ( 𝑖) + 𝑘 | 𝐽𝑚0 ≤ 𝑖 < 𝐽𝑚0 +1 })) ≤

𝐽𝑚0 +1 −1

∑︁

𝑖= 𝐽𝑚0

𝐽𝑚0 +1 −1 ∑︁ 1 1 < ≤ 0.2 𝐴 ( 𝑖) + 𝑘 𝐴 ( 𝑖) 𝑖= 𝐽 𝑚0

• (Case 3: 𝑖 ≥ 𝐽𝑚0 +1 ) Consider any element 𝐴 ( 𝑖) where 𝑖 belongs to some block 𝑚 ≥ 𝑚0 +1, meaning 10 𝐽𝑚 ≥ 10 𝐽𝑚0 +1 > 𝑘. Recall the construction of the 𝑚-th block: 𝐴 ( 𝑖) + 𝑘 = ( 𝑅𝑚 + 𝑘) + ( 𝑖 − 𝐽𝑚 + 1) 𝑃𝑚

Because 10 𝐽𝑚 ≥ 𝑘, we have 𝑞𝑘 | 𝑃𝑚 . By construction, we also have 𝑞𝑘 | ( 𝑅𝑚 + 𝑘). Consequently, 𝑞𝑘 | ( 𝐴 ( 𝑖) + 𝑘) for every element in this infinite tail. The set of multiples generated by Case 3 is therefore entirely contained within the multiples of the prime 𝑞𝑘 . Expressing this with the upper density notation: 𝑑 (M ({ 𝐴 ( 𝑖) + 𝑘 | 𝑖 ≥ 𝐽𝑚0 +1 })) ≤ 𝑑 (M ({𝑞𝑘 })) =

1 𝑞𝑘

≤

1 29

By the union bound, the total upper density of the multiples of 𝐴 + 𝑘 is bounded above by: 0.1 + 0.2 +

1 3 ≈ 0.334 < = 1 − 𝜖. 29 4

□ This problem is a more general variant to the original question stating that “For all 𝐴 ⊆ ℕ, does there exist 𝑘 ≥ 1 such that almost all integers have a divisor of the form 𝑎 + 𝑘 for some 𝑎 ∈ 𝐴?”. A simple counterexample to this question can be produced using the Chinese Remainder Theorem. In the more general variant we resolve, note the Chinese Remainder Theorem is still used to construct a counterexample, but with additional constraints to make the upper density of 𝐴 + 𝑘 small, for all 𝑘. We originally communicated the result in https://www.erdosproblems.com/forum/thread/26, and share the Lean proof at

https://github.com/google-deepmind/alphaproof-nexus-results/blob/main /APNOutputs/ErdosProblems/erdos_26.variants.tenenbaum.lean. Erdős #846 Theorem. Let 𝐴 ⊂ ℝ2 be an infinite set for which there exists some 𝜖 > 0 such that in any subset of 𝐴 of size 𝑛 there are always at least 𝜖𝑛 with no three on a line. Is it true that 𝐴 is the union of a finite number of sets where no three are on a line? Proof. We will show that there exists an infinite set 𝐴 ⊂ ℝ2 for which any 𝑛-element subset contains at least 𝑛/2 points with no three on a line, but 𝐴 is not the union of a finite number of sets where no three are on a line. Let 𝐾∞ be the countably infinite complete graph with vertex set 𝑉 = { 𝑥1 , 𝑥2 , . . . }. We choose the sequence of real numbers ( 𝑥 𝑖 ) 𝑖∞=1 such that it grows sufficiently fast to avoid 39

Advancing Mathematics Research with AI-Driven Formal Proof Search

any accidental roots of polynomials that will arise in our collinearity condition, by setting 𝑛 𝑥𝑛 = 1004 . We construct our point set 𝐴 ⊂ ℝ2 by mapping each edge 𝑒 = { 𝑥 𝑖 , 𝑥 𝑗 } of 𝐾∞ to a point 𝑃𝑒 as follows: 𝑃𝑒 = ( 𝑥 𝑖 + 𝑥 𝑗 , 𝑥 𝑖2 + 𝑥 𝑖 𝑥 𝑗 + 𝑥 2𝑗 ) (1) Let 𝐴 = { 𝑃𝑒 | 𝑒 ∈ 𝐸 ( 𝐾∞ )}.

Lemma. Three points in 𝐴 are collinear if and only if their corresponding edges form a triangle in 𝐾∞ .

Proof of Lemma. First, assume three edges form a triangle in 𝐾∞ with vertices 𝑎, 𝑏, 𝑐 ∈ 𝑉 . The corresponding points in 𝐴 are: 𝑃 𝑎𝑏 = ( 𝑎 + 𝑏, 𝑎2 + 𝑎𝑏 + 𝑏2 ) 𝑃𝑏𝑐 = ( 𝑏 + 𝑐, 𝑏2 + 𝑏𝑐 + 𝑐2 )

𝑃 𝑐𝑎 = ( 𝑐 + 𝑎, 𝑐2 + 𝑐𝑎 + 𝑎2 )

The slope 𝑚 of the line connecting 𝑃𝑎𝑏 and 𝑃𝑏𝑐 is given by: 𝑚=

( 𝑏2 + 𝑏𝑐 + 𝑐2 ) − ( 𝑎2 + 𝑎𝑏 + 𝑏2 ) 𝑐2 − 𝑎2 + 𝑏𝑐 − 𝑎𝑏 = ( 𝑏 + 𝑐) − ( 𝑎 + 𝑏) 𝑐−𝑎

Factoring the numerator yields: 𝑚=

( 𝑐 − 𝑎)( 𝑐 + 𝑎) + 𝑏 ( 𝑐 − 𝑎) =𝑎+𝑏+𝑐 𝑐−𝑎

By symmetry, the slope of the line connecting 𝑃𝑏𝑐 and 𝑃 𝑐𝑎 is also 𝑎 + 𝑏 + 𝑐. Because the slopes are equal, the three points are collinear. Conversely, suppose three distinct edges do not form a triangle. We must show their corresponding points are not collinear. The condition that these points are collinear is equivalent to the determinant of their 3 × 3 augmented coordinate matrix evaluating to zero. Because the sequence ( 𝑥 𝑖 ) 𝑖∞=1 grows quickly enough, any polynomial evaluated on its terms is strictly dominated by the highest power of its largest variable. By sorting the endpoints of the three edges, we can group the expanded determinant into three topological cases based on whether the largest vertex is present in one, two, or all three of the edges. In every case, because the edges are distinct and do not form a triangle, the coefficient of the dominant highest-degree term is bounded strictly away from zero. Furthermore, the massive gap between consecutive terms in the sequence ensures that the lower-degree terms are strictly bounded and cannot sum to cancel the leading term out. Therefore, the determinant never evaluates to zero, and no accidental collinearities occur. □ Lemma. Any 𝑛-element subset of 𝐴 contains at least 𝑛/2 points with no three on a line.

Proof of Lemma. Let 𝑆 ⊂ 𝐴 be an arbitrary subset of size 𝑛. The elements of 𝑆 correspond to a subgraph 𝐺𝑆 ⊂ 𝐾∞ containing exactly 𝑛 edges. Every graph with 𝑛 edges contains a bipartite subgraph 𝐵𝑆 with at least 𝑛/2 edges. Because 𝐵𝑆 is bipartite, it contains no odd cycles and is therefore triangle-free. By the previous lemma, the corresponding points in 𝐴 40

Advancing Mathematics Research with AI-Driven Formal Proof Search

contain no collinear triplets. This provides a subset of at least ⌈𝑛/2⌉ points with no three on a line, satisfying the condition with 𝜖 = 1/2. □ To complete the proof of the theorem, assume for contradiction that 𝐴 can be covered by Ð a finite number of sets where no three are on a line; that is, 𝐴 = 𝑟𝑘=1 𝐴𝑘 . This partition naturally induces an 𝑟 -coloring on the edges of 𝐾∞ . By the infinite Ramsey Theorem, any finite coloring of the edges of the infinite complete graph must contain a monochromatic triangle. Consequently, there exists some color class 𝑘 containing three edges that form a triangle. By the lemma, these three edges map to three collinear points in 𝐴𝑘 . This contradicts the assumption that 𝐴𝑘 contains no three collinear points. Therefore, 𝐴 cannot be covered by finitely many sets with no three on a line.

□

We originally communicated the result in https://www.erdosproblems.com/fo rum/thread/846#post-4447 to the ErdosProblems site, and share the Lean proof at

https://github.com/google-deepmind/alphaproof-nexus-results/blob/ma in/APNOutputs/ErdosProblems/erdos_846.lean. This result was independently

discovered by an internal model at OpenAI [49]. In the discussion at the ErdosProblems site, it was pointed out that this result also follows from a projection argument of Reiher, Rödl and Sales [50]. Erdős #152 Theorem. For a Sidon set 𝐴 ⊂ ℕ of size 𝑛, let 𝐼 ( 𝐴 + 𝐴) count the isolated elements of the sumset — those 𝑠 ∈ 𝐴 + 𝐴 with 𝑠 ± 1 ∉ 𝐴 + 𝐴. Define 𝑓 ( 𝑛) as the minimum of 𝐼 ( 𝐴 + 𝐴) over all Sidon sets of size 𝑛. Then 𝑓 ( 𝑛) ≥ ( 𝑛2 − 100𝑛 − 16)/16, so in particular 𝑓 ( 𝑛) → ∞. Proof. The proof establishes, for every Sidon set 𝐴 of size 𝑛: 16 · 𝐼 ( 𝐴 + 𝐴) + 100𝑛 + 16 ≥ 𝑛2 .

(★)

Let 𝐷 = { 𝑎 − 𝑏 : 𝑎, 𝑏 ∈ 𝐴 } denote the difference set and 𝑆 = 𝐴 + 𝐴 the sumset. For any set 𝑋 ⊆ ℤ, let 𝑁𝑘 ( 𝑋 ) := | 𝑥 ∈ 𝑋 : 𝑥 + 𝑘 ∈ 𝑋 | be the number of pairs at distance 𝑘, 𝑉2 ( 𝑋 ) := | 𝑥 ∈ 𝑋 : 𝑥 ± 1 ∈ 𝑋 | be the number of interior points, and 𝐼 ( 𝑋 ) be the isolated points . Let 𝑋 ⊂ ℤ. We will employ the following three facts: 1. 𝐼 ( 𝑋 ) + 2 𝑁1 ( 𝑋 ) = | 𝑋 | + 𝑉2 ( 𝑋 ), by partitioning elements by neighbor count. Í 2. 4 𝑁1 ( 𝑋 ) + 𝑁3 ( 𝑋 ) ≤ 3| 𝑋 | + 2 𝑁2 ( 𝑋 ), which follows from writing 𝑁𝑘 ( 𝑥 ) = 𝑥 ∈ℤ 1𝑋 ( 𝑥 )1𝑋 ( 𝑥 + 𝑘) and a pointwise check of the indicator function 1 𝑋 across all 4-point windows ( 𝑥, 𝑥 + 1, 𝑥 + 2, 𝑥 + 3); that is, summing the local inequality 1𝑋 ( 𝑥 ) + 1𝑋 ( 𝑥 + 1) + 1𝑋 ( 𝑥 + 2) + 1𝑋 ( 𝑥 )1𝑋 ( 𝑥 + 2) + 1𝑋 ( 𝑥 + 1)1𝑋 ( 𝑥 + 3) ≥ 1𝑋 ( 𝑥 )1𝑋 ( 𝑥 + 1) + 21𝑋 ( 𝑥 + 1)1𝑋 ( 𝑥 + 2) + 1𝑋 ( 𝑥 + 2)1𝑋 ( 𝑥 + 3) + 1𝑋 ( 𝑥 )1𝑋 ( 𝑥 + 3) and then summing over all 𝑥 ∈ ℤ. 3. 2 𝑁2 ( 𝑋 ) ≤ 𝑁3 ( 𝑋 ) + 2𝑉2 ( 𝑋 ) + 2 𝐼 ( 𝑋 ). Consider each pair ( 𝑥, 𝑥 + 2) ∈ 𝑋 2 and we proceed by cases on 𝑥 + 1. Let 𝐺 = { 𝑥 ∈ 𝑋 | 𝑥 + 1 ∉ 𝑋 ∧ 𝑥 + 2 ∈ 𝑋 }. If 𝑥 + 1 ∈ 𝑋 , then the pair is counted exactly by 𝑉2 , so 𝑁2 ( 𝑋 ) = 𝑉2 ( 𝑋 ) + |𝐺 |. If 𝑥 + 1 ∉ 𝑋 , then • If 𝑥 − 1 ∈ 𝑋 , then ( 𝑥 − 1, 𝑥 + 2) is a pair counted in 𝑁3 ( 𝑋 ). • If 𝑥 + 3 ∈ 𝑋 , then ( 𝑥, 𝑥 + 3) is a pair counted in 𝑁3 ( 𝑋 ).

41

Advancing Mathematics Research with AI-Driven Formal Proof Search

• If 𝑥 − 1 ∉ 𝑋 , then 𝑥 is an isolated point in 𝐼 ( 𝑋 ), and if 𝑥 + 3 ∉ 𝑋 , then 𝑥 + 2 is an isolated point in 𝐼 ( 𝑋 ).

Since each 𝑁3 pair can be counted by two different gaps, while isolated points are distinct in this construction, we have 2| 𝐺 | ≤ 𝑁3 ( 𝑋 ) + 2 𝐼 ( 𝑋 ). Next, for each 𝑘 ≥ 1, count quadruples ( 𝑎, 𝑏, 𝑐, 𝑑 ) ∈ 𝐴4 with 𝑎 + 𝑏 + 𝑘 = 𝑐 + 𝑑 . Rewriting as 𝑎 − 𝑐 = 𝑑 − 𝑏 − 𝑘 and partitioning by 𝛿 = 𝑎 − 𝑐 yields the following two quadruple transfer bounds: 1. The cases 𝛿 = 0 and 𝛿 = −𝑘 each contribute ≤ | 𝐴 | (one coordinate determines the rest). For any 𝛿 ∉ {0, −𝑘 }, the Sidon property ensures that there is at most one pair ( 𝑎, 𝑐) with 𝑎 − 𝑐 = 𝛿 and at most one pair ( 𝑑, 𝑏) with 𝑑 − 𝑏 = 𝛿 + 𝑘. Consequently, each gap of size 𝑘 in 𝐷 identifies exactly one quadruple. Thus |quad𝑘 | ≤ 𝑁𝑘 ( 𝐷) + 2𝑛. 2. Each "good" element 𝑠 ∈ 𝑆 with 𝑠 + 𝑘 ∈ 𝑆 (excluding ≤ 2𝑛 doubles of the form 2𝑎) produces ≥ 4 quadruples, giving 4 𝑁𝑘 ( 𝑆) ≤ |quad𝑘 | + 8𝑛. Combining these bounds shows that 𝑁𝑘 ( 𝐷) and 𝑁𝑘 ( 𝑆) are related up to 𝑂 ( 𝑛) error. Applying fact (2) to 𝐷 = 𝐴 − 𝐴 gives 4 𝑁1 ( 𝐷) + 𝑁3 ( 𝐷) ≤ 3| 𝐷 | + 2 𝑁2 ( 𝐷)

and then substitute the above two quadruple transfer bounds for 𝑘 = 1, 2, 3 and collecting all 𝑂 ( 𝑛) terms gives 16 𝑁1 ( 𝑆) + 4 𝑁3 ( 𝑆) ≤ 3| 𝐷 | + 8 𝑁2 ( 𝑆) + 100𝑛

Then, using fact (3) on 𝑆 we obtain

16 𝑁1 ( 𝑆) + 4 𝑁3 ( 𝑆) ≤ 3| 𝐷 | + (4 𝑁3 ( 𝑆) + 8𝑉2 ( 𝑆) + 8 𝐼 ( 𝑆)) + 100𝑛

and notice that the 4 𝑁3 ( 𝑆) terms cancel. Then applying fact (1) we obtain (8| 𝑆 | + 8𝑉2 ( 𝑆) − 8 𝐼 ( 𝑆)) ≤ 3| 𝐷 | + 8𝑉2 ( 𝑆) + 8 𝐼 ( 𝑆) + 100𝑛

and see that the 8𝑉2 ( 𝑆) terms now cancel, leaving

16 𝐼 ( 𝑆) + 100𝑛 ≥ 8| 𝑆 | − 3| 𝐷 | .

The standard Sidon estimates | 𝑆 | ≥ 𝑛2 /2 and | 𝐷 | ≤ 𝑛2 then give 16 𝐼 ( 𝑆)+100𝑛 ≥ 4𝑛2 −3𝑛2 = 𝑛2 , accounting for a boundary correction of +16 at zero yields (★). □ We include the Lean proof at https://github.com/google-deepmind/alphapro of-nexus-results/blob/main/APNOutputs/ErdosProblems/erdos_152.lean. OEIS Conjectures Theorem. (A conjecture of OEIS A051293, 2002) Let 𝑎𝑛 denote the number of nonempty subsets of {1, 2, 3, . . . , 𝑛} whose elements have an integer average. Then    2𝑛+1 1 3 13 75 541 1 𝑎𝑛 = 1+ + 2 + 3 + 4 + 5 +𝑜 5 𝑛

𝑛

𝑛

𝑛

𝑛

𝑛

𝑛

42

Advancing Mathematics Research with AI-Driven Formal Proof Search

Proof. A subset 𝑆 ⊆ {1, 2, . . . , 𝑛} has an integer average if and only if the sum of its elements is divisible by its cardinality | 𝑆 |. Let 𝑁 ( 𝑛, 𝑘) denote the number of subsets of size 𝑘 whose sum is Í divisible by 𝑘. We can express the total number of such subsets as 𝑎𝑛 = 𝑛𝑘=1 𝑁 ( 𝑛, 𝑘) To isolate the condition that 𝑘 divides  sum of the elements in 𝑆, we utilize the orthogonalityÍof roots  the 2𝜋𝑖 𝑗 −1 𝑁 𝜔 𝑘, 𝑗 of unity. Let 𝜔𝑘, 𝑗 = exp 𝑘 . By the standard orthogonality relation, the sum 1𝑘 𝑘𝑗=0 equals 1 Íif 𝑘 divides 𝑁 , and 0 otherwise. Thus, the indicator function for divisibility by 𝑘 is
1 Í𝑘−1 𝑠 ∈𝑆 𝑠 . Summing this over all 𝑛𝑘 subsets of size 𝑘 yields 𝑗=0 𝜔 𝑘, 𝑗 𝑘 𝑁 ( 𝑛, 𝑘) =

1 ∑︁ ∑︁ 𝑘−1

𝑘

Í

𝜔 𝑘, 𝑠𝑗∈𝑆

𝑠

𝑗=0 | 𝑆 |=𝑘

We isolate the principal term corresponding to 𝑗 = 0, which evaluates trivially to 1𝑘 𝑛𝑘 . Let the remainder term be 𝑅𝑛,𝑘 , defined as 𝑅𝑛,𝑘 =

1 ∑︁ ∑︁ 𝑘−1

𝑘

Í

𝜔 𝑘, 𝑠𝑗∈𝑆

𝑠

𝑗=1 | 𝑆 |=𝑘

Thus, 𝑁 ( 𝑛, 𝑘) = 1𝑘 𝑛𝑘 + 𝑅𝑛,𝑘 . Summing over all possible subset sizes 𝑘, we obtain 𝑎𝑛 =

  𝑛 ∑︁ 1 𝑛 𝑘=1

𝑘 𝑘

+

𝑛 ∑︁

𝑅𝑛,𝑘

𝑘=1

Í Í 𝑗 Using the well-known identity 𝑛𝑘=1 1𝑘 𝑛𝑘 = 𝑛𝑗=1 2 −1 , we separate this into two sums: 𝑆𝑛 = 𝑗 Í𝑛 2 𝑗 Í𝑛 1 𝑗=1 𝑗 and the harmonic number 𝐻𝑛 = 𝑗=1 𝑗 . This yields our fundamental decomposition 𝑎𝑛 = 𝑆𝑛 − 𝐻𝑛 +

𝑛 ∑︁

𝑅𝑛,𝑘

𝑘=1

Í𝑛 Next, we establish that the sum of the remainders 𝑘=1 𝑅 𝑛,𝑘 is asymptotically negligible. Í Í 𝑠 Consider the inner sum |𝑆 |=𝑘 𝜔𝑘, 𝑠𝑗∈𝑆 . This sum is exactly the coefficient of 𝑧 𝑘 in the polynomial Î𝑛 𝑚 𝑃𝑛,𝑘, 𝑗 ( 𝑧 ) = 𝑚=1 (1 + 𝑧𝜔 𝑘, 𝑗 ). By standard coefficient bounds, the magnitude of the 𝑘-th coefficient of a polynomial is bounded by its maximum modulus on the unit circle | 𝑧 | = 1: ∑︁ | 𝑆 |=𝑘

Í

𝜔 𝑘, 𝑠𝑗∈ 𝑆

𝑠

≤ max | 𝑧 |=1

𝑛 Ö 𝑚=1

𝑚 |1 + 𝑧𝜔 𝑘, 𝑗|

𝑚 For a fixed 𝑘 and 𝑗 ∈ {1, . . . , 𝑘 − 1}, the sequence of roots 𝜔𝑘, is periodic with period 𝑗 𝐿 = gcd(𝑘 𝑗,𝑘) ≥ 2. The product over a full period 𝐿 can be evaluated algebraically: the roots of Î 𝐴+𝐿−1 𝑚 𝐿 𝑋 𝐿 − 1 dictate that 𝑚 =𝐴 (1 + 𝑧𝜔 𝑘, 𝑗 ) = 1 − (− 𝑧 ) . For any 𝑧 on the unit circle, the magnitude |1 − (− 𝑧) 𝐿 | is strictly bounded by 2. When taking the product over all 𝑛 terms, we group them into ⌊ 𝑛/ 𝐿⌋ full periods, leaving 𝑛 mod 𝐿 residual terms. For | 𝑧 | = 1, each full period 𝑚 contributes at most a factor of 2, and by the triangle inequality |1 + 𝑧𝜔 𝑘, | ≤ 2, each residual 𝑗 term also contributes at most a factor of 2. Therefore, the total product is bounded by 43

Advancing Mathematics Research with AI-Driven Formal Proof Search

2 ⌊𝑛/𝐿⌋+( 𝑛 mod 𝐿) . Because 𝐿 ≥ 2, we have ⌊ 𝑛/ 𝐿⌋ + ( 𝑛 mod 𝐿) ≤ 2𝑛 + 1. Thus, for any 𝑧 on the unit circle, we have 𝑛 | 𝑃𝑛,𝑘, 𝑗 ( 𝑧)| ≤ 2 2 +1 = 2 · 2𝑛/2

Consequently, the magnitude of the coefficient is bounded by 2 · 2𝑛/2 . Applying this to our remainder definition yields | 𝑅𝑛,𝑘 | ≤ 𝑘−1 2 · 2𝑛/2 ≤ 2 · 2𝑛/2 . Summing over 𝑘 ∈ {1, . . . , 𝑛} gives 𝑘 the strict bound 𝑛 ∑︁ 𝑅𝑛,𝑘 ≤ 2𝑛2𝑛/2 𝑘=1

Í 𝑗 We must now evaluate the asymptotics of 𝑆𝑛 = 𝑛𝑗=1 2𝑗 . We propose the asymptotic approximation 𝑓𝑛 , defined as   2𝑛+1 𝑃 ( 𝑛) 2𝑛+1 1 3 13 75 541 𝑓𝑛 = 1+ + 2 + 3 + 4 + 5 = 6 𝑛

𝑛

𝑛

𝑛

𝑛

𝑛

𝑛

where 𝑃 ( 𝑛) = 𝑛5 + 𝑛4 + 3𝑛3 + 13𝑛2 + 75𝑛 + 541. To demonstrate that 𝑓𝑛 is a highly accurate approximation of 𝑆𝑛 , we analyze the discrepancy in their consecutive differences. Let 𝐸 𝑗 be the discrete derivative error given by 𝐸 𝑗 = 𝑓 𝑗 − 𝑓 𝑗−1 −

2𝑗 𝑗

Í By telescoping summation, 𝑆𝑛 − 𝑓𝑛 = 𝑆1 − 𝑓1 − 𝑛𝑗=2 𝐸 𝑗 . To bound 𝐸 𝑗 , we expand 𝑓 𝑗 − 𝑓 𝑗−1 algebraically to obtain   2 𝑗 2 𝑗 2 𝑃 ( 𝑗)( 𝑗 − 1) 6 − 𝑃 ( 𝑗 − 1) 𝑗6 − 𝑗5 ( 𝑗 − 1) 6 𝑓 𝑗 − 𝑓 𝑗−1 − = 𝑗 𝑗6 ( 𝑗 − 1) 6 Let 𝐴 ( 𝑥 ) = 2 𝑃 ( 𝑥 )( 𝑥 − 1) 6 − 𝑃 ( 𝑥 − 1) 𝑥 6 − 𝑥 5 ( 𝑥 − 1) 6 . Expanding 𝐴 ( 𝑥 ) leaves a polynomial of strictly degree 5: 𝐴 ( 𝑥 ) = −4683 𝑥 5 + 13586 𝑥 4 − 19540 𝑥 3 + 15356 𝑥 2 − 6342 𝑥 + 1082

In particular, it is easy to show that | 𝐴 ( 𝑗)| ≤ 100000 𝑗5 for 𝑗 ≥ 2. Substituting this back into the error term yields 100000 · 2 𝑗 |𝐸 𝑗| ≤ 7 𝑗

Í Summing these errors up to 𝑛, the sum is dominated by its largest terms, giving 𝑛𝑗=2 | 𝐸 𝑗 | =  𝑛 Í O 2𝑛7 . Recall our decomposition 𝑎𝑛 = 𝑓𝑛 + ( 𝑆𝑛 − 𝑓𝑛 ) − 𝐻𝑛 + 𝑛𝑘=1 𝑅𝑛,𝑘 . To prove the theorem,  𝑛+1  it suffices to show that the combined error terms are 𝑜 2𝑛6 :  𝑛+1  2 = 𝑜 . 6 𝑛7  𝑛+1  𝑛 2. 𝐻𝑛 ∼ ln 𝑛 = 𝑜 2𝑛6 .  𝑛+1  Í 3. 𝑅𝑛,𝑘 ≤ 2𝑛2𝑛/2 = 𝑜 2𝑛6 .

1. 𝑆𝑛 − 𝑓𝑛 = O

2

 𝑛

44

Advancing Mathematics Research with AI-Driven Formal Proof Search

Since all residual terms are bounded by 𝑜 𝑎𝑛 = 𝑓𝑛 + 𝑜

 𝑛+1  2 𝑛6

=

2𝑛+1 𝑛



 𝑛+1 

2

𝑛6

, we conclude that

1

3

1+

𝑛

+

𝑛2

+

13 𝑛3

+

75

+

𝑛4

541 𝑛5

+𝑜



1



𝑛5

This establishes the conjectured asymptotic expansion.

□

Í 𝑚
2 𝑚+ 𝑘
2 Theorem. (A conjecture of OEIS A228143, 2018) Let 𝑠𝑚 = 𝑚 be the sequence 𝑘=0 𝑘 𝑘 A005259. Let 𝑎𝑛 denote the determinant of the ( 𝑛 + 1) × ( 𝑛 + 1) Hankel-type matrix whose Í 𝑛 2 ( 𝑖, 𝑗)-entry is 𝑠𝑖+ 𝑗 for all 𝑖, 𝑗 = 0, . . . , 𝑛. Let 𝐴 ( 𝑥 ) = ∞ 𝑛=0 𝑎𝑛 𝑥 = 1 + 48 𝑥 + 161856 𝑥 + . . . 1/8 denote the ordinary generating function of 𝑎𝑛 . Then 𝐴 ( 𝑥 /3) has integer coefficients. Proof. We proceed in three main stages: analyzing the matrix entries modulo 3, analyzing them modulo 4, and using the resulting divisibility properties of the determinant 𝑎𝑛 to construct the required eighth root as a formal power series over the integers.

First, we determine the residues of 𝑠𝑚 modulo 3.
By writing 𝑘 in base 3, Kummer’s Theorem dictates that the highest power of 3 dividing 2𝑘𝑘 equals the number of carries when
evaluating 𝑘 + 𝑘 in base 3. If 𝑘 contains the digit 2, a carry occurs, so 2𝑘𝑘 ≡ 0 (mod 3). Alternatively, if 𝑘 consists only
of the digits 0 and 1, there
are no carries.
Applying Lucas’s Theorem digit-by-digit to 2𝑘𝑘 yields a product of terms 00 = 1 and 21 = 2 ≡ −1 (mod 3).
Thus, 2𝑘𝑘 ≡ (−1) 𝑐 (mod 3), where 𝑐 is the number of 1s in the base-3 representation of 𝑘.
Since 𝑐 shares the same parity as 𝑘, we obtain 2𝑘𝑘 ≡ (−1) 𝑘 (mod 3). We can rewrite the squared product of binomial coefficients as: 𝑚 𝑘

  

𝑚+𝑘 𝑘

 2

𝑚+𝑘 = 2𝑘



2 

2𝑘

2

𝑘

When 2𝑘𝑘 . 0 (mod 3), the base-3 digits of 2𝑘 are strictly 0s and 2s. Applying Lucas’s


Theorem to 𝑚2+𝑘𝑘 , each digit of the evaluation takes the form 𝑑0𝑖 = 1 or 𝑑2𝑖 ∈ {0, 1}. Thus,
2
𝑚+ 𝑘
in {0, 1} are invariant under squaring, 𝑚2+𝑘𝑘 ≡ 𝑚2+𝑘𝑘 2𝑘 ≡ 0 or 1 (mod 3). Since values
(mod 3). Furthermore, since 2𝑘𝑘 ∈ {0, (−1) 𝑘 } (mod 3), squaring it absorbs the parity:
2𝑘
2 𝑘 2𝑘 ≡ (−1) (mod 3). Combining these pieces, we find that for all 𝑚 and 𝑘: 𝑘 𝑘 𝑚 𝑘

  

𝑚+𝑘 𝑘

 2

≡ (−1)

𝑘



𝑚+𝑘 2𝑘



2𝑘 𝑘



≡ (−1)

𝑘

𝑚 𝑘

 

𝑚+𝑘 𝑘



(mod 3)

Í Summing this equivalence over 𝑘 = 0, . . . , 𝑚 yields 𝑠𝑚 ≡ 𝑚 (−1) 𝑘 𝑚𝑘 𝑚𝑘+𝑘 (mod 3). By 𝑘 =0

Í 𝑘 𝑚 𝑚+ 𝑘 a standard alternating binomial sum identity, 𝑚 = (−1) 𝑚 . Consequently, 𝑘=0 (−1) 𝑘 𝑘 𝑠𝑚 ≡ (−1) 𝑚 (mod 3).

Using this congruence, we apply row operations to the matrix 𝑀 ( 𝑛) to establish that 3𝑛 | 𝑎𝑛 . Let 𝑃𝑛 be the lower-triangular matrix with ones on the main diagonal, 𝑃 𝑖,0 = −(−1) 𝑖 for 𝑖 ≥ 1, and zeros elsewhere. The matrix product 𝑃𝑛 𝑀 ( 𝑛) replaces each row 𝑖 ≥ 1 with the 𝑖-th row

45

Advancing Mathematics Research with AI-Driven Formal Proof Search

minus (−1) 𝑖 times the 0-th row. Visually, the modified matrix takes the form:  𝑠0 𝑠1 𝑠2   𝑠1 + 𝑠0 𝑠2 + 𝑠1 𝑠3 + 𝑠2   𝑠2 − 𝑠0 ( 𝑛) 𝑠3 − 𝑠1 𝑠4 − 𝑠2 𝑃𝑛 𝑀 =   .. .. ..  . . .  𝑠𝑛 − (−1) 𝑛 𝑠0 𝑠𝑛+1 − (−1) 𝑛 𝑠1 𝑠𝑛+2 − (−1) 𝑛 𝑠2 

··· ··· ···

𝑠𝑛

  𝑠𝑛+1 + 𝑠𝑛  𝑠𝑛+2 − 𝑠𝑛   .. ..  . .  𝑛  · · · 𝑠2𝑛 − (−1) 𝑠𝑛 

The new ( 𝑖, 𝑗)-entry for 𝑖 ≥ 1 is 𝑠𝑖+ 𝑗 − (−1) 𝑖 𝑠 𝑗 . By our previous congruence, 𝑠𝑖+ 𝑗 − (−1) 𝑖 𝑠 𝑗 ≡ (−1) 𝑖+ 𝑗 − (−1) 𝑖 (−1) 𝑗 ≡ 0 (mod 3). Thus, every entry in rows 1 through 𝑛 of the new matrix is divisible by 3. Factoring a 3 out of each of these 𝑛 rows gives a factor of 3𝑛 . Because det( 𝑃𝑛 ) = 1, we conclude that 3𝑛 | det( 𝑀 ( 𝑛) ) = 𝑎𝑛 .

Second, we analyze 𝑠𝑚 modulo 4. For any 𝑘 ≥ 1, the product 𝑚𝑘 𝑚𝑘+𝑘 is always even, 

2 which implies its square is divisible by 4. Thus, 𝑚𝑘 𝑚𝑘+𝑘 ≡ 0 (mod 4) for all 𝑘 ≥ 1. The 𝑘 = 0 term evaluates to 1, yielding 𝑠𝑚 ≡ 1 (mod 4) for all 𝑚.

We apply a similar matrix transformation to establish divisibility by 4𝑛 . Let 𝑃𝑛′ be the lower-triangular matrix with ones on the diagonal, 𝑃′𝑖,0 = −1 for 𝑖 ≥ 1, and zeros elsewhere. The product 𝑃𝑛′ 𝑀 ( 𝑛) subtracts the 0-th row from every subsequent row 𝑖 ≥ 1:  𝑠0 𝑠1  𝑠1 − 𝑠0 𝑠2 − 𝑠1  𝑃𝑛′ 𝑀 ( 𝑛) = 𝑠 − 𝑠 𝑠 − 𝑠 2 0 3 1  .. ..  . . 

 ··· 𝑠𝑛  · · · 𝑠𝑛+1 − 𝑠𝑛  · · · 𝑠𝑛+2 − 𝑠𝑛   .. ..  . . 

For 𝑖 ≥ 1, the ( 𝑖, 𝑗)-entry becomes 𝑠𝑖+ 𝑗 − 𝑠 𝑗 . Since 𝑠𝑚 ≡ 1 (mod 4) for all 𝑚, this difference evaluates to 1 − 1 ≡ 0 (mod 4). Factoring 4 out of the 𝑛 modified rows shows that 4𝑛 | det( 𝑀 ( 𝑛) ) = 𝑎𝑛 .

Now we combine these divisibility properties. We explicitly compute 𝑎1 = 48. For 𝑛 ≥ 1, we know 4𝑛 | 𝑎𝑛 , and since 4𝑛 ≥ 16 for 𝑛 ≥ 2, it follows that 16 | 𝑎𝑛 for all 𝑛 ≥ 1 (as 16 | 48 for 𝑛 = 1). Because 16 and 3𝑛 are coprime, their respective divisibilities imply 16 · 3𝑛 | 𝑎𝑛 for all 𝑛 ≥ 1. Í 𝑎𝑛 𝑛 𝑛 We consider the scaled generating function 𝐴 ( 𝑥 /3) = ∞ 𝑛=0 3𝑛 𝑥 . Let 𝑏𝑛 = 𝑎𝑛 /3 denote the coefficients of this series. Since 𝑎0 = 1, we have 𝑏0 = 1. For 𝑛 ≥ 1, our divisibility result Í 𝑛 yields 16 | 𝑏𝑛 . Therefore, we can write 𝐴 ( 𝑥 /3) = 1 + 16𝑌 ( 𝑥 ), where 𝑌 ( 𝑥 ) = ∞ 𝑛=1 𝑦𝑛 𝑥 is a formal power series with integer coefficients and zero constant term (𝑌 (0) = 0). Finally, we construct the eighth root 𝐶 ( 𝑥 ) = 𝐴 ( 𝑥 /3) 1/8 ∈ ℤ⟦ 𝑥 ⟧. We seek a series of the form 𝐶 ( 𝑥 ) = 1 + 2 𝑋 ( 𝑥 ) where 𝑋 ( 𝑥 ) ∈ ℤ⟦𝑥 ⟧ has no constant term. Expanding the eighth power yields (1 + 2 𝑋 ( 𝑥 )) 8 = 1 + 16 𝑋 ( 𝑥 ) + 112 𝑋 ( 𝑥 ) 2 + 448 𝑋 ( 𝑥 ) 3 + 1120 𝑋 ( 𝑥 ) 4

+ 1792 𝑋 ( 𝑥 ) 5 + 1792 𝑋 ( 𝑥 ) 6 + 1024 𝑋 ( 𝑥 ) 7 + 256 𝑋 ( 𝑥 ) 8

Factoring out 16 from the higher degree terms, we define the polynomial

𝑃 ( 𝑋 ) = 7 𝑋 2 + 28 𝑋 3 + 70 𝑋 4 + 112 𝑋 5 + 112 𝑋 6 + 64 𝑋 7 + 16 𝑋 8 46

Advancing Mathematics Research with AI-Driven Formal Proof Search

Thus, (1 + 2 𝑋 ( 𝑥 )) 8 = 1 + 16( 𝑋 ( 𝑥 ) + 𝑃 ( 𝑋 ( 𝑥 ))). To satisfy 𝐶 ( 𝑥 ) 8 = 𝐴 ( 𝑥 /3), we must solve the equation 1 + 16( 𝑋 ( 𝑥 ) + 𝑃 ( 𝑋 ( 𝑥 ))) = 1 + 16𝑌 ( 𝑥 ), which simplifies to 𝑋 ( 𝑥 ) + 𝑃 ( 𝑋 ( 𝑥 )) = 𝑌 ( 𝑥 ). Í 𝑛 We determine the coefficients 𝑥𝑛 of 𝑋 ( 𝑥 ) = ∞ 𝑛=1 𝑥 𝑛 𝑥 inductively. We set 𝑥0 = 0. For the 𝑛+1 inductive step, the coefficient of 𝑥 in the equation is 𝑥𝑛+1 + [ 𝑥 𝑛+1 ] 𝑃 ( 𝑋 ( 𝑥 )) = 𝑦𝑛+1

Because every term in 𝑃 ( 𝑋 ) has degree at least 2, and 𝑋 ( 𝑥 ) has no constant term, the 𝑥 𝑛+1 coefficient of 𝑃 ( 𝑋 ( 𝑥 )) depends only on the terms 𝑥1 , . . . , 𝑥𝑛 . Therefore, we can uniquely solve for the integers 𝑥𝑛+1 as ! 𝑛 ∑︁ 𝑥𝑛+1 = 𝑦𝑛+1 − [ 𝑥 𝑛+1 ] 𝑃 𝑥𝑘 𝑥 𝑘 𝑘=1

This well-defined recurrence provides an integer sequence ( 𝑥𝑛 )𝑛≥1 giving a formal power series 𝑋 ( 𝑥 ) ∈ ℤ⟦𝑥 ⟧ that satisfies 𝑋 ( 𝑥 ) + 𝑃 ( 𝑋 ( 𝑥 )) = 𝑌 ( 𝑥 ). Substituting this back into our expansion yields (1 + 2 𝑋 ( 𝑥 )) 8 = 1 + 16𝑌 ( 𝑥 ) = 𝐴 ( 𝑥 /3). Setting 𝐶 ( 𝑥 ) = 1 + 2 𝑋 ( 𝑥 ), we have established the existence of the desired integer power series 𝐶 ( 𝑥 ) = 𝐴 ( 𝑥 /3) 1/8 . □

These OEIS problems were added as conjectures in 2022 (https://oeis.org/A0512 93) and 2018 (https://oeis.org/A228143). Though neither problem has likely received much attention, the ability to provide a guarantee on the correctness of the statement that an expert conjectured serves value. For example, it appears that a good part of the work is done in identifying the asymptotic formula to be conjectured in OEIS A051293. In this case, ensuring the formula holds with a rigorous proof is a matter of validating intuition without carrying out potentially tedious proof steps, which our agent can handle. The Lean proofs for the two problems can be found at https://github.com/google-deepmind/alphap roof-nexus-results/blob/main/APNOutputs/OEIS. A variant of the Graph Reconstruction Conjecture

The Kelly-Ulam graph reconstruction program aims to recover a graph from its deck of one-vertex-deleted subgraphs [62, 36]. A standard bipartite version was formulated by Bondy and Hemminger as the problem of showing that bipartite graphs are reconstructible [10]. The following theorem proves a structured incidence-deletion analogue under strong type-distinguishability assumptions. Terminology Let Ω = 𝐿 ⊔ 𝑅 be a finite vertex set with a partition into the disjoint parts 𝐿, 𝑅 ⊆ Ω. A graph 𝐾 is bipartite with respect to ( 𝐿, 𝑅) if every edge of 𝐾 has one endpoint in 𝐿 and one endpoint in 𝑅. We say 𝐾 is 2-connected if 𝐾 is connected and, for every vertex 𝑣, the induced graph on Ω \ { 𝑣} is connected. For a graph 𝐾 and a vertex 𝑣, write 𝐾 \inc 𝑣 for the graph obtained from 𝐾 by deleting all edges incident to 𝑣, while leaving the vertex set unchanged. Thus 𝐸 ( 𝐾 \inc 𝑣) = { 𝑥 𝑦 ∈ 𝐸 ( 𝐾 ) : 𝑥 ≠ 𝑣, 𝑦 ≠ 𝑣} .

A bipartite isomorphism 𝐾  𝐵 𝐾 ′ is a graph isomorphism whose underlying bijection preserves both parts 𝐿 and 𝑅. The bipartite deck is the multiset D 𝐵 ( 𝐾 ) := {{[ 𝐾 \inc 𝑣] 𝐵 : 𝑣 ∈ Ω }},

47

Advancing Mathematics Research with AI-Driven Formal Proof Search

where [·] 𝐵 denotes bipartite-isomorphism class. Let 𝑁 𝐾 ( 𝑥 ) be the neighbor set of 𝑥 in 𝐾 . The degree profile and type of 𝑥 are 𝑃 𝐾 ( 𝑥 ) := {{deg 𝐾 ( 𝑦 ) : 𝑦 ∈ 𝑁 𝐾 ( 𝑥 )}},

𝜏 𝐾 ( 𝑥 ) := (deg 𝐾 ( 𝑥 ) , 𝑃 𝐾 ( 𝑥 )) .

The type profile of 𝑢 is the multiset of the types of its neighbors: 𝑇𝐾 ( 𝑢) := {{𝜏 𝐾 ( 𝑥 ) : 𝑥 ∈ 𝑁 𝐾 ( 𝑢)}} .

Finally, for a type 𝑡 = ( 𝑑, 𝑀 ) ∈ ℕ × Multiset(ℕ) and 𝑎 ∈ ℕ, define 𝐹𝑎 ( 𝑡 ) := (max( 𝑑 − 1, 0) , 𝑀 \ { 𝑎}) ,

where 𝑀 \ { 𝑎} means deletion of one occurrence of 𝑎 from the multiset 𝑀 . In the applications below, 𝐹𝑎 is applied to neighbor-types, whose first coordinate is positive, so max( 𝑑 − 1, 0) = 𝑑 − 1 there. We write #𝑡 𝑀 for the multiplicity of 𝑡 in a multiset 𝑀 .

Theorem (Weak bipartite graph reconstruction) Let 𝐺 and 𝐻 be finite simple graphs on the same finite vertex set Ω, both bipartite with respect to the same parts Ω = 𝐿 ⊔ 𝑅 and | Ω | ≥ 3. Assume that 𝐺 is 2-connected and all vertex types of 𝐺 are pairwise distinct, that is, 𝜏𝐺 ( 𝑥 ) ≠ 𝜏𝐺 ( 𝑦 ) if 𝑥 ≠ 𝑦 . If D 𝐵 ( 𝐺 ) = D 𝐵 ( 𝐻 ), then 𝐺 and 𝐻 are bipartite-isomorphic.

Proof. Write 𝑛 = | Ω | and 𝑒 ( 𝐾 ) = | 𝐸 ( 𝐾 )|. Since bipartite isomorphisms preserve edge counts, the deck determines the multiset

For every vertex 𝑣,

{{ 𝑒 ( 𝐾 \inc 𝑣) : 𝑣 ∈ Ω }} . 𝑒 ( 𝐾 \inc 𝑣) + deg 𝐾 ( 𝑣) = 𝑒 ( 𝐾 ) ,

because 𝐾 \inc 𝑣 removes exactly the edges incident to 𝑣. Also, ∑︁ 𝑒 ( 𝐾 \inc 𝑣) = ( 𝑛 − 2) 𝑒 ( 𝐾 ) ,

(1) (2)

𝑣∈ Ω

because each edge of 𝐾 remains in precisely the cards indexed by the 𝑛 − 2 vertices not incident to that edge. Since 𝑛 ≥ 3, equation (2) shows that the deck determines 𝑒 ( 𝐾 ). Applying this to the equal decks of 𝐺 and 𝐻 gives 𝑒 (𝐺) = 𝑒 ( 𝐻 ) ,

(3)

and then equation (1) shows that the degree multisets of 𝐺 and 𝐻 are equal. Equality of the two decks also gives a bijection 𝑓 : Ω → Ω such that, for every 𝑣 ∈ Ω, there is a bipartite isomorphism 𝜙𝑣 : 𝐺 \inc 𝑣  𝐵 𝐻 \inc 𝑓 ( 𝑣) .

(4)

deg𝐺 ( 𝑣) = deg 𝐻 ( 𝑓 ( 𝑣))

(5)

For this matched pair of cards, edge counts are equal. Combining this with (1) and (3) yields

for every 𝑣.

48

Advancing Mathematics Research with AI-Driven Formal Proof Search

Next, 𝐺 has minimum degree at least 2. Indeed, if a vertex had degree 0, then 𝐺 would not be connected; if a vertex 𝑥 had the unique neighbor 𝑦 , then the induced graph on Ω \ { 𝑦 } would contain the isolated vertex 𝑥 , contradicting 2-connectivity. Since the degree multisets of 𝐺 and 𝐻 are equal, 𝐻 also has minimum degree at least 2. Therefore, in any graph 𝐾 with minimum degree at least 2, the card 𝐾 \inc 𝑣 has a unique isolated vertex, namely 𝑣. Indeed, the vertex 𝑣 is isolated because all its incident edges have been removed. On the other hand, if 𝑥 ≠ 𝑣, then 𝑥 has at least two neighbors in 𝐾 , at most one of which is 𝑣; hence 𝑥 has a neighbor 𝑦 ≠ 𝑣, and the edge 𝑥 𝑦 remains in 𝐾 \inc 𝑣.

Applying this uniqueness to (4), the isomorphism 𝜙𝑣 sends the unique isolated vertex of 𝐺 \inc 𝑣 to the unique isolated vertex of 𝐻 \inc 𝑓 ( 𝑣). Hence

(6)

𝜙𝑣 ( 𝑣) = 𝑓 ( 𝑣) .

Since 𝜙𝑣 preserves 𝐿 and 𝑅, (6) implies that 𝑓 preserves the two parts: 𝑣 ∈ 𝐿 ⇐⇒ 𝑓 ( 𝑣) ∈ 𝐿,

𝑣 ∈ 𝑅 ⇐⇒ 𝑓 ( 𝑣) ∈ 𝑅.

(7)

We now prove that 𝑓 preserves vertex types. It remains, in view of (5), to compare degree profiles. For a graph 𝐾 and vertex 𝑣, put 𝐴 𝐾 ( 𝑘) := #{ 𝑥 ∈ Ω : deg 𝐾 ( 𝑥 ) = 𝑘 },

and

𝐵 𝐾,𝑣 ( 𝑘) := #{ 𝑥 ∈ Ω : deg 𝐾 \inc 𝑣 ( 𝑥 ) = 𝑘 }, 𝐶 𝐾,𝑣 ( 𝑘) := #{ 𝑥 ∈ 𝑁 𝐾 ( 𝑣) : deg 𝐾 ( 𝑥 ) = 𝑘 } .

Counting vertices of degree 𝑘 before and after deleting the incidence set of 𝑣 gives, for every 𝑘 ≥ 0, 𝐶 𝐾,𝑣 ( 𝑘 + 1) + 𝐴 𝐾 ( 𝑘) + 1𝑘=0 = 𝐶 𝐾,𝑣 ( 𝑘) + 𝐵 𝐾,𝑣 ( 𝑘) + 1deg𝐾 ( 𝑣)=𝑘 . (8)

Indeed, in 𝐾 \inc 𝑣, every non-neighbor of 𝑣 keeps its degree, while every neighbor of 𝑣 has its degree lowered by 1. Hence the vertices of degree 𝑘 in 𝐾 \inc 𝑣 are precisely the old non-neighbors of degree 𝑘, the old neighbors of degree 𝑘 + 1, and additionally 𝑣 itself if 𝑘 = 0. Therefore 𝐵 𝐾,𝑣 ( 𝑘) = 𝐴 𝐾 ( 𝑘) − 𝐶 𝐾,𝑣 ( 𝑘) − 1deg𝐾 ( 𝑣)=𝑘 + 𝐶 𝐾,𝑣 ( 𝑘 + 1) + 1𝑘=0 . Since the global degree multisets are equal, 𝐴𝐺 ( 𝑘) = 𝐴 𝐻 ( 𝑘). Since 𝜙𝑣 is an isomorphism between the matched cards, 𝐵𝐺,𝑣 ( 𝑘) = 𝐵 𝐻, 𝑓 ( 𝑣) ( 𝑘). By (5), the final indicator in (8) is also the same for 𝐺 and 𝐻 . Finally, 𝐶 𝐾,𝑣 (0) = 0, because a neighbor always has positive degree. Induction on 𝑘 in (8) gives

Thus

𝐶𝐺,𝑣 ( 𝑘) = 𝐶 𝐻, 𝑓 ( 𝑣) ( 𝑘)

and together with (5) this proves

( 𝑘 ≥ 0) .

𝑃𝐺 ( 𝑣) = 𝑃 𝐻 ( 𝑓 ( 𝑣)) , 𝜏𝐺 ( 𝑣) = 𝜏 𝐻 ( 𝑓 ( 𝑣))

(9) 49

Advancing Mathematics Research with AI-Driven Formal Proof Search

for every 𝑣 ∈ Ω. We next prove equality of type profiles: 𝑇𝐺 ( 𝑢) = 𝑇𝐻 ( 𝑓 ( 𝑢))

(10)

{{𝜏𝐺 ( 𝑥 ) : 𝑥 ∈ 𝑆 }} = {{𝜏 𝐻 ( 𝑥 ) : 𝑥 ∈ 𝑆 }} .

(11)

for every 𝑢. Fix 𝑢. If 𝑢 ∈ 𝐿, take 𝑆 = 𝑅, otherwise take 𝑆 = 𝐿 (thus 𝑆 is the opposite side from 𝑢). By (7) and (9), the multisets of global types on 𝑆 agree: The card isomorphism 𝜙𝑢 also preserves 𝑆, and therefore the multisets of local types on 𝑆 agree: {{𝜏𝐺\inc 𝑢 ( 𝑥 ) : 𝑥 ∈ 𝑆 }} = {{𝜏 𝐻 \inc 𝑓 (𝑢) ( 𝑥 ) : 𝑥 ∈ 𝑆 }} . (12) For 𝑥 ∈ 𝑆, bipartiteness gives the local-type formula ( 𝐹deg𝐺 (𝑢) ( 𝜏𝐺 ( 𝑥 )) , if 𝑥 ∈ 𝑁𝐺 ( 𝑢) , 𝜏𝐺 \inc 𝑢 ( 𝑥 ) = 𝜏𝐺 ( 𝑥 ) , if 𝑥 ∉ 𝑁𝐺 ( 𝑢) .

(13)

Indeed, if 𝑥 is adjacent to 𝑢, then deleting the incidence set of 𝑢 removes the edge 𝑢𝑥 , lowering deg𝐺 ( 𝑥 ) by one and deleting one occurrence of deg𝐺 ( 𝑢) from the degree profile of 𝑥 . If 𝑥 is not adjacent to 𝑢, then any neighbor of 𝑥 lies on the same side of the bipartition as 𝑢, and therefore cannot be adjacent to 𝑢; hence the type of 𝑥 is unchanged. The same formula holds for 𝐻 and 𝑓 ( 𝑢). Taking the number of occurrences of an arbitrary type 𝑡 in (13) gives

#𝑡 {{𝜏𝐺\inc 𝑢 ( 𝑥 ) : 𝑥 ∈ 𝑆 }} + #𝑡 𝑇𝐺 ( 𝑢) = #𝑡 {{𝜏𝐺 ( 𝑥 ) : 𝑥 ∈ 𝑆 }} + #𝑡 {{ 𝐹deg𝐺 (𝑢) ( 𝑠) : 𝑠 ∈ 𝑇𝐺 ( 𝑢)}} . (14)

There is an identical identity for 𝐻 . The first terms on the two sides of (14) agree by (12), and the global-type terms agree by (11). Also deg𝐺 ( 𝑢) = deg 𝐻 ( 𝑓 (𝑢)) by (5). Hence equality of the type-profile counts can be proved by descending induction on the first coordinate of 𝑡 . The base case is that no type in a type profile can have first coordinate at least 𝑛, since every vertex degree is < 𝑛. For the induction step, the only types 𝑠 with 𝐹deg𝐺 (𝑢) ( 𝑠) = 𝑡 have first coordinate 𝑡1 + 1; moreover every 𝑠 occurring in a type profile has positive first coordinate. Thus the rightmost term in (14) is already equal for 𝐺 and 𝐻 by the induction hypothesis, and subtracting the two versions of (14) yields equality of the number of occurrences of 𝑡 in 𝑇𝐺 ( 𝑢) and in 𝑇𝐻 ( 𝑓 ( 𝑢)). This proves (10). The distinctness of types transfers from 𝐺 to 𝐻 : if 𝜏 𝐻 ( 𝑥 ) = 𝜏 𝐻 ( 𝑦 ), then by applying (9) to

𝑓 −1 ( 𝑥 ) and 𝑓 −1 ( 𝑦 ) we obtain equality of the corresponding 𝐺 -types, so 𝑥 = 𝑦 .

Since types are pairwise distinct, adjacency is determined by type profiles: for every graph 𝐾 among 𝐺, 𝐻 and every pair of vertices 𝑎, 𝑏, 𝐾 has edge 𝑎𝑏

⇐⇒

𝜏 𝐾 ( 𝑏) ∈ 𝑇𝐾 ( 𝑎) .

(15)

The forward implication is the definition of 𝑇𝐾 ( 𝑎). Conversely, if 𝜏 𝐾 ( 𝑏) occurs in 𝑇𝐾 ( 𝑎), then some neighbor 𝑐 of 𝑎 has 𝜏 𝐾 ( 𝑐) = 𝜏 𝐾 ( 𝑏), and distinctness of types gives 𝑐 = 𝑏. Finally, for any 𝑢, 𝑣 ∈ Ω, equations (9), (10), and (15) give

𝐺 has edge 𝑢𝑣 ⇐⇒ 𝜏𝐺 ( 𝑣) ∈ 𝑇𝐺 ( 𝑢) ⇐⇒ 𝜏 𝐻 ( 𝑓 ( 𝑣)) ∈ 𝑇𝐻 ( 𝑓 ( 𝑢)) ⇐⇒ 𝐻 has edge 𝑓 ( 𝑢) 𝑓 ( 𝑣) . 50

Advancing Mathematics Research with AI-Driven Formal Proof Search

Thus 𝑓 is a graph isomorphism 𝐺  𝐻 . By (7), it preserves the two bipartition parts, so it is a bipartite isomorphism. □ The Lean proof discovered for this problem is at https://github.com/google-dee pmind/alphaproof-nexus-results/blob/main/APNOutputs/AICollaborator/G raphs/bipartite_graph_reconstruction_conjecture_2.lean. Log-Concavity of Hilbert Sequences Pure 𝑂-sequences, introduced in the context of Stanley’s work on Hilbert functions of monomial level algebras in the late 1970s, have been studied intensively over the last fifteen years [57]. They exhibit surprisingly strong positivity phenomena, especially in small codimension and type. Although pure 𝑂-sequences are not log-concave in general, the case of codimension 3 and type 2 remained open for over a decade [9, 68]. The following theorem establishes log-concavity in precisely this remaining case. Theorem. Every pure 𝑂-sequence of codimension 3 and type 2 is log-concave. Terminology. A monomial 𝑥0𝑚 (0) 𝑥1𝑚 (1) 𝑥2𝑚 (2) in three variables is identified with its exponent vector 𝑚 = ( 𝑚 (0) , 𝑚 (1) , 𝑚 (2)) ∈ ℕ3 . We write 𝑚′ ≤ 𝑚 for coordinate-wise inequality and | 𝑚 | = 𝑚 (0) + 𝑚 (1) + 𝑚 (2) for total degree. A finite order ideal Γ ⊂ ℕ3 is a finite set closed downward under this order: if 𝑛 ∈ Γ and 𝑚 ≤ 𝑛, then 𝑚 ∈ Γ. A monomial 𝑚 ∈ Γ is maximal if every 𝑛 ∈ Γ with 𝑚 ≤ 𝑛 also satisfies 𝑛 ≤ 𝑚. The ideal is pure if all maximal monomials have the same total degree; this common degree is the socle degree. The type is the number of maximal monomials. The pure 𝑂-sequence of Γ is ℎΓ ( 𝑑 ) = #{ 𝑚 ∈ Γ : | 𝑚 | = 𝑑 } .

For a monomial 𝑔, we simply write ℎ𝑔 ( 𝑑 ) = #{𝑢 ≤ 𝑔 : | 𝑢 | = 𝑑 }. The 𝑂-sequence is log-concave if ℎΓ ( 𝑖 − 1) ℎΓ ( 𝑖 + 1) ≤ ℎΓ ( 𝑖) 2 (0 < 𝑖 < 𝑒) ,

where 𝑒 is the socle degree of Γ. We write 1𝑃 for the indicator of the condition 𝑃 .

Proof. Let Γ be a pure order ideal in three variables and suppose that its two maximal monomials are 𝑚1 ≠ 𝑚2 . Since Γ is pure, | 𝑚1 | = | 𝑚2 | = 𝑒. Every element of a finite order ideal lies below a maximal element, so Γ = { 𝑢 : 𝑢 ≤ 𝑚1 } ∪ { 𝑢 : 𝑢 ≤ 𝑚2 } ,

After possibly interchanging 𝑚1 and 𝑚2 , there is a coordinate 𝑥 ∈ {0, 1, 2} such that 𝑚2 ( 𝑥 ) > 𝑚1 ( 𝑥 ) ,

𝑚2 ( 𝑦 ) ≤ 𝑚1 ( 𝑦 )

( 𝑦 ≠ 𝑥).

(1)

Indeed, the three integers 𝑚1 ( 𝑖) − 𝑚2 ( 𝑖) sum to zero and are not all zero, hence one sign occurs in a minority position; if necessary we swap the two monomials so that the minority sign is negative. Let 𝑐 = 𝑚1 ( 𝑥 ) + 1, and define ( 𝑀red ( 𝑦 ) =

𝑚2 ( 𝑥 ) − 𝑚1 ( 𝑥 ) − 1, 𝑚2 ( 𝑦 ) ,

𝑦 = 𝑥, 𝑦 ≠ 𝑥. 51

Advancing Mathematics Research with AI-Driven Formal Proof Search

Then | 𝑀red | = 𝑒 − 𝑐. For 𝑢 ≤ 𝑚2 , condition (1) implies 𝑢 ̸≤ 𝑚1

⇐⇒

𝑢 ( 𝑥 ) ≥ 𝑐.

If 𝑑 ≥ 𝑐, the map 𝑢 ↦→ 𝑢 − 𝑐𝑒𝑥 bijects {𝑢 ≤ 𝑚2 : | 𝑢 | = 𝑑, 𝑢 ( 𝑥 ) ≥ 𝑐 } with { 𝑣 ≤ 𝑀red : | 𝑣 | = 𝑑 − 𝑐 }. If 𝑑 < 𝑐, the first set is empty. Hence the 𝑂 sequence of Γ can be written as 𝐻 ( 𝑑 ) := ℎΓ ( 𝑑 ) = ℎ𝑚1 ( 𝑑 ) + 1𝑑 ≥𝑐 ℎ 𝑀red ( 𝑑 − 𝑐) .

(2)

We need to prove that 𝐻 ( 𝑑 − 1) 𝐻 ( 𝑑 + 1) ≤ 𝐻 ( 𝑑 ) 2 holds for 0 < 𝑑 < 𝑒. as

For an integer-valued sequence 𝐹 : ℕ → ℤ, define the first and scond difference sequences Δ𝐹 (0) = 𝐹 (0) ,

Δ2 𝐹 (0) = Δ𝐹 (0) ,

Δ𝐹 ( 𝑑 ) = 𝐹 ( 𝑑 ) − 𝐹 ( 𝑑 − 1)

( 𝑑 > 0) ,

Δ2 𝐹 ( 𝑑 ) = Δ𝐹 ( 𝑑 ) − Δ𝐹 ( 𝑑 − 1)

( 𝑑 > 0) .

We first prove an elementary divisor-count formula for a single monomial. Let 𝑚 = ( 𝛼, 𝛽, 𝛾 ) be a monomial. For 𝑝, 𝑞 ∈ ℕ, set 𝐿 𝑝,𝑞 ( 𝑘) = #{𝑟 ∈ ℕ : 𝑟 < 𝑝, 𝑟 ≤ 𝑘, 𝑘 − 𝑟 < 𝑞} .

Thus 𝐿 𝑝,𝑞 ( 𝑘) counts the number of pairs ( 𝑟, 𝑠) with 0 ≤ 𝑟 < 𝑝, 0 ≤ 𝑠 < 𝑞, and 𝑟 + 𝑠 = 𝑘. A direct box count gives 𝑡 ∑︁ ℎ𝑚 ( 𝑡 ) = 1𝑡−𝑘<𝛾+1 𝐿𝛼+1,𝛽 +1 ( 𝑘) . 𝑘=0

With the convention Δ𝐹 (0) = 𝐹 (0), the first-difference identities are and hence

Δ𝐿 𝑝,𝑞 ( 𝑡 ) = 1𝑡< 𝑝 + 1𝑡<𝑞 − 1𝑡< 𝑝+𝑞

( 𝑡 ≥ 0) ,

Δℎ𝑚 ( 𝑡 ) = 𝐿𝛼+1,𝛽 +1 ( 𝑡 ) − 1𝑡≥𝛾+1 𝐿𝛼+1,𝛽 +1 ( 𝑡 − 𝛾 − 1)

Taking one more difference gives, for every 𝑡 > 0,

( 𝑡 ≥ 0) .

Δ2 ℎ𝑚 ( 𝑡 ) = 1𝑡≤𝛼 + 1𝑡≤ 𝛽 + 1𝑡≤𝛾 − 1𝑡≤𝛼+ 𝛽 +1 − 1𝑡≤ 𝛽 +𝛾+1

− 1𝑡≤𝛾+𝛼+1 + 1𝑡≤𝛼+ 𝛽 +𝛾+2 .

(3)

In particular, Δ2 ℎ𝑚 ( 𝑡 ) ≤ 1. The same bound holds for the shifted sequence 𝑡 ↦−→ 1𝑡≥𝑐 ℎ𝑀red ( 𝑡 −𝑐) , because below the shift its second difference is zero, and from the shift onward it is the second difference of the principal sequence of 𝑀red . Therefore Δ2 𝐻 ( 𝑡 ) ≤ 2.

Formula (3) also implies the following useful dichotomy. If 𝑡 > 0 and Δ2 ℎ𝑚 ( 𝑡 ) = 1, then either 𝑡 ≤ 𝑚 (0) , 𝑡 ≤ 𝑚 (1) , 𝑡 ≤ 𝑚 (2) , (L) or

𝑡 ≥ 𝑚 (0) + 𝑚 (1) + 2,

𝑡 ≥ 𝑚 (1) + 𝑚 (2) + 2,

𝑡 ≥ 𝑚 (0) + 𝑚 (2) + 2,

𝑡 ≤ | 𝑚 | + 2. (U)

We refer to these as the lower and upper alternatives. For 𝑡 = 0, the lower alternative is automatic. We shall also use the following elementary consequences of the same box count. 52

Advancing Mathematics Research with AI-Driven Formal Proof Search

1. If 𝑡 ≤ 𝑚 ( 𝑖) for all 𝑖, then

2ℎ𝑚 ( 𝑡 ) = ( 𝑡 + 1)( 𝑡 + 2) ,

Δℎ𝑚 ( 𝑡 ) = 𝑡 + 1.

2. If 𝑡 ≥ 𝑚 ( 𝑖) + 𝑚 ( 𝑗) for every pair { 𝑖, 𝑗 }, and 𝑡 ≤ | 𝑚 | + 2, then,

2ℎ𝑚 ( 𝑡 ) = (| 𝑚 | + 1 − 𝑡 )(| 𝑚 | + 2 − 𝑡 ) .

(6)

Δℎ𝑚 ( 𝑡 ) = −(| 𝑚 | + 2 − 𝑡 ) .

(7)

2ℎ𝑚 ( 𝑡 ) ≤ (| 𝑚 | − 𝑡 + 1)(| 𝑚 | − 𝑡 + 2) .

(8)

Δℎ𝑚 ( 𝑡 ) ≤ 0.

(9)

3. If 𝑡 ≥ 𝑚 ( 𝑖) + 𝑚 ( 𝑗) + 1 for every pair { 𝑖, 𝑗 }, and 𝑡 ≤ | 𝑚 | + 2, then 4. For all 𝑡 , 5. If 2𝑡 ≥ | 𝑚 | + 1, then

(5)

Now fix 0 < 𝑑 < 𝑒 = | 𝑚1 | = | 𝑚2 |. Using 𝐻 ( 𝑑 ) = 𝐻 ( 𝑑 − 1) + Δ𝐻 ( 𝑑 ) and Δ𝐻 ( 𝑑 + 1) = Δ𝐻 ( 𝑑 ) + Δ2 𝐻 ( 𝑑 + 1) gives 𝐻 ( 𝑑 ) 2 − 𝐻 ( 𝑑 − 1) 𝐻 ( 𝑑 + 1) = ( Δ𝐻 ( 𝑑 )) 2 − 𝐻 ( 𝑑 − 1) Δ2 𝐻 ( 𝑑 + 1) .

(10)

Since 𝐻 ( 𝑑 − 1) ≥ 0 and Δ2 𝐻 ( 𝑑 + 1) ≤ 2, it is enough to prove the following two statements: and

Δ2 𝐻 ( 𝑑 + 1) = 1

=⇒

𝐻 ( 𝑑 − 1) ≤ ( Δ𝐻 ( 𝑑 )) 2 ,

(11)

Δ2 𝐻 ( 𝑑 + 1) = 2

=⇒

2 𝐻 ( 𝑑 − 1) ≤ ( Δ𝐻 ( 𝑑 )) 2 .

(12)

Indeed, if Δ2 𝐻 ( 𝑑 + 1) ≤ 0, equation (10) is immediate; if it is 1 or 2, then (11) or (12) applies. Write 𝑓 ( 𝑡 ) = ℎ𝑚1 ( 𝑡 ) and 𝑔 ( 𝑡 ) = 1𝑡≥𝑐 ℎ𝑀red ( 𝑡 − 𝑐), so that 𝐻 = 𝑓 + 𝑔 . Since Δ2 𝑓 ≤ 1 and Δ2 𝑔 ≤ 1, if Δ2 𝐻 ( 𝑑 + 1) = 1, then either or If Δ2 𝐻 ( 𝑑 + 1) = 2, then

Δ2 𝑓 ( 𝑑 + 1) = 1,

Δ2 𝑔 ( 𝑑 + 1) = 0,

(A)

Δ2 𝑓 ( 𝑑 + 1) = 0,

Δ2 𝑔 ( 𝑑 + 1) = 1.

(B)

Δ2 𝑓 ( 𝑑 + 1) = Δ2 𝑔 ( 𝑑 + 1) = 1.

(C)

Case A1: (A)+(L) for 𝑓 . Suppose equation (A) holds and the lower alternative (L) holds for 𝑓 with 𝑡 = 𝑑 + 1. Then in particular 𝑑 + 1 ≤ 𝑚1 ( 𝑥 ) < 𝑐, thus 𝑔 ( 𝑑 − 1) = 𝑔 ( 𝑑 ) = 0, hence Δ𝑔 ( 𝑑 ) = 0 and therefore 𝐻 ( 𝑑 − 1) = 𝑓 ( 𝑑 − 1) ,

Δ𝐻 ( 𝑑 ) = Δ 𝑓 ( 𝑑 ) .

By (5), 2 𝑓 ( 𝑑 − 1) = 𝑑 ( 𝑑 + 1) and Δ 𝑓 ( 𝑑 ) = 𝑑 + 1. Therefore

𝐻 ( 𝑑 − 1) = 𝑓 ( 𝑑 − 1) ≤ ( 𝑑 + 1) 2 = ( Δ 𝑓 ( 𝑑 )) 2 = ( Δ𝐻 ( 𝑑 )) 2 . 53

Advancing Mathematics Research with AI-Driven Formal Proof Search

This proves (11) in this case. Case A2: (A)+(U) for 𝑓 . Assume equation (A) holds and the upper alternative (U) holds for 𝑓 with 𝑡 = 𝑑 + 1. Let us introduce the shorthand notation 𝜌 = 𝑒 − 𝑑 . Then (U) gives 𝜌 ≥ −1. Applying (6) and (7) gives 2 𝑓 ( 𝑑 − 1) = ( 𝜌 + 2)( 𝜌 + 3) ,

Δ 𝑓 ( 𝑑 ) = −( 𝜌 + 2) .

(13)

The shifted summand satisfies Δ𝑔 ( 𝑑 ) ≤ 0,

2𝑔 ( 𝑑 − 1) ≤ ( 𝜌 + 2)( 𝜌 + 3) ,

2𝑔 ( 𝑑 ) ≤ ( 𝜌 + 1)( 𝜌 + 2) .

(14)

Indeed, the two inequalities for 𝑔 ( 𝑑 − 1) and 𝑔 ( 𝑑 ) follow from the universal upper bound (8), applied to the shifted sequence. For the sign of Δ𝑔 ( 𝑑 ), if 𝑑 < 𝑐, then Δ𝑔 ( 𝑑 ) = 0. If 𝑑 ≥ 𝑐, then the upper alternative for 𝑓 implies 𝑑 ≥ 𝑚1 ( 𝑥 ) + 𝑚1 ( 𝑦 ) + 1,

𝑑 ≥ 𝑚1 ( 𝑥 ) + 𝑚1 ( 𝑧 ) + 1,

where { 𝑥, 𝑦, 𝑧 } = {0, 1, 2}. Adding these inequalities gives 2𝑑 ≥ 2𝑚1 ( 𝑥 ) + 𝑚1 ( 𝑦 ) + 𝑚1 ( 𝑧 ) + 2 = 𝑒 + 𝑚1 ( 𝑥 ) + 2 . Since 𝑐 = 𝑚1 ( 𝑥 ) + 1 and | 𝑀red | = 𝑒 − 𝑐, this is equivalent to 2( 𝑑 − 𝑐) ≥ | 𝑀red | + 1. Thus the midpoint monotonicity (9) applies to the shifted 𝑀red -sequence and gives Δ𝑔 ( 𝑑 ) ≤ 0. To prove (11), by (13) it remains to show

2

𝑓 ( 𝑑 − 1) + 𝑔 ( 𝑑 − 1) ≤ −( 𝜌 + 2) + Δ𝑔 ( 𝑑 ) .

By (13) and (14), this follows from
2 ( 𝜌 + 2)( 𝜌 + 3) + 2𝑔 ( 𝑑 − 1) ≤ 2 −( 𝜌 + 2) + Δ𝑔 ( 𝑑 ) .

(15)

Since 𝑔 ( 𝑑 ) = 𝑔 ( 𝑑 − 1) + Δ𝑔 ( 𝑑 ), the third inequality in (14) gives 2𝑔 ( 𝑑 − 1) ≤ ( 𝜌 + 1)( 𝜌 + 2) − 2Δ𝑔 ( 𝑑 ) . Therefore the difference between the right-hand side and the left-hand side of (15) is at least
2
2 −( 𝜌 + 2) + Δ𝑔 ( 𝑑 ) − ( 𝜌 + 2)( 𝜌 + 3) − ( 𝜌 + 1)( 𝜌 + 2) − 2Δ𝑔 ( 𝑑 )
= 2Δ𝑔 ( 𝑑 ) Δ𝑔 ( 𝑑 ) − 2( 𝜌 + 2) + 1 . This is nonnegative because Δ𝑔 ( 𝑑 ) ≤ 0, 𝜌 ≥ −1, and hence Δ𝑔 ( 𝑑 ) − 2( 𝜌 + 2) + 1 ≤ 0.

Thus (11) holds in this case, and we completed the (A) case. For the two cases when (B) holds, that is Δ2 𝑔 ( 𝑑 + 1) = 1, we use the following shift reduction. If Δ2 𝐻 ( 𝑑 + 1) = 1 and 𝐻 ( 𝑑 + 1) ≤ ( Δ𝐻 ( 𝑑 + 1)) 2 , 54

Advancing Mathematics Research with AI-Driven Formal Proof Search

then

𝐻 ( 𝑑 − 1) ≤ ( Δ𝐻 ( 𝑑 )) 2 .

(16)

Indeed, Δ𝐻 ( 𝑑 ) = Δ𝐻 ( 𝑑 + 1) − 1 and 𝐻 ( 𝑑 − 1) = 𝐻 ( 𝑑 + 1) − Δ𝐻 ( 𝑑 + 1) − Δ𝐻 ( 𝑑 ). Therefore 𝐻 ( 𝑑 − 1) = 𝐻 ( 𝑑 + 1) − 2Δ𝐻 ( 𝑑 + 1) + 1 ≤ ( Δ𝐻 ( 𝑑 + 1)) 2 − 2Δ𝐻 ( 𝑑 + 1) + 1 = ( Δ𝐻 ( 𝑑 )) 2 .

Case B1: (B)+(L) for 𝑔. Assume equation (B) holds and the lower alternative (L) holds for 𝑔 with 𝑡 = 𝑑 + 1. Let 𝐷 = 𝑑 + 1. Since Δ2 𝑔 ( 𝐷) = 1, necessarily 𝐷 ≥ 𝑐, and Δ2 ℎ 𝑀red ( 𝐷 − 𝑐) = 1. In the lower subcase 𝐷 − 𝑐 ≤ 𝑀red ( 𝑖) for every 𝑖. Then 𝐷 − 𝑐 + 1 ≥ 1, and the lower formula (5) gives 2𝑔 ( 𝐷) = ( 𝐷 − 𝑐 + 1)( 𝐷 − 𝑐 + 2) , Δ𝑔 ( 𝐷) = 𝐷 − 𝑐 + 1. (17) We next prove two bounds for 𝑓 at 𝐷:

𝑓 ( 𝐷) ≤ ( 𝐷 + 1) Δ 𝑓 ( 𝐷) ,

Δ 𝑓 ( 𝐷) = 𝑐.

(18)

First, since Δ2 𝑓 ( 𝐷) = 0, the explicit formula (3), together with the lower inequalities for 𝑀red , implies 𝐷 ≤ 𝑚1 (0) + 𝑚1 (1) + 1,

𝐷 ≤ 𝑚1 (1) + 𝑚1 (2) + 1,

𝐷 ≤ 𝑚1 (0) + 𝑚1 (2) + 1.

(19)

Indeed, the two pair inequalities involving 𝑥 follow directly from 𝐷 − 𝑐 ≤ 𝑀red ( 𝑦 ) ≤ 𝑚1 ( 𝑦 ) for 𝑦 ≠ 𝑥 . The remaining pair inequality follows from (3): if it failed, then the corresponding two single indicators would be zero; since 𝐷 ≥ 𝑐 = 𝑚1 ( 𝑥 ) + 1, the 𝑥 -single indicator is also zero, and the right-hand side of (3) would be negative, contradicting Δ2 𝑓 ( 𝐷) = 0.

Thus, in (3) for 𝑓 at 𝐷, all three pair indicators and the triple indicator are equal to 1. Since Δ2 𝑓 ( 𝐷) = 0, exactly two of the three single indicators are equal to 1. Moreover the 𝑥 -single indicator is zero, because 𝐷 ≥ 𝑚1 ( 𝑥 ) + 1. Hence the two remaining single indicators are equal to 1. It follows that for every 1 ≤ 𝑘 ≤ 𝐷, the same two single indicators are still equal to 1, while the three pair indicators and the triple indicator are also equal to 1. Therefore Δ 2 𝑓 ( 𝑘) ≥ 2 − 3 + 1 = 0

(1 ≤ 𝑘 ≤ 𝐷) .

Thus the first differences Δ 𝑓 ( 𝑘) are nondecreasing on {0, 1, . . . , 𝐷 }. Since 𝑓 ( 𝐷) =

we get

𝐷 ∑︁ 𝑗=0

Δ 𝑓 ( 𝑗) ,

𝑓 ( 𝐷) ≤ ( 𝐷 + 1) Δ 𝑓 ( 𝐷) .

This proves the first inequality in (18).

For the second inequality in (18), relabel the two coordinates different from 𝑥 as 𝑦, 𝑧, and write 𝐴 = 𝑚1 ( 𝑦 ) + 1, 𝐵 = 𝑚1 ( 𝑧 ) + 1, 55

Advancing Mathematics Research with AI-Driven Formal Proof Search

and recall 𝑐 = 𝑚1 ( 𝑥 ) + 1. Using the box-count formula with 𝑥 as the third coordinate, the first-difference formula gives Δ 𝑓 ( 𝐷) = 𝐿 𝐴,𝐵 ( 𝐷) − 𝐿 𝐴,𝐵 ( 𝐷 − 𝑐) ,

because 𝐷 ≥ 𝑐. From the preceding paragraph, 𝐷 < 𝐴 and 𝐷 < 𝐵, hence 𝐿 𝐴,𝐵 ( 𝐷) = 𝐷 + 1,

Therefore

𝐿 𝐴,𝐵 ( 𝐷 − 𝑐) = 𝐷 − 𝑐 + 1.

Δ 𝑓 ( 𝐷) = ( 𝐷 + 1) − ( 𝐷 − 𝑐 + 1) = 𝑐,

proving (18). Using (17) and (18), we have

2 𝐻 ( 𝐷) = 2 𝑓 ( 𝐷) + 2𝑔 ( 𝐷) ≤ 2Δ 𝑓 ( 𝐷)( 𝐷 + 1) + ( 𝐷 − 𝑐 + 1)( 𝐷 − 𝑐 + 2) .

Also, by (17),

Δ𝐻 ( 𝐷) = Δ 𝑓 ( 𝐷) + Δ𝑔 ( 𝐷) = Δ 𝑓 ( 𝐷) + ( 𝐷 − 𝑐 + 1) .

Thus it is enough to show

2 2Δ 𝑓 ( 𝐷)( 𝐷 + 1) + ( 𝐷 − 𝑐 + 1)( 𝐷 − 𝑐 + 2) ≤ 2 Δ 𝑓 ( 𝐷) + 𝐷 − 𝑐 + 1 .

Since 𝐷 + 1 = ( 𝐷 − 𝑐 + 1) + 𝑐, the difference between the right-hand side and the left-hand side is
2Δ 𝑓 ( 𝐷) Δ 𝑓 ( 𝐷) − 𝑐 + 2Δ 𝑓 ( 𝐷)( 𝐷 − 𝑐 + 1) + ( 𝐷 − 𝑐 + 1)( 𝐷 − 𝑐) .

This is nonnegative because Δ 𝑓 ( 𝐷) ≥ 𝑐 and 𝐷 − 𝑐 + 1 ≥ 1. Therefore 𝐻 ( 𝐷) ≤ ( Δ𝐻 ( 𝐷)) 2 . By the shift reduction (16), this proves (11). Case B2: (B)+(U) for 𝑔. Again let 𝐷 = 𝑑 + 1 and put 𝜌 = 𝑒 − 𝐷. The upper alternative for ℎ 𝑀red at 𝐷 − 𝑐 gives 𝜌 ≥ −2. Since | 𝑀red | = 𝑒 − 𝑐, formulas (6) and (7) give 2𝑔 ( 𝐷) = ( 𝜌 + 1)( 𝜌 + 2) ,

Δ𝑔 ( 𝐷) = −( 𝜌 + 2) .

(20)

2 𝑓 ( 𝐷) ≤ ( 𝑒 − 𝐷 + 1)( 𝑒 − 𝐷 + 2) = ( 𝜌 + 1)( 𝜌 + 2) .

(21)

For the first summand, the universal upper bound (8) gives

It remains to justify the sign of Δ 𝑓 ( 𝐷). Since 𝑔 is in the upper alternative at 𝐷, we have

𝐷 − 𝑐 ≥ 𝑀red (0) + 𝑀red (1) + 2, 𝐷 − 𝑐 ≥ 𝑀red (1) + 𝑀red (2) + 2, 𝐷 − 𝑐 ≥ 𝑀red (0) + 𝑀red (2) + 2.

Adding these three inequalities gives

Hence

3( 𝐷 − 𝑐) ≥ 2| 𝑀red | + 6 = 2( 𝑒 − 𝑐) + 6.

2 |𝑀 | + 9 2| 𝑀red | + 6 = | 𝑀red | + 1 + red > | 𝑀red | + 1, 3 3 because | 𝑀red | ≥ 0. Therefore 2( 𝐷 − 𝑐) ≥

2 𝐷 = 2( 𝐷 − 𝑐) + 2𝑐 ≥ ( 𝑒 − 𝑐 + 1) + 2𝑐 = 𝑒 + 𝑐 + 1 ≥ 𝑒 + 1.

56

Advancing Mathematics Research with AI-Driven Formal Proof Search

By midpoint monotonicity (9), applied to 𝑓 = ℎ𝑚1 , we get Δ 𝑓 ( 𝐷) ≤ 0. Using (20), (21), we get 2 𝐻 ( 𝐷) ≤ 2( 𝜌 + 1)( 𝜌 + 2) , Δ𝐻 ( 𝐷) = Δ 𝑓 ( 𝐷) − ( 𝜌 + 2) . Since 𝜌 ≥ −2 and Δ 𝑓 ( 𝐷) ≤ 0, we have

2 ( 𝜌 + 1)( 𝜌 + 2) ≤ −Δ 𝑓 ( 𝐷) + 𝜌 + 2 .

giving the desired 𝐻 ( 𝐷) ≤ ( Δ𝐻 ( 𝐷)) 2 . By the shift reduction (16), this proves (11). Case C: (C) holds. So here Δ2 𝐻 ( 𝑑 + 1) = 2 and hence Δ2 𝑓 ( 𝑑 + 1) = Δ2 𝑔 ( 𝑑 + 1) = 1. Since Δ2 𝑔 ( 𝑑 + 1) = 1, necessarily 𝑑 + 1 ≥ 𝑐. Therefore the lower alternative (L) for 𝑓 is impossible, because it would imply 𝑑 + 1 ≤ 𝑚1 ( 𝑥 ) < 𝑐. Hence 𝑓 is in its upper alternative, that is, (U) holds for 𝑓 . The lower alternative (L) for 𝑔 is also impossible. Indeed, if 𝑑 + 1 − 𝑐 ≤ 𝑀red ( 𝑖) for every 𝑖, then, choosing any 𝑦 ≠ 𝑥 , we get 𝑑 + 1 ≤ 𝑚1 ( 𝑥 ) + 1 + 𝑀red ( 𝑦 ) = 𝑚1 ( 𝑥 ) + 1 + 𝑚2 ( 𝑦 ) ≤ 𝑚1 ( 𝑥 ) + 1 + 𝑚1 ( 𝑦 ) .

But the upper alternative for 𝑓 gives 𝑑 + 1 ≥ 𝑚1 ( 𝑥 ) + 𝑚1 ( 𝑦 ) + 2, a contradiction. Thus 𝑔 is also in its upper alternative, and (U) holds for 𝑔. Put 𝜌 = 𝑒 − 𝑑 again. Since | 𝑀red | = 𝑒 − 𝑐, we also have | 𝑀red | − ( 𝑑 − 𝑐) = 𝑒 − 𝑑 = 𝜌. The upper formulas (6) and (7), applied to 𝑓 and to the shifted summand 𝑔, give

and Therefore

2 𝑓 ( 𝑑 − 1) = ( 𝜌 + 2)( 𝜌 + 3) ,

Δ 𝑓 ( 𝑑 ) = −( 𝜌 + 2) ,

2𝑔 ( 𝑑 − 1) = ( 𝜌 + 2)( 𝜌 + 3) ,

Δ𝑔 ( 𝑑 ) = −( 𝜌 + 2) .

2 𝐻 ( 𝑑 − 1) = 2( 𝜌 + 2)( 𝜌 + 3) ,

Δ𝐻 ( 𝑑 ) = −2( 𝜌 + 2) .

Since the upper alternative for 𝑓 gives 𝜌 ≥ −1, we have

( Δ𝐻 ( 𝑑 )) 2 − 2 𝐻 ( 𝑑 − 1) = 4( 𝜌 + 2) 2 − 2( 𝜌 + 2)( 𝜌 + 3) = 2( 𝜌 + 2)( 𝜌 + 1) ≥ 0.

which proves (12). This completes the proof of (11) and (12), and hence by (10) 𝐻 ( 𝑑 − 1) 𝐻 ( 𝑑 + 1) ≤ 𝐻 ( 𝑑 ) 2 . Since 0 < 𝑑 < 𝑒 was arbitrary and 𝐻 is the pure 𝑂-sequence of Γ by (2), the theorem follows. □ The Lean proof for the problem can be found at https://github.com/google-dee pmind/alphaproof-nexus-results/tree/main/APNOutputs/AICollaborator/A lgebraicGeometry. A Convergence Proof of Modified Anchored Gradient Descent-Ascent A natural-language version of the convergence proof we discovered can be found in Surina et al. [58]. The Lean proof is at https://github.com/google-deepmind/alphaproof-n

exus-results/blob/main/APNOutputs/Optimization/LastIterateConvergence. lean.

57

Advancing Mathematics Research with AI-Driven Formal Proof Search

Written on the Wall, Conjecture 2 For a graph 𝐺 , let 𝑉 ( 𝐺 ) be the set of vertices and 𝐸 (𝐺 ) the set of edges. For 𝑣 ∈ 𝑉 ( 𝐺 ), write 𝑑 ( 𝑣) for the degree of 𝑣, and let 𝑁 ( 𝑣) be the set of vertices adjacent to 𝑣 in 𝐺 . Let 𝛼 ( 𝑣) be the local independence number of 𝑣: the size of the largest independent set in 𝐺 [ 𝑁 ( 𝑣)]. Let Í ℓ ( 𝐺 ) := 1𝑛 𝑣 𝛼 ( 𝑣) be the average of the local independence numbers, and let 𝐿𝑆 ( 𝐺 ) be the maximum number of leaves in a spanning tree of 𝐺 , or 0 if 𝐺 is not connected. Theorem. If 𝐺 is a simple connected graph on 𝑛 vertices, then 𝐿𝑆 ( 𝐺 ) ≥ 2( ℓ ( 𝐺 ) − 1) .

Proof. Let 𝑉 := 𝑉 (𝐺 ). For every vertex 𝑣 ∈ 𝑉 , fix a maximum independent set 𝐴 ( 𝑣) in 𝐺 [ 𝑁 ( 𝑣)]. Then 𝛼 ( 𝑣) = | 𝐴 ( 𝑣)|. Now take two copies of 𝑉 , and add edges 𝑢𝑣 from 𝑢 ∈ 𝑉 on the left to 𝑣 ∈ 𝐴 (𝑢) on the right. This forms a bipartite graph, where vertices on the left side have degree 𝛼 ( 𝑣). The key idea is to look at the degrees of the vertices on the right side, and formulate the entire proof in terms of them. Formally, put 𝑐 ( 𝑣) := |𝑢 ∈ 𝑉 ( 𝐺 ) : 𝑣 ∈ 𝐴 ( 𝑢)| as the degree of a vertex 𝑣 on the right side. Í Í Note that 𝑐 ( 𝑣) ≤ 𝑑 ( 𝑣), for all 𝑣 ∈ 𝑉 . Because 𝑣 𝛼 ( 𝑣) = 𝑣 𝑐 ( 𝑣), it is enough to show that Í ( 𝐿𝑆 ( 𝐺 )/2 + 1). To simplify the notation, we set 𝜇 := 𝐿𝑆 ( 𝐺 )/2 + 1, and so the goal 𝑣 𝑐 ( 𝑣) ≤ 𝑛Í is to show 𝑣 𝑐 ( 𝑣) ≤ 𝑛𝜇 . Lemma 1. For every edge 𝑢𝑣 ∈ 𝐸 ( 𝐺 ) we have 𝑐 ( 𝑢) + 𝑐 ( 𝑣) ≤ | 𝑁 ( 𝑢) ∪ 𝑁 ( 𝑣)|. Proof of Lemma 1. For every vertex 𝑤 ∈ 𝑁 (𝑢) ∪ 𝑁 ( 𝑣), at most one of 𝑢 and 𝑣 can be part of 𝐴 ( 𝑤), otherwise the edge 𝑢𝑣 would contradict the fact that 𝐴 ( 𝑤) is independent. On the other hand, if 𝑤 ∈ 𝑉 is such that 𝑢 or 𝑣 is in 𝐴 ( 𝑤), then 𝑤 must be part of 𝑁 (𝑢) ∪ 𝑁 ( 𝑣). Then 𝑐 ( 𝑢) + 𝑐 ( 𝑣) is at most the size of 𝑁 ( 𝑢) ∪ 𝑁 ( 𝑣). □ Lemma 2. For every edge 𝑢𝑣 ∈ 𝐸 ( 𝐺 ) we have | 𝑁 (𝑢) ∪ 𝑁 ( 𝑣)| ≤ 𝐿𝑆 ( 𝐺 ) + 2. Proof of Lemma 2. We construct a spanning tree in 𝐺 with at least | 𝑁 (𝑢) ∪ 𝑁 ( 𝑣)| − 2 leaves. Start with the edge 𝑢𝑣 and add all the vertices in 𝑁 (𝑢) ∪ 𝑁 ( 𝑣) \ {𝑢, 𝑣} as pendant vertices of degree 1. There are | 𝑁 (𝑢) ∪ 𝑁 ( 𝑣)| − 2 leaves in this tree 𝑇 ′. Because 𝐺 is connected, we can expand 𝑇 ′ to a spanning tree 𝑇 of 𝐺 by adding edges until no more can be added. Then from every leaf in 𝑇 ′ there is a path to a leaf in 𝑇 that doesn’t cross 𝑢𝑣. All these leaves must be distinct, since they are contained in distinct subtrees of 𝑇 . Then 𝑇 has at least | 𝑁 (𝑢) ∪ 𝑁 ( 𝑣)| −2 leaves. □ Lemmas 1 and 2 show that for every edge 𝑢𝑣 ∈ 𝐸 (𝐺 ), 𝑐 ( 𝑢) + 𝑐 ( 𝑣) ≤ 𝐿𝑆 ( 𝐺 ) + 2 = 2 𝜇.

Í Next, we observe that 𝑣 𝑐 ( 𝑣) ≤ 𝑛𝜇 trivially holds if every 𝑐 ( 𝑣) ≤ 𝜇 . So assume this is not the case. Then we can split the vertices into "heavy" vertices with 𝑐 ( 𝑣) > 𝜇 , and "light" vertices with 𝑐 ( 𝑣) ≤ 𝜇 . Let 𝑆 be the set of heavy vertices.

𝑆 must be an independent set, since the above equation shows that for any edge 𝑢𝑣, at most one of 𝑢 or 𝑣 can be heavy. Less obvious is that light vertices cannot have many neighbors in 𝑆. Lemma 3. If 𝑣 is a light vertex, then | 𝑁 ( 𝑣) ∩ 𝑆 | < 𝜇 . 58

Advancing Mathematics Research with AI-Driven Formal Proof Search

Proof of Lemma 3. Let 𝑢 ∈ 𝑁 ( 𝑣) ∩ 𝑆. Since 𝑆 is independent, all neighbours of 𝑢 are outside 𝑁 ( 𝑣) ∩ 𝑆. So | 𝑁 ( 𝑢) ∪ 𝑁 ( 𝑣)| ≥ | 𝑁 ( 𝑣) ∩ 𝑆 | + | 𝑁 ( 𝑢)|. Using Lemma 2 we get | 𝑁 ( 𝑣) ∩ 𝑆 | ≤ | 𝑁 ( 𝑢) ∪ 𝑁 ( 𝑣)| − | 𝑁 ( 𝑢)| ≤ 𝐿𝑆 ( 𝐺 ) + 2 − 𝑑 (𝑢) .

As 𝑑 ( 𝑢) ≥ 𝑐 (𝑢) > 𝜇 , we obtain | 𝑁 ( 𝑣) ∩ 𝑆 | < 𝐿𝑆 ( 𝐺 ) + 2 − 𝜇 = 𝜇 . □

Then the theorem follows from the following more general statement: Claim. Let 𝑐 : 𝑉 → ℝ and 𝜇 ≥ 0 satisfy: 1. 𝑐 ( 𝑣) ≤ 𝑑 ( 𝑣) for all 𝑣, 2. 𝑐 ( 𝑢) + 𝑐 ( 𝑣) ≤ 2 𝜇 for every edge 𝑢𝑣, 3. 𝑆 := {𝑢 : 𝑐 ( 𝑢) > 𝜇 } is an independent set, 4. | 𝑁 ( 𝑣) ∩ 𝑆 | < 𝜇 for every 𝑣 ∉ 𝑆. Í Then 𝑣 𝑐 ( 𝑣) ≤ 𝑛𝜇 . Proof of Claim. We assume 𝑆 is non-empty, otherwise the claim is trivially true. The proof uses a discharging argument: it sends the excess 𝑐 ( 𝑢) − 𝜇 from a heavy vertex 𝑢 ∈ 𝑆 to its Í neighbors. The redistribution keeps the total sum 𝑣 𝑐 ( 𝑣) constant. However, the amount sent to a light vertex 𝑣 is less than the slack 𝜇 − 𝑐 ( 𝑣), so the overall sum can’t exceed 𝑛𝜇 . Precisely, define a weight function that transfers excess from heavy to light vertices: ( 𝜇−𝑐 ( 𝑣) if 𝑢 ∈ 𝑆 and 𝑢𝑣 is an edge, 𝑊 ( 𝑢, 𝑣) := 𝑑 (𝑢) 0 otherwise. Because 𝑆 is independent, the weight flows only from heavy to light vertices. We now show two statements. Each heavy vertex sends out enough weight. If 𝑢 ∈ 𝑆 and 𝑢𝑣 is an edge, then 𝑐 ( 𝑢)+ 𝑐 ( 𝑣) ≤ 2 𝜇 by condition 2. So 𝜇 − 𝑐 ( 𝑣) ≥ 𝑐 (𝑢) − 𝜇 . Then ∑︁ 𝑐 ( 𝑢) − 𝜇 𝑊 ( 𝑢, 𝑣) ≥ 𝑑 ( 𝑢) = 𝑐 (𝑢) − 𝜇. 𝑑 ( 𝑢) 𝑣 ∈ 𝑁 ( 𝑢)

Each light vertex absorbs at most its slack. Let 𝑣 ∉ 𝑆. Then 𝑣 receives weight from vertices in 𝐹 := 𝑁 ( 𝑣) ∩ 𝑆. Let 𝑢 ∈ 𝐹 . From conditions (1) and (4), we have | 𝐹 | < 𝜇 < 𝑐 ( 𝑢) ≤ 𝑑 ( 𝑢). Then the total weight received is ∑︁ ∑︁ 𝜇 − 𝑐 ( 𝑣) ∑︁ 𝜇 − 𝑐 ( 𝑣) 𝑊 ( 𝑢, 𝑣) = < = 𝜇 − 𝑐 ( 𝑣) . 𝑑 ( 𝑢 ) | 𝐹 | 𝑢∈ 𝐹 𝑢∈ 𝐹 𝑢∈ 𝐹

These two statements together show that ∑︁ ∑︁ ∑︁ ∑︁ ∑︁ ∑︁ 𝑐 ( 𝑢) − 𝜇 ≤ 𝑊 ( 𝑢, 𝑣) = 𝑊 ( 𝑢, 𝑣) ≤ 𝜇 − 𝑐 ( 𝑣) . 𝑢 ∈𝑆

Re-arranging the terms gives

𝑢∈𝑆 𝑣∉𝑆

Í

𝑣∉𝑆 𝑢∈𝑆

𝑣 𝑐 ( 𝑣) < 𝑛𝜇 as desired.

𝑣∉𝑆

□

The discovered lean proof for this is available at https://github.com/google-dee

pmind/alphaproof-nexus-results/blob/main/APNOutputs/OEIS/GraphConjec ture2.lean. 59