Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel

Built by Colin Snyder · colin@colinsnyder.com

Advised by Mike Kim · proposed solutions ↓

Inspired by Ignis · previously built by Myself, Dhruv Agarwal, & Nitin Kesarwani at the New Turing Institute

Star Fleet is an AI system that solves the world's hardest open mathematics problems using Lean 4. It's a Mac desktop app that controls up to 20 custom agentic harnesses called “starships” in parallel, each running its own GPT-5.6 instance on a dedicated 60-vCPU server and working on a separate math problem. Everything is built from scratch in TypeScript & Bun.

Each starship has access to:

• x86-64 CPU bursts of up to 2,000 vCPUs for search programs that shard into thousands of independent single-core jobs
• H100 GPU bursts for massively parallel search programs
• The world's largest corpus, afaik, of Lean 4 premises (theorems & lemmas), searchable in plain English via gemini-embeddings-2 & chroma vector db
• A Firecrawl.dev index of arXiv.org research papers & GitHub repos
• Claude Fable API wrapped in a proof-verifier agentic harness to review submitted answers + an iMessage API to ask Colin (the human) for an additional review after Fable's approval
• Ton 618, a local long-term memory system where every verified Lean 4 premise (theorem or lemma) is woven into a dependency graph, so proofs compound
• A dedicated 60-vCPU, 120 GiB memory sandbox preinstalled with SAT/SMT solvers (CaDiCaL, kissat, Z3), Google's CP-SAT, computer algebra systems (SageMath, PARI/GP, GAP, Macaulay2), and the full Rust, CUDA C++, and Lean 4 toolchains

Solution Proposed (27) #

Many problems listed as “open” carry informal or partial answers already available online; we tried extremely hard to avoid working on any such problems.

• 1. Erdős Problem #123Erdős Problem www.erdosproblems.com/123## ›Question

Let be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form (), none of which divide any other?

(Erdős Problem #123 — prize: $250 — number theory — https://www.erdosproblems.com/123)

›Result #

For every pairwise-coprime triple of integers a,b,c>1, every sufficiently large integer is a sum of distinct terms a^i b^j c^k such that no selected term divides another. In Lean, this is the theorem Erdos123.erdos_123 : Erdos123.IntendedStatement.

def IntendedStatement : Prop :=
  ∀ a b c : ℕ, 1 < a → 1 < b → 1 < c → PairwiseCoprime3 a b c →
    IsDComplete (Smooth3 a b c)

/-- Erdős Problem 123 for the intended nondegenerate hypothesis `a,b,c>1`. -/
theorem erdos_123 : IntendedStatement := intended_erdos_123

›Report #

The problem and why it resisted the usual induction #

For pairwise-coprime integers , consider the numbers

The question asks whether every sufficiently large integer is a sum of distinct such numbers, with the additional requirement that

no chosen summand divides another.The divisibility condition is the real source of difficulty. Ordinary completeness arguments can use many terms from different scales, but terms from different scales tend to be comparable by divisibility. Conversely, a set chosen to be a divisibility antichain can be too arithmetically sparse to fill consecutive integers.

Earlier work had developed a powerful reduction scheme: choose a correction with the required residue modulo one base, subtract it, divide by that base, and induct. For particular triples this succeeds after a finite computer check. In general, however, it leaves a stubborn

finite-seed problem: one must first represent every integer in a multiplicatively wide interval . The correction induction does not construct that interval; it only propagates it.This explains why several attractive partial ideas did not finish the problem:

• A signed identity of difference one gives two consecutive sums, but one residue representative per class necessarily has spread at least the modulus minus one. A width-one interval cannot grow under ordinary residue gluing.
• Complete residue systems on a primitive level solve congruences, but say nothing about their numerical spread.
• Van der Waerden and Hales–Jewett arguments produce arbitrarily long arithmetic progressions of primitive sums, but initially with an uncontrolled common difference.
• Even after fixing the common difference, a progression carries a large positive baseline . Replicating such progressions increases width and baseline at the same rate, so it need not produce the multiplicatively wide seed required by induction.

The important lesson was that

large additive width is not enough. The lower endpoint has to remain under quantitative control.## The homogeneous-level coordinate system

The first structural simplification is to work on one homogeneous exponent level

For pairwise-coprime bases greater than one, divisibility of monomials is coordinatewise comparison of their exponents. Therefore two distinct monomials on the same level can never divide one another. Every subset of a homogeneous level is automatically primitive.

This turns the problem into an additive question about subset sums while making primitiveness essentially free—as long as all pieces of the construction can be placed on the same exact degree.

An edge-code construction supplies primitive subset sums on one level with distinct residues modulo and a bounded carry. Coloring by that carry and applying finite van der Waerden, itself obtained from Mathlib’s Hales–Jewett theorem, gives arbitrarily long exact arithmetic progressions of primitive homogeneous subset sums.

Turning one AP into a large lattice interval #

Order the bases as

Choose

and then choose so that

Define two coprime homogeneous translation weights

Copies of one AP digit family are translated by the weights

The choice places different copies in disjoint bands of the -exponent. Multiplying every term by makes every AP term strict-interior. All copies then lie on one exact exponent degree.

A bounded homogeneous-radix lemma proves that coefficient sums

contain a full interval of width at least . Replacing each coefficient by the corresponding AP digit set realizes this as an interval on a lattice of step , where is the AP difference.

Filling residues with face corrections #

The next ingredient constructs, on

every sufficiently high exact degree, a primitive correction for each residue modulo any prescribed modulus. The corrections are supported on the three coordinate faces and, in the ordered case, have total size bounded byApply this with modulus , on the same exact degree as the AP-radix construction. Face-supported corrections are disjoint from the strict-interior AP terms. Moreover,

so exponential domination gives

Thus the correction spread is eventually smaller than the radix width. Residue gluing converts the lattice interval into an ordinary consecutive interval satisfying

for a fixed constant .

At this stage there is a genuine interval, but its multiplicative width is still only bounded by a constant. This is exactly where the earlier baseline problem remained.

The key breakthrough: an optional interior shell #

The decisive idea was to exploit monomials that had not yet been used, on the

same exact homogeneous level.For each of linearly many indices , fix a -exponent just beyond every AP band. Among the remaining -exponents, choose the last point of the geometric grid

below a target of size . Because consecutive grid points differ by the fixed factor , the selected monomial lies in a controlled multiplicative window. After restoring the common factors, this produces at least distinct optional monomials satisfying

Every optional term is therefore no larger than the already available interval width. Adding such a term optionally—either use it or do not—extends a consecutive interval without changing its lower endpoint. Since all optional terms remain on the same exact level and lie beyond the AP exponent bands, primitiveness and disjointness are preserved.

Their combined contribution is

while the lower endpoint remains . Hence the ratio of the upper endpoint to the lower endpoint grows linearly with . For every requested , and beyond every requested lower threshold, this constructs a primitively represented interval

This interior-shell amplification is what removes the finite-seed obstruction. The successful coordinate change was not merely “work on a homogeneous level,” but “place the main growth along an interior homogeneous ray, then use the unused transverse strip as optional mass.”

Completing the induction #

The residue-reduction argument was strengthened to a flexible finite-seed gate: there are constants and such that

any represented interval with implies d-completeness.Applying the arbitrary-width construction with proves d-completeness for ordered bases . Pairwise-coprime bases greater than one are distinct, so every triple has one of six strict orderings. Explicit permutations of the exponents show that permuting the bases leaves the smooth set unchanged, completing all cases.

Verification #

The proof is formalized in Lean 4 with Mathlib. The final theorem is

Erdos123.erdos_123 : Erdos123.IntendedStatement

where

IntendedStatement

quantifies over all pairwise-coprime natural bases greater than one and asserts an explicit eventual threshold for primitive representations.The complete project builds successfully, and a source scan finds no proof placeholders. Lean’s axiom report for the final theorem is exactly

[propext, Classical.choice, Quot.sound]

with no

sorryAx

. The webpage literally writes ; that universal formulation is false at . The project records this separately and proves the intended nondegenerate conjecture used in the source literature and independent formal-conjecture encoding.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 2. Erdős Problem #129Erdős Problem www.erdosproblems.com/129## ›Question

Let be the smallest such that if the edges of are -coloured then there is a set of vertices which does not contain a copy of in at least one of the colours. Prove that there is a constant such that

(Erdős Problem #129 — graph theory, ramsey theory — https://www.erdosproblems.com/129)

›Result #

The proposed bound is false: for every natural n ≥ 120, 2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n), so no constant C > 1 can satisfy R(n;3,2) < C^(√n) for all n. Consequently the exact formal proposition LiteralProblem129 is false.

theorem not_literalProblem129 : ¬ LiteralProblem129 := by
  intro h
  exact not_claimedBoundFor_two (h 2 (by omega))

theorem R3_two_global_exponential_sandwich (n : ℕ) (hn : 120 ≤ n) :
    2 ^ (n / 120) < R3 n 2 ∧ R3 n 2 ≤ 2 ^ (2 * n) := by
  exact ⟨two_pow_div_120_lt_R3_two n hn,
    R3_two_le_two_pow_two_mul n⟩

›Report #

The problem and why it was deceptive #

Erdős Problem 129 defines a Ramsey-type threshold

R(n;3,r)

: the least orderN

such that everyr

-colouring of the edges ofK_N

has ann

-vertex set on which at least one colour contains no triangle. The proposed bound wasR(n;3,r) < C(r)^(√n)

.At first sight this looks like a difficult upper-bound problem in multicolour Ramsey theory. There was an additional historical obstacle: the modern Erdős Problems database already recorded Antonio Girão's observation that the displayed statement is false, but retained an OPEN label on the theory that the 1997 source must have intended some different, unstated definition.

That ambiguity mattered. Disproving a mistranscription would not solve the intended problem, while silently inventing a replacement would not answer the published question. The work therefore had to settle both the mathematics and the statement-fidelity issue.

What earlier reasoning missed #

The decisive probabilistic estimate comes from looking at

many edge-disjoint triangles inside every tested vertex set.A random red-blue colouring makes any fixed triangle monochromatic in a specified colour with probability

1/8

. If ann

-set contains quadratically many edge-disjoint triangles, those events use disjoint edge variables and are independent. Consequently, the probability that the set has no triangle in a specified colour is exponentially small inn²

, not merely inn

.This is enough to union-bound over all

n

-subsets of a graph whose order is exponential inn

. The printedexp(c√n)

lower estimate was therefore simply a weak true estimate; it was not logically inconsistent with the published definition and did not force the existence of a missing condition.There were also two formal dead ends:

• An initial counting proof used Lean's native_decide

. Although computationally correct, this introduced generated axioms and was unsuitable for a kernel-only certificate. It was replaced by kerneldecide

. - The first endpoint negated an operational least-order formulation, while the formal statement defined R

using a natural-number infimum. That gap required a finite Ramsey theorem and a proof that the infimum is attained.

The construction that works #

For each parameter

t≥1

, take an arbitrary set of60t

vertices and divide it into three equal parts. Latin-square triples of the form(i, j, i+j)

produce a quadratic family of pairwise edge-disjoint triangles. The formal construction supplies

6(60t²+2)

such triangles for every enumeration of the set.For one target colour, a colouring that avoids a monochromatic packed triangle has at most

7^L · 2^(|E|-3L)

possibilities, where

L

is the packing size. Union-bounding over both colours and all enumerated60t

-sets shows that some colouring ofK_(2^t)

makesevery60t

-set contain both a red triangle and a blue triangle. Thus the Ramsey property fails at ambient order2^t

.This already defeats every square-root-exponential upper bound. To identify the actual scale, an elementary canonical-sequence proof gives the complementary finite Ramsey estimate

R(n;3,2)≤2^(2n)

. Monotonicity in the tested set size then extends the packed lower bound from the subsequencen=60t

to everyn≥120

:2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n)

.So the literal threshold is exponential with exponent linear in

n

, whereas the conjectured upper bound has exponent only√n

.## Resolving the source ambiguity

The publisher scan of Erdős's 1997 paper was checked directly. It defines

f_k^(r)(n)

as the largest order admitting anr

-colouring in which everyn

-set contains aK_k

in every colour. Lean proves that, fork=3

and two colours, this admissibility condition is exactly the negation of the website's Ramsey predicate.The investigation then followed the historical alternatives rather than assuming the scan was conclusive:

• Erdős and Gyárfás's Split and balanced colorings of complete graphsdefines different minimum-order split and balanced parameters, with polynomial rather than square-root-exponential behaviour. - Their A variant of the classical Ramsey problemstudies(p,q)

-colourings and a different extremal function. - Gyárfás's 2013 retrospective discusses both projects but gives no corrected version of Problem 129.

• A searchable corpus of all 218 PDFs linked from Gyárfás's publication page revealed no later correction or alternative formulation.

The source's weak probabilistic lower bound therefore does not identify another problem, and no primary source supplies one. The formally verified disproof answers the only definite published statement. Girão retains priority for the elementary probabilistic objection; the contribution here is the complete formal certificate, exact threshold diagnosis, and source audit.

Verification #

The proof is a standalone Lean 4 + Mathlib project. It includes:

• the faithful definitions of edge colourings, monochromatic triangles, RamseyAt

, and the exact infimumR3

; - the Latin-square triangle packing and exact colouring count;

• the union-bound construction;
• ambient and test-size monotonicity;
• finite Ramsey existence and infimum attainment;
• the exact negation of the proposed theorem and the global exponential sandwich.

The verifier builds all 8572 targets, directly checks the final theorem file, and rejects

native_decide

,sorry

,admit

, or any declared axiom. The final theorems depend only on Mathlib's standard logical principlespropext

,Classical.choice

, andQuot.sound

.

cd verified_math/F-015_global-exponential-threshold/lean && bash verify.sh

The run ends with:

Build completed successfully (8572 jobs).
PASS: global exponential sandwich kernel-checked; no forbidden proof escape

›Download Full Solution & Verify with Your AI #

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• An initial counting proof used Lean's
• 3. Erdős Problem #130Erdős Problem www.erdosproblems.com/130## ›Question

Let be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in , where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite?

(Erdős Problem #130 — graph theory, chromatic number — https://www.erdosproblems.com/130)

›Result #

There exists an infinite set A in R^2 containing no three collinear points and no four concyclic points such that, for every natural number k, the graph joining pairs at positive integer distance has no proper k-coloring. Thus the chromatic number in Erdos Problem #130 can be infinite.

theorem Erdos130.erdos130_infinite_chromatic :
    Exists fun A : Set Point =>
      And A.Infinite
        (And (GeneralPosition A)
          (forall k : Nat, Not (HasKColoring A k))) := by
  exact InfiniteAssembly.erdos130_infinite_chromatic_solution

›Report #

The problem and the obstruction #

Erdős Problem #130 asks whether an infinite set of points in the real plane can simultaneously satisfy two demands that pull in opposite directions:

strong general position: no three points are collinear and no four are concyclic;arithmetic density: the graph joining pairs at positive integer distance has infinite chromatic number.

The difficulty is not merely finding many integer distances. Classical constructions can realize complicated finite graphs by integer distances, but they often put all vertices on one circle. Conversely, placing points on a parabola or another rigid curve makes general position nearly automatic, but turns integer distance into a sparse Diophantine condition whose chromatic behavior is opaque.

Even the clique version illustrates the rigidity: a general-position integral clique of size seven is known, while the next case has resisted direct attack. An infinite-chromatic graph cannot therefore be expected to arise from simply enlarging cliques.

Where the natural approaches stalled #

Several standard coordinate systems expose only one half of the problem.

Universal finite-graph realizations control distances but are typically cocircular, violating the no-four-on-a-circle condition in the strongest possible way.Parabola and hyperbola parametrizations solve the incidence problem, but reduce adjacency to Pythagorean sum or product graphs over the rationals. Exact searches found small chromatic examples, not a mechanism forcing unbounded chromatic number.Finite-field parabola caps avoid collinear triples but produced low-degeneracy integer-distance graphs and many cyclic configurations.Naive homothetic Ramsey constructions can force chromatic complexity, but a finite homothetic Ramsey witness necessarily contains structured collinear subsets. General position cannot simply be appended afterward.

The underlying mismatch was trying to make the

points themselves carry both the Ramsey structure and the incidence genericity. The successful construction assigns those jobs to different geometric objects and different stages.## The change of coordinates: circles first, points later

The key move is to construct a graph as a

circle tangency graph and only afterward extract planar points.For positive circles with rational centers and rational radii, external tangency gives

Thus tangency already supplies rational center distances. After a common scaling, those distances become integers. Circle configurations also have enough continuous algebraic freedom to impose genericity without destroying their prescribed tangencies.

This separates the proof into three independent tasks:

• build finite rational circle tangency graphs of arbitrarily high chromatic number;
• use circle inversion to make their centers geometrically generic;
• place countably many finite point blocks together without creating mixed degeneracies.

The Hales--Jewett tangency booster #

Suppose a finite circle family indexed by an alphabet

α

has no proper coloring byk

colors. Hales--Jewett supplies a finite word dimensionι

such that every coloring of the wordsι → α

contains a monochromatic combinatorial line.For positive weights

γᵢ

, each word determines weighted center and radius data. The construction introduces:- a large circle for every word; - a small homothetic copy of the old family for every combinatorial line;

• one matched tangency between each word on that line and its corresponding circle in the small copy.

If the new family had a

(k+1)

-coloring, Hales--Jewett would give a monochromatic line among the large circles. If a matched small circle used that color, its matched tangency would be monochromatic. Otherwise the entire small copy avoids that color and induces ak

-coloring of the old family, again impossible. This raises the required number of colors by one.The combinatorial identity is easy; preserving geometry is not. The induction maintains a

GoodFamily

invariant:- every radius is positive;

• centers are injectively indexed;
• no distinct pair is internally tangent;
• no distinctly indexed triple is coaxial.

Every possible failure for the large word circles is represented by an explicit multivariate polynomial in the weights and large radius. Pair and triple nonidentity lemmas show that their finite product is nonzero. Polynomial extensionality on an infinite rational box then chooses positive rational weights and a sufficiently large rational radius avoiding every failure simultaneously.

Each small line copy is adjoined in a rational direction on the unit circle. A second finite product of univariate exceptional polynomials excludes mixed center collisions, internal tangencies, and coaxial triples. Iterating from one circle yields finite

positive rational good circle families with arbitrarily high tangency chromatic number.## Why inversion fixes general position

Taking the original circle centers would not suffice. Instead, invert the circles about a generic rational center

O

. For a circle with centerc_i

and radiusr_i

, writeWhen

D_i≠0

, the image circle has relative centerThree such centers are collinear precisely when a denominator-cleared determinant vanishes. As a polynomial in

O

, that determinant is identically zero exactly for a coaxial source triple. The induction has already excluded those triples.The quadruple condition is subtler. Its cleared cyclic determinant is again a polynomial in

O

. If it vanished identically, a Lorentzian circle-space argument would force four positive circle vectors into a forbidden pairwise-orthogonal configuration. The formal Gram-determinant identity rules this out whenever the relevant source triples are noncoaxial.There are only finitely many denominator, triple, and quadruple conditions. Their product is a nonzero bivariate polynomial, so one

rational inversion center avoids all of them. The inverse centers therefore have nonzero orientation for every distinct triple and nonzero cyclic determinant for every distinct quadruple.Tangency survives in the exact form

All terms are rational. A single positive natural multiplier clears the denominators of every signed transformed radius. Uniformly scaling the inverse centers then turns every required tangency edge into a positive integer-distance edge while preserving general position.

The final obstacle: combining all finite witnesses #

Unbounded finite chromatic number is not yet one infinite example. Arbitrary translations of finite blocks preserve their internal integer distances, but may create new collinear triples or concyclic quadruples involving several blocks.

The blocks are inserted recursively. A new block is translated by

For each insertion, every mixed collision, orientation, and cyclic determinant becomes an explicit univariate polynomial in

t

. The one-moving and three-moving cases have a leading coefficient equal, up to sign, to a nonzero orientation. The decisive two-moving/two-fixed cyclic case has coefficientsIf both vanished, the product

would vanish. Both pairs are distinct, so this is impossible. Hence every mixed exceptional polynomial is genuine. A rational

t

avoids their finite product.A verified prefix state stores all parameters chosen so far together with a proof of strong general position. Earlier parameters remain unchanged when a block is added. Any finite tuple of points in the eventual countable union appears in some later verified prefix, so global general position follows. Translation preserves every within-block distance, and the

k

th block still defeats everyk

-coloring. Therefore the final integer-distance graph has no finite proper coloring.## Formal verification

The proof is fully machine-checked in

Lean 4 + Mathlib against the original pinned statement, not a weakened surrogate. The final theorem is:

theorem Erdos130.erdos130_infinite_chromatic :
    ∃ A : Set Point,
      A.Infinite ∧ GeneralPosition A ∧ ∀ k : ℕ, ¬ HasKColoring A k

Verification included:

• a clean lake clean && lake build

of the checker project; - an empty scan for sorry

,admit

, or declared axioms; - an axiom audit showing only Mathlib's standard propext

,Classical.choice

, andQuot.sound

; - a second self-contained build of the archived F-017 proof project;

• an independent referee rerun and acceptance.

The final proof artifact is

verified_math/F-017_erdos130-infinite-chromatic-solution/Research/InfiniteAssembly.lean

; the exact verifier-facing theorem is inResearch/Basic.lean

in the same archived project.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 4. Erdős Problem #254Erdős Problem www.erdosproblems.com/254## ›Question

Let be such thatandfor every , where is the distance of from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of .

(Erdős Problem #254 — number theory — https://www.erdosproblems.com/254)

›Result #

Erdős Problem #254 is true: if A ⊆ ℕ has dyadic shell counts tending to infinity and ∑_{n∈A} ‖θn‖ = ∞ for every real 0 < θ < 1, then every sufficiently large natural number is a sum of distinct elements of A.

namespace Erdos254

/-- Erdős Problem 254. -/
theorem erdos_254 : Statement :=
  FinalProof.erdos_254

end Erdos254

›Report #

The problem and why it is difficult #

Let

A ⊆ ℕ

. Assume that the number of elements ofA

in every dyadic shell(x,2x]

tends to infinity, and thatfor every

0<θ<1

, where‖x‖

is distance to the nearest integer. Erdős asked whether these two hypotheses force every sufficiently large integer to be a sum ofdistinct elements ofA

.The hypotheses control two very different phenomena:

• dyadic abundance gives enough additive growth to build sets of subset sums with bounded gaps;
• phase divergence excludes rational and irrational Bohr obstructions.

Neither condition alone is close to sufficient. The real difficulty is to assign disjoint elements of

A

to several roles—two piecewise-Bohr classes, a phase-correction class, and a final syndetic class—without destroying the phase hypothesis or reusing a summand.## Where the natural approaches stalled

Several tempting shortcuts are false.

Coloring dyadic shells and selecting one “good” color does not preserve every phase. Convergent phases form an additive subgroup, but an intersection of four such subgroups can be irredundant. Thus full divergence for the union does not imply full divergence for one color.Shell-local reserve choices can be defeated after the fact. A concrete four-point shell shows that every one-point reserve can be made the unique nonmultiple of a suitably chosen modulus.Finite modular coverage is not enough. We proved exact tail subset-sum coverage modulo every integer, but irrational Bohr obstructions remain.Choosing correction supports after constructing the Bohr system is circular. Enlarging an interval to accommodate corrections moves the base representations and can reintroduce collisions.Merely rerunning the standard ergodic proof was not practical. The usual Bergelson–Furstenberg–Weiss proof passes through a symbolic system and its Kronecker factor, infrastructure not already available in Mathlib.

The key was therefore to solve the allocation problem globally and replace the missing ergodic machinery by a finite-cyclic spectral proof that could be kernel-checked from first principles.

First breakthrough: countably many bad phases #

The decisive structural observation is that dyadic abundance makes the set of phases with finite total mass

countable.For a fixed bound on

two sufficiently close phases cannot both satisfy that bound. Indeed, if their difference is

δ

, look at a dyadic shell at scale about1/(8δ)

. Every element of that shell contributes a controlled positive amount to the difference phase, and the growing shell cardinality contradicts the assumed bound. Hence every bounded phase sublevel is finite, and the union of those sublevels is countable.This converts an uncountable allocation problem into a countable diagonalization. We split off a shell-abundant seed, enumerate only its countably many convergent phases, and balance reserves against those phases. The resulting reserve has syndetic distinct subset sums, while its actual complement still has divergent phase mass for

every nonzero phase. Splitting the reserve by rank produces three pairwise-disjoint syndetic finite-sum classes and a disjoint universally phase-divergent correction class.That resolves the support-allocation obstruction completely.

Second breakthrough: a finite-cyclic proof of the BFW theorem #

The remaining input was the Bergelson–Furstenberg–Weiss theorem: the sum of two syndetic subsets of

ℕ

contains a piecewise-Bohr set.Instead of formalizing an abstract Kronecker factor, we built the spectral argument from finite cyclic groups.

Dense aligned blocks

A syndetic set has a uniformly positive number of points in long finite blocks. Given dense blocks from two syndetic sets, finite cyclic averaging finds a large fiber on which all pairs have the same exact sum. A dense subblock of that fiber has the property that each positive internal difference, after one common translation, belongs to the original sumset.

Exact spectral measures

For a signal

Φ : ZMod N → ℂ

, we proved Parseval’s identity for Mathlib’s unnormalized DFT:Weighting the

N

th roots of unity by these squared Fourier magnitudes gives an exact probability spectral measure. Its Fourier coefficients are normalized cyclic autocorrelations, and its mass at the trivial character is the normalized squared mean of the signal.A cofinal ultrafilter and compactness of probability measures produce a limiting circle measure. Portmanteau’s theorem preserves a positive atom at

1

, while positivity of a limiting Fourier coefficient forces the corresponding finite pattern to translate into the syndetic sumset.### Wiener decomposition and piecewise Bohr structure

For an atomless finite circle measure, we formalized Wiener’s lemma directly. The normalized geometric kernel tends to zero off the diagonal, the diagonal has product measure zero, and dominated convergence gives

Every finite measure then splits into:

• a countable atomic Fourier series, uniformly approximable by finitely many characters;
• an atomless remainder with squared-Cesàro-null Fourier coefficients.

The positive atom at

1

makes the finite atomic approximation uniformly positive on a finite-dimensional Bohr neighborhood. The error is smaller than a fixed threshold on a thick set. Their intersection is therefore contained in the Fourier-positivity set.Finally, compact-rotation return times are syndetic. This lets a smaller pure Bohr neighborhood embed into the piecewise-Bohr set, and the finite-embedding ultrafilter argument transfers it into the original sumset. This yields the full BFW theorem in exactly the finite-torus form required by the number-theoretic argument.

Final assembly #

Apply BFW to two of the three disjoint syndetic finite-sum classes. Their sum contains a finite-dimensional piecewise-Bohr return set.

The universally phase-divergent correction class has distinct subset-sum phases dense in the relevant closed torus subgroup. Compactness supplies finitely many corrections that move every large orbit point into the BFW open set. Because all source classes were chosen disjointly in advance, these corrections cannot reuse a base summand. The third syndetic class fills the remaining bounded gaps.

Consequently, every sufficiently large natural number is represented by a finite set of distinct elements of

A

.## Verification

The formal statement was pinned independently before proof development. The checker byte-compares the canonical statement and root import, rejects every

sorry

oradmit

, deletes project build objects, rebuilds the complete dependency graph, kernel-checks the exact theorem type, and audits all transitive axioms.The accepted command was:

cd /home/azureuser/snapshot && check_answer/verify.sh

Its final output was:

Build completed successfully (8617 jobs).
Erdos254.erdos_254 : Erdos254.Statement
'Erdos254.erdos_254' depends on axioms: [propext, Classical.choice, Quot.sound]
PASS: canonical Erdős 254 statement has a placeholder-free kernel proof

Thus the proof uses only Lean/Mathlib’s standard quotient, extensionality, and classical-choice axioms, with no project-added axiom or proof placeholder.

›Download Full Solution & Verify with Your AI #

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 5. Erdős Problem #267Erdős Problem www.erdosproblems.com/267## ›Question

Let and be the Fibonacci sequence. Let be an infinite sequence with . Mustbe irrational?

(Erdős Problem #267 — irrationality — https://www.erdosproblems.com/267)

›Result #

For every infinite sequence n₁ < n₂ < ⋯ with a uniform ratio gap n_{k+1}/n_k ≥ c for some c > 1, the sum Σ 1/F_{n_k} of reciprocal Fibonacci numbers is irrational. This holds for every c > 1, closing the range 1 < c < 2 that Badea (1993) left open.

noncomputable def reciprocalFibSeries (n : ℕ → ℕ) : ℝ :=
  ∑' k : ℕ, (Nat.fib (n k) : ℝ)⁻¹

/-- The problem's uniform ratio-gap condition. -/
def HasRatioGap (n : ℕ → ℕ) : Prop :=
  ∃ c : ℝ, 1 < c ∧ ∀ k : ℕ, c ≤ (n (k + 1) : ℝ) / (n k : ℝ)

/-- A faithful formalization of Erdős Problem 267. -/
theorem erdos_problem_267
    (n : ℕ → ℕ)
    (hpos : ∀ k : ℕ, 0 < n k)
    (hmono : StrictMono n)
    (hgap : HasRatioGap n) :
    Irrational (reciprocalFibSeries n)

›Report #

The problem and why it is difficult #

Let , , and let be any infinite index sequence with a uniform ratio gap for some . Erdős asked whether

must be irrational.

For fast-growing gaps this is classical territory: when the series is covered by known irrationality criteria for lacunary series (Badea, 1993). The genuinely open range was , where the terms shrink too slowly for size-based criteria — the tail of the series is not small enough compared with its leading term to force a contradiction from a single denominator. Any proof must instead exploit the precise arithmetic of Fibonacci numbers, not just their growth.

Where the natural approaches stalled #

Pure size arguments fail. Below , the tail can be comparable to , so the classical "the fractional part cannot be that small" argument does not close.Working modulo one denominator loses the structure. Individual share deep divisibility relations (periods, gcd identities); rationality forces global coherence conditions acrossallselected indices simultaneously, which no single modulus sees.Golden-ratio expansions need exactness. The identity converts the series into a Lambert-type series in , but making "the coefficients cannot all cancel" rigorous requires controlling a lattice of quadratic integers, not an archimedean estimate.

The proof architecture #

The formal proof assumes a rational (more generally, a

scaled-golden) total and derives a contradiction in three stages.1. Exact Lambert and quadratic-norm infrastructure. The reciprocal Fibonacci expansion is collected into a locally finite integer coefficient word over . A rational total forces normalized residuals to lie in a fixed lattice, and a sufficiently longequal / mismatch / equalcomparison between two windows of the word produces a nonzero quadratic integer whose norm lies strictly between and — impossible. The rest of the proof engineers such a comparison.2. Reduction to bounded two-adic order. If the selected indices contain arbitrarily deep dyadic structure (unbounded two-adic order), they must contain a complete selected dyadic tail; such tails can be deleted exactly, preserving both the ratio gap and the scaled-golden total, and only finitely many disjoint tails can exist. This reduces any putative rational counterexample to one with uniformly bounded selected two-adic order.3. The reverse-window contradiction. For the bounded-order remainder, the proof selects arbitrarily late "genuinely new" prefix periods, makes the reduced period quotient odd, and controls compatibility conditions with an exact offset count on a linear-width budget. Protecting two affine window centers by a polynomial CRT density argument isolates a singleton target inside a short radius; a protected sieve plus the norm gate from stage 1 then contradicts the assumed total. The cutoff at which this happens is explicit — polynomial in the period data — so the argument closes without any unproved case.Combining the two branches eliminates every rational value, for every sequence with any uniform ratio gap .

Verification #

The faithful statement quantifies over all index sequences with the exact quotient condition from the problem:

theorem erdos_problem_267
    (n : ℕ → ℕ) (hpos : ∀ k, 0 < n k) (hmono : StrictMono n)
    (hgap : HasRatioGap n) :
    Irrational (reciprocalFibSeries n)

where

reciprocalFibSeries

is the realtsum

of(Nat.fib (n k))⁻¹

andHasRatioGap

asserts one real with for all . The pinned project builds with warnings promoted to errors (lake --wfail build

), a source scan finds no proof placeholders, and#print axioms

reports exactly[propext, Classical.choice, Quot.sound]

. The download bundle contains the pinned statement project, the self-contained standalone artifact, and the checker documentation with the line-by-line fidelity audit.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 6. Erdős Problem #320Erdős Problem www.erdosproblems.com/320## ›Question

Let count the number of distinct sums of the form for . Estimate .

(Erdős Problem #320 — number theory, unit fractions — https://www.erdosproblems.com/320)

›Result #

Let P(x)=1 for x≤exp(3) and P(x)=log(x)P(log(x)) for x>exp(3). There exist constants c,C>0 such that eventually c(N/log N)P(log log N)≤log S(N)≤C(N/log N)P(log log N); equivalently S(N)=exp(Θ((N/log N)∏_{j≥3, stopped}log_j N)).

/-- Final machine-checked estimate: log S(N) is bounded above and below by
positive constants times the fully stopped iterated-log product scale. -/
theorem exists_two_sided_full_product_estimate :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ᶠ N : ℕ in atTop,
      c * ((N : ℝ) / Real.log N) *
          Research.renewalProduct N (Research.logLogNat N) ≤ Research.logS N ∧
      Research.logS N ≤ C * ((N : ℝ) / Real.log N) *
          Research.renewalProduct N (Research.logLogNat N)

›Report #

The problem and why it is hard #

Let

There are subsets, but many can have the same sum. Estimating therefore means understanding an enormous family of

exact rational collisions. Neither extreme is informative: counting subsets ignores collisions, while putting every fraction over gives a support interval far too large to reveal the true scale.The answer contains not just , but a product of iterated logarithms. That makes the problem especially unforgiving: a fixed inefficiency at each renewal step becomes a factor such as , which is not a constant. A proof must retain asymptotic coefficient one through every active logarithmic level.

Where natural approaches stall #

Three otherwise reasonable approaches lose exactly the information the problem needs.

A global common denominator is too coarse. It controls the range of possible numerators but discards the prime-by-prime structure responsible for most collisions.Naive renewal estimates leak constants. Partitioning denominators by a large prime does produce the right recursive shape, but ordinary integral approximations introduce endpoint, floor, and prime-number-theorem losses. Repeating a factor smaller than one through levels destroys the claimed order of magnitude.Lower-bound constructions are not automatically collision-free. Multiplying a previously useful denominator by a new prime creates binary choices only if every possible signed reciprocal relation remains incompatible. A heuristic “the prime is large” argument is insufficient; numerator and reduced-denominator bounds must be exact.

The central issue was thus not merely finding a recurrence. It was finding formulations in which the recurrence has

unit leading coefficient and all remaining losses are summable across the full iterated-log depth.## The approach that worked

1. Turn equality of subset sums into a signed relation

Two subsets give the same value precisely when their symmetric difference yields

This exact reformulation identifies “good” denominators: indices whose inclusion cannot be changed inside a zero signed relation. Every set of good indices contributes independent binary choices, giving

2. Use the unique large prime for the upper renewal

A denominator has at most one prime factor above a chosen threshold. Partitioning by that prime separates the support into disjoint blocks. Smooth denominators are handled by a least-common-multiple bound; the other blocks reduce to smaller instances indexed by .

The key technical device is an

exact discrete benchmark Its renewal transform telescopes exactly. This avoids a Riemann-sum error at every level. A reserve term absorbs the smooth part and the finitely many low-index bins, yielding the full-depth upper bound.

3. Propagate good denominators with compatible primes

For the lower bound, the decisive arithmetic lemma is:

If is good and is prime with , then is good.

The proof reduces every relevant rational sum, bounds its numerator, and uses coprimality with to rule out cancellation. Generated products are then shown to be pairwise disjoint, producing an exact lower renewal.

A crude but explicit estimate

is sufficient. It permits all up to a constant multiple of .

4. Preserve coefficient one

The lower recurrence closes in the form

with coefficient

exactly one. Two effects make this possible:- since , the strict gain absorbs both the clean prime-number-theorem error and the floor error;

• discrete Abel summation makes the increasing exponential compatibility penalty enter with the favorable sign.

This is the point at which the full iterated-log scale becomes attainable.

5. Make the depth-dependent losses summable

Even a unit renewal has finite-mesh losses. At height , the proof evaluates a power tail with

The iterated-log product loses at most a factor . These losses are summable, and their total leaves a uniform coefficient at least , independent of the number of active levels. Adaptive tower cutoffs keep every tail inside the preceding induction range. At the maximal active height, the omitted terminal factors are bounded by one fixed constant, so the adaptive product is comparable to the fully stopped product.

The resulting estimate #

Define

Then there are constants such that, for all sufficiently large ,

Equivalently,

Verification #

The complete argument was formalized in

Lean 4 + Mathlib. The final theorem isResearchPNT.exists_two_sided_full_product_estimate

inverified_math/F-038_two-sided-full-product-estimate/lean/ResearchPNT/FinalEstimate.lean

.Verification is deliberately strict:

• the checker rejects sorry

,admit

, custom axioms,opaque

, andunsafe

escape hatches; - it builds the complete combinatorial, analytic, upper-renewal, and lower-renewal chain;

• it audits the exact final theorem with #print axioms

; - the only reported axioms are Mathlib’s standard propext

,Classical.choice

, andQuot.sound

; - the audited prime-number-theorem dependency is bundled locally, all remote revisions are pinned, and the project was rebuilt from an empty .lake

directory.

The clean build completed all 8,721 jobs and passed the theorem-closure audit. An independent referee reran the verification before accepting the result.

›Download Full Solution & Verify with Your AI #

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 7. Erdős Problem #321Erdős Problem www.erdosproblems.com/321## ›Question

What is the size of the largest such that all sums are distinct for ?

(Erdős Problem #321 — number theory, unit fractions — https://www.erdosproblems.com/321)

›Result #

If R(N) is the largest size of a subset of {1,…,N} whose reciprocal subset sums are all distinct, then R(N) = Θ((N/log N) ∏_{j=3}^{k(N)} log_j N), where k(N) is the last iterated logarithm above one fixed absolute threshold. Equivalently, there are absolute c,C>0 such that these two bounds hold for every sufficiently large N.

theorem erdos321_asymptotic : ∃ N₀ : ℕ, ∃ B c C : ℝ, 3 ≤ N₀ ∧ 192 ≤ B ∧ 0 < c ∧ 0 ≤ C ∧ ∀ n, N₀ ≤ n → ∃ d : ℕ, d ≤ n ∧ IsTerminalLogDepth B n d ∧ c * terminalReciprocalScale n d ≤ (extremalSize n : ℝ) ∧ (extremalSize n : ℝ) ≤ C * terminalReciprocalScale n d

›Report #

The problem and the obstruction #

Let be the largest size of a set for which all sums

are distinct. The answer is

where is the last iterated logarithm above a fixed absolute threshold.

The problem is difficult because a collision is an arbitrary signed reciprocal relation

not merely a pairwise coincidence. Local graph tests therefore miss the real obstruction. For example, even a set passing every relation of the form can still contain a larger-support collision.

There is a second, analytic difficulty. Each useful recursion replaces by a quantity on the scale of , so iterating it generates the factors . A proof at any fixed number of iterations is not enough: the number of relevant iterations tends to infinity, albeit as slowly as . Any fixed factor lost at every step becomes an unbounded error.

Why the established approaches stalled #

Earlier lower-bound constructions used denominators with specially separated prime factors or a greedy compatible-prime rule. These methods successfully produced any

fixed number of iterated-log factors, but controlling arbitrary signed relations forced substantial losses.The upper side counted all possible reciprocal subset sums using a common-denominator grid. This also produced iterated-log bounds, but in coordinates that did not transparently match the lower construction.

The central gap was therefore not the first few logarithms. It was

uniform depth:- lower and upper recurrences had to be put on the same kernel;

• prime-distribution errors had to remain controlled along every recursion orbit;
• constants could not be multiplied once per iterated logarithm;
• the inhomogeneous source term could not simply be discarded.

A midpoint-block argument illustrates the trap. It readily proves bounds involving , but loses a factor such as at every additional level. That is harmless at fixed depth and fatal at terminal depth.

The approach that worked #

1. Put both sides into one exact recurrence

For the lower bound, denominators were grouped by their largest prime factor. Instead of selecting one cofactor per prime, an entire optimal reciprocal-dissociated cofactor code was inserted into each good prime fibre. Bad primes were charged globally through the prime divisors of exact signed-sum numerators.

For the upper bound, let be the number of all reciprocal subset-sum values from , and put . Since every valid set of size creates values,

A smooth/large-prime decomposition and an LCM-grid bound gave an entropy recurrence in the same quotient classes as the lower recurrence.

A formally audited prime number theorem then showed that both normalized quantities are governed by the same positive discrete logarithmic operator

with a common adaptive endpoint .

2. Replace the recurrences by one positive Neumann model

After normalization by , all kernel errors were shown to be summable along every adaptive recursion chain. This is stronger than merely proving that the one-step error tends to zero.

The lower extremal function and upper entropy were then compared, up to fixed constants, with one stopped positive model

where is a fixed terminal threshold and .

This reduced the original problem to evaluating a single explicit finite Neumann series.

3. Remove the depth loss

The decisive estimate was a sharp additive comparison between one operator weight and the corresponding telescoping increment:

Consequently, every truncated operator mass differs from its exact difference by at most . Unlike a factor-two estimate, this does not impose a fixed loss at every level.

The lower proof then used

depth-dependent logarithmic blocks. At remaining depth , only a fraction on the order of of the available logarithmic interval is discarded. The mass losses are summable. The coordinate shifts are also summable because reverse logarithms separate geometrically: if all retained coordinates exceed a fixed threshold , thenThis yields a fixed positive fraction of the complete terminal product, uniformly over all depths.

4. Control the entire upper tail at once

The Neumann model was expanded into nonnegative depth terms plus one exact remainder. Every retained depth term is at most three times its corresponding iterated-log product.

Once the next iterate drops below , every possible leaf belongs to one fixed finite range. The model is bounded on that range by a fixed constant . Positivity then bounds the

whole unexpanded remainder by times the terminal depth term. This avoids paying another constant for each post-terminal step.Earlier products form a geometric tail because each new retained factor is at least . Hence their sum is bounded by the deepest product.

Combining both sides gives

and transferring back through the normalized extremal/entropy comparison proves the result.

Formal verification #

The proof was carried out in Lean 4 with Mathlib. The formalization includes:

• exact rational reciprocal sums;
• quantification over the full powerset;
• an attained finite maximum defining ;
• the combinatorial lower and entropy upper recurrences;
• the audited prime-distribution input;
• the uniform-depth Neumann analysis;
• existence of the terminal iterated-log depth;
• cancellation of the normalization to obtain the raw cardinality bound.

The final theorem is

Erdos321.erdos321_asymptotic

. Its constants are chosen before , terminal-depth existence is part of the conclusion, and there is no depth-dependent hidden constant.The acceptance gate builds the complete source closure, recompiles every Lean file with

hasSorry

promoted to an error, and audits the final theorem's transitive axioms. The final axiom set is exactly

[propext, Classical.choice, Quot.sound]

with no

sorry

,admit

,native_decide

, or project-local axiom in the proof.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 8. Erdős Problem #336Erdős Problem www.erdosproblems.com/336## ›Question

For let be the maximal finite such that there exists a basis of order (so every large integer is the sum of at most integers from ) and exact order (so every large integer is the sum of exactly integers from ). Find the value of

(Erdős Problem #336 — number theory, additive basis — https://www.erdosproblems.com/336)

›Result #

The limit is 1/3: for the attained maximal exact-order function h(r), lim_{r→∞} h(r)/r² = 1/3.

/-- An extremal function exists, and h(r)/r² converges to c for every
extremal function. -/
def HasProblem336Value (c : ℝ) : Prop :=
  (∃ h : ℕ → ℕ, IsExtremalFunction h) ∧
    ∀ h : ℕ → ℕ, IsExtremalFunction h →
      Filter.Tendsto (fun r : ℕ => (h r : ℝ) / (r : ℝ) ^ 2)
        Filter.atTop (nhds c)

theorem Erdos336.problem336 : HasProblem336Value (1 / 3 : ℝ)

›Report #

The problem and why it is difficult #

For each

r ≥ 2

, leth(r)

be the largest exact order of an asymptotic basis of variable order at mostr

. The problem asks for the limit ofh(r)/r²

.The difficulty is not the lower bound: explicit periodic bases already suggest the quadratic scale and the coefficient

1/3

. The hard direction is auniform upper bound for every asymptotic basis. Three layers interact:- the original set is infinite and only represents sufficiently large integers;

• after normalization, the relevant obstruction lives in finite cyclic groups;
• the sharp coefficient depends on rank-one geometry, so a coarse small-doubling theorem loses too much.

Even after reducing to a finite cyclic problem, one must show that a primitive set with short variable-length representations has a short common exact representation length. The extremal configurations resemble thin progressions, and every error of one fibre can change the sharp

1/3

coefficient.## Where the natural approaches stalled

A first route was to import a general inverse theorem for small-doubling sets. That was both much heavier than necessary and insufficiently sharp at the endpoint. A more specialized route used Lev’s 2020 moderate-torsion argument, but formalization exposed two genuine obstructions.

First, a printed unique-difference estimate loses a factor of two. The claimed bound is contradicted by

A = {0,1,3} ⊂ Z/6Z,

which has four uniquely represented ordered differences although

|A|²/4 = 9/4

. The prose argument counts undirected Mantel edges as if they were ordered differences. The high-power setting repairs this through Ruzsa’s triangle inequality, but the printed lemma cannot simply be imported.Second, the endpoint representation-selection argument omits a critical three-point case. For

C = {0,x,2x},

the two new sums are

3x

and4x

. Their unavoidable endpoint loads are1

and3

, not the balanced bound2

needed by the generic counting argument. Reorienting the progression does not fix this. Pure deficiency arithmetic remains short by exactly one far-fibre term, and treating the progression quotient as an immediate rank-one certificate is unsafe because its lift can retain two independent directions.These failures identified the real bottleneck: the proof needed exact endpoint geometry, not a broader inverse theorem.

The route that worked #

The proof first transfers the infinite problem to a finite cyclic removal statement. A dyadic high-power argument finds a scale with doubling below

9/4

. Dense alternatives, bounded quotient alternatives, and rank-one alternatives are then handled separately. The rank-one endgame is encoded by an exact two-generator lattice diagram; its L-shape area inequality gives

3|G| ≤ (H+2)²,

which is the geometric source of the coefficient

1/3

.The central structural step rectifies a cyclic set into a graph

T ⊂ ℤ × ZMod N

supported between two occupied integer fibres,

0

andl

. Quotienting by the displacement between these endpoints produces a finite endpoint quotientB

. LetF

be the Kneser stabilizer ofB+B

, letC=B/F

, and let

D = (C+C) \ C

be the genuinely new sum classes.

The proof then exhausts the endpoint possibilities:

|D|=0

gives the desired progression-plus-subgroup certificate directly;|D|=1

is excluded by a sharp two-piece projection inequality;|D|≥3

in the nonvertical branch is excluded by representation selection or a two-class/three-sum-class quotient;- a vertical stabilizer forces the double-set saturation defect to be no larger than the original-set defect, contradicting full primitivity;

• the remaining |D|=2

nonvertical case is resolved by a complete classification of three-point critical sumsets.

That final classification was the decisive local breakthrough. Every three-point set with five double sums has one of three forms:

• a load-two selector exists;
• a subgroup quotient has two classes for the set and three for its double;
• the set is the genuine progression {0,x,2x}

.

The first two forms are ruled out by the existing sharp inequalities. In the progression form, direct integer-projection fibre geometry supplies the missing information that deficiency counting could not see, and excludes the branch.

From normalized endpoints back to the original set #

The endpoint theorem initially applies only to a normalized rectified graph. Four exact transport results connect it to the original cyclic set:

• translation preserves cardinality, doubling, affine generation, and subgroup-saturation defects;
• strict-half rectification preserves |A|

,|A+A|

, and the number of quotient fibres; - lifted progression certificates descend to cyclic rank certificates;

• the homomorphism

θ(i,x) = π(x) - i

vanishes on the rectified graph. Consequently, the vertical preimage of the endpoint stabilizer lies inside the rectifying kernel

π.ker

.This last observation permits

relative vertical primitivity instead of an unjustified absolute assumption. The normalized endpoint assembly therefore proves the fully primitive rectifiable theorem. Balanced and small-defect subgroup quotients then descend by strong induction, yielding the full rectifiable3n-3

theorem. The finite high-power reduction and infinite transference complete the upper bound, while the periodic construction supplies the matching lower bound.A final statement audit also closed a logical loophole: merely proving convergence for every extremal function could be vacuous if no such function existed. Eventual cyclic bounds can be padded with retained zeros to cover every smaller parent length; they therefore bound every admissible exact order. Since exact order one is always attainable,

Nat.findGreatest

selects an attained finite maximum for eachr≥2

. The final theorem explicitly proves both existence and convergence.## Verification

The result is formalized in Lean 4.31.0 with Mathlib revision

fabf563a7c95a166b8d7b6efca11c8b4dc9d911f

.The executable checker:

• validates a SHA-256 manifest of all 191 research source files;
• builds the complete final dependency graph ( 8729

build jobs); - checks an independently duplicated, nonvacuous statement of the problem;

• rejects sorry

,admit

, and project-declared axioms throughout the research tree; - runs #print axioms

on the final theorem.

The only reported dependencies are Lean’s standard

propext

,Classical.choice

, andQuot.sound

. The checker ends with:

PASS: Erdős Problem 336 has verified value 1/3.

Thus the limit is exactly

1/3.

›Download Full Solution & Verify with Your AI #

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 9. Erdős Problem #394Erdős Problem www.erdosproblems.com/394## ›Question

Let denote the least such thatIs it true thatfor some ?Is it true that, for ,

(Erdős Problem #394 — number theory — https://www.erdosproblems.com/394)

›Result #

Both questions in Erdős Problem 394 have affirmative answers: one may take c = 1/2048 in Σ_{n≤x} t₂(n) ≪ x²/(log x)^c. For every fixed integer k ≥ 2, one also has Σ_{n≤x} t_{k+1}(n) = o(Σ_{n≤x} t_k(n)) as x → ∞.

/-- The affirmative assertion in the first question. -/
def FirstQuestion : Prop :=
  ∃ c : ℝ, c > 0 ∧
    (fun x : ℝ ↦ Tsum 2 x) =O[atTop]
      (fun x : ℝ ↦ x ^ 2 / (Real.log x) ^ c)

/-- The affirmative assertion in the second question. -/
def SecondQuestion : Prop :=
  ∀ k : ℕ, k ≥ 2 →
    (fun x : ℝ ↦ Tsum (k + 1) x) =o[atTop]
      (fun x : ℝ ↦ Tsum k x)

theorem erdos394_first_target : FirstQuestion
theorem erdos394_second_target : SecondQuestion

›Report #

The problem—and the real obstruction #

For positive integers , let be the least positive integer such that

Erdős Problem 394 asks two average-order questions. Does some satisfy

And, for every fixed , is

The difficulty is not merely that is irregular. Its large values are structurally unavoidable. If is prime, then

in particular, . Thus no uniform pointwise saving can prove either assertion. Even the elementary monotonicity is far too weak: the second question asks for a ratio tending to zero after summation.

Both questions nevertheless have

affirmative answers. The first estimate holds with the explicit choice , and the adjacent sums satisfy the requested little-o relation for every fixed .## Why the natural attacks stalled

The failed approaches exposed four distinct traps.

Pointwise estimates attack the wrong phenomenon. Prime inputs keep nearly as large as . The saving exists only after the arithmetic structures of many integers are aggregated.An upper-bound sieve proves only half the theorem. It is possible to make the -sum small by sieving medium prime factors, but comparison with also requires a denominator lower bound that preserves a stronger Euler factor.Crude Euler estimates destroy the adjacent-length gap. The saving between and is encoded in a precise powered inequality. Estimating the products separately loses exactly the small exponent difference needed at the end.A sparse subsequence does not settle an all- asymptotic. An early hierarchy at cutoffs gave valid and strong finite bounds. But neighboring cutoffs were separated by enormous factors, so monotonicity could not interpolate the ratio estimate. The finite work was useful; the grid itself was a dead end.

The conceptual mistake behind the most natural sieve route was therefore to view the numerator as the whole problem. The decisive step was to build the numerator and denominator

as a matched pair, retain their exact Euler-product relationship, and place both estimates on a dense multiplicative grid.## The finite numerator mechanism

Fix an adjacent length parameter , a cutoff , and an interval of medium primes . For each , extract the squarefree product of the primes from which divide . Integers divisible by some , with , form a controlled exceptional set.

For all remaining integers, admissible starts can be encoded prime by prime. The proof packages these local choices into a finite

root box. A lattice-counting and moment argument bounds the mean least admissible start over that box. It then combines this bound with an even Bonferroni truncation and a completely explicit finite Brun sieve.The result is a global upper bound for

consisting of a sieve-density Euler main term and explicit square-prime and Brun-tail errors. Progression discrepancies, elementary-symmetric tails, and truncation losses are all handled as finite inequalities; no asymptotic sieve theorem is inserted as an unproved black box.

The missing denominator #

For a selected squarefree modulus , attach a prime larger than every medium prime and consider . Most unit residue classes of avoid all short shifted-product representations. For a prime in one of those good classes, the least valid start is forced to be large, giving a lower bound for .

A second finite prime sieve lower-bounds the weighted mass of the good primes. These contributions can then be summed over many selected moduli . Because the attached prime lies above the medium-prime range, unique factorization makes

injective. No denominator mass is counted twice.

After controlling floors and the subset truncation, this construction produces a lower bound for

with an enhancement factor

That enhancement is the feature a generic lower bound misses, and it is precisely what makes adjacent lengths separate.

The key insight: keep the Euler gap exact #

The numerator density and denominator enhancement obey an exact powered comparison. With

the relevant products can be arranged into an inequality of the form

The extra power on the right is the fixed saving. Rather than approximate each product independently, the proof carries this identity intact until elementary reciprocal-prime and endpoint-density estimates turn it into a logarithmic gain.

This is the central mathematical insight of the proof:

the little-o statement comes from an algebraic gap between two matched Euler products, not from a stronger standalone estimate for either sum.## The dense hierarchy

To turn the finite estimates into an asymptotic valid at every cutoff, use

and choose the lower and upper medium-prime scales using the exponents and . A generous polynomial dilution and an even Brun order leave enough room for all root-box, tail, and denominator conditions.

The crucial strengthening is uniformity between grid points. For each fixed , the formal proof establishes that, eventually in ,

every natural cutoff satisfyingobeys

Unlike the abandoned sparse hierarchy, this grid has bounded multiplicative gaps, and the estimate already covers each entire gap.

For a large real , take and . Exact natural-logarithm inequalities place in the required interval. Since , for every it eventually exceeds . The boxed estimate then gives

which is exactly the epsilon definition of the desired little-o relation.

Verification #

The proof is formalized in

Lean 4 with Mathlib. The formal statement preserves every important detail of the original question:t k n

is the leastpositive start;- the consecutive product is exact natural-number arithmetic; Tsum k x

sums overFinset.Icc 1 ⌊x⌋₊

;- the conclusions use Mathlib's IsBigO atTop

andIsLittleO atTop

; - the second assertion quantifies over every fixed natural .

The final archive contains 106 Lean source files. Its verifier scans every source for

sorry

,admit

, and addedaxiom

declarations, builds the complete dependency closure, and directly elaborates the file containing both final target theorems. The full build completed successfully, and the definitive output was:PASS: both faithful Erdős 394 targets are proof-escape-free and accepted by Lean The source-only closure was also rebuilt during independent review, and Colin accepted the result for publication.

›Download Full Solution & Verify with Your AI #

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 10. Erdős Problem #415Erdős Problem www.erdosproblems.com/415## ›Question

For any let be the largest such that any of the possible ordering patterns appears in some sequence of with . Is it true thatfor some constant ? Is the first pattern which fails to appear alwaysIs it true that the 'natural' ordering which mimics what happens to is the most likely to appear?

(Erdős Problem #415 — number theory — https://www.erdosproblems.com/415)

›Result #

All three questions answered. (1) No — F(n) = o(log log log n), so no constant c > 0 gives F(n) = (c+o(1))·logloglog n; kernel-proved via the decreasing-run bound and the F ≤ G bridge. (2) No — the decreasing pattern is not always the first to fail: F(826)=3 while φ(823)>φ(824)>φ(825)>φ(826), certified by an independent exact Euler-sieve checker. (3) No — the 'natural' ordering (which has a tie, φ(1)=φ(2), so it is formalized with weak patterns) is not the most frequent: kernel theorems refute it under both the eventual-maximality and limiting-frequency readings.

/-- The longest decreasing run is little-oh of the triple logarithm. -/
theorem G_ratio_tendsto_zero :
    Tendsto (fun X : ℕ ↦ (G X : ℝ) / tripleLog X) atTop (𝓝 0)

›Report #

The problem and its interpretation #

For let be the largest such that

every one of the ordering patterns occurs in some block with . Erdős Problem #415 asks three questions:- Is for some constant ?

• Is the first pattern that fails to appear always the strictly decreasing one?
• Is the "natural" ordering — the one mimicking — the most likely to appear?

For the first two questions, "the possible ordering patterns" is formalized as strict permutations (tied blocks realize no strict pattern), matching the problem's own count of . The third question

cannotbe read strictly, because — the natural reference pattern has a tie. It is therefore formalized with weak comparison patterns and answered under both standard asymptotic readings: eventual cumulative maximality, and maximal limiting cumulative frequency.## Question 1: no — the proposed asymptotic fails

The formal theorem proves , so no constant can satisfy the displayed asymptotic.

The mechanism: for all patterns to occur, the strictly decreasing pattern must occur, so , the longest strictly decreasing run of totient values up to . A decreasing run of length forces consecutive integers whose prime-loss profiles descend times in a row; an elementary prime-loss analysis shows such runs are shorter than every fixed multiple of . Kernel theorems

G_ratio_tendsto_zero

andnot_AsymptoticQuestion

close the question.## Question 2: no — an exact finite counterexample

, yet is strictly decreasing. So at the first failing length the decreasing pattern is present, and something else is missing. The value and the run are certified by an independent exact Rust checker (Euler sieve, exhaustive block scan, rank-vector census) that shares no code with the search that found the witness.

Question 3: no — equality cannot dominate #

At the natural reference order is

equality(), so the question becomes: do ties dominate both strict orders in frequency? The proof shows they cannot.Write the totient loss as and truncate at a prime cutoff . Equal consecutive totients force the exact identity , which is eventually tiny. The finite-prime part of the adjacent difference splits into a six-periodic base (primes 2 and 3) with a positive minimum separation , plus a period- extra term coprime to 6. A CRT injection shows at most of every indices can land within of any target — concentration is impossible beyond density -ish. Combining this with mean tail bounds for the omitted large primes, the density of ties is eventually below , while equality, increase, and decrease partition all two-blocks. So some strict order beats the natural (equality) order at every large cutoff, and if the three limiting frequencies exist they sum to one with equality's at most . Kernel theorems refute both

EventuallyNaturalIsMostFrequentK2

andLimitingNaturalIsMostFrequentK2

.## Verification

All Lean results build sorry-free with standard axioms only (

propext, Classical.choice, Quot.sound

); the finite witness passes the independent exact checker. The download bundle contains the pinned strict formalization, the proof project, the counterexample candidate with its checker, and the fidelity audit documenting every interpretation choice above.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 11. Erdős Problem #450Erdős Problem www.erdosproblems.com/450## ›Question

How large must be such that the number of integers in with a divisor in is at most ?

(Erdős Problem #450 — number theory, divisors — https://www.erdosproblems.com/450)

›Result #

For every fixed real ε>0 there is a constant C(ε) such that y≥C(ε)n suffices uniformly for every natural translate x and all sufficiently large n; concretely, if Sε is a finite set of primes at least 5 with ∑_{p∈Sε}1/p>152/ε, then C(ε)=∏_{p∈Sε}p²+2 works. Conversely, for every 0<ε<1 every sufficient eventual threshold is greater than n for all sufficiently large n, so the sharp fixed-ε order is Θ_ε(n).

noncomputable def turanLinearAnswer (ε : ℝ) (n : ℕ) : ℕ :=
  n * (primeSquarePeriod (turanPrimeSet ε) + 2)

/-- Main upper bound: Erdős Problem 450 admits a translate-uniform linear scale
`y = C(ε)n`. -/
theorem turanLinearAnswer_isSufficientScale :
    IsSufficientScale turanLinearAnswer

/-- Every sufficient eventual threshold has to exceed `n` eventually for each
fixed `0 < ε < 1`. -/
theorem sufficientScale_eventually_gt_n
    (Y : ℝ → ℕ → ℕ) (hY : IsSufficientScale Y)
    (ε : ℝ) (hεpos : 0 < ε) (hεone : ε < 1) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → n < Y ε n

›Report #

The problem and its hidden difficulty #

Erdős asked how large an interval length must be before the integers in having a divisor in occupy at most an -fraction of the interval.

The natural uniform reading is adversarial in the translate: the estimate must hold for

every, not merely for a typical interval. That distinction is the main difficulty. Global density estimates—even very strong ones—do not prevent exceptional translates from containing dense clusters.There is also a genuine linear obstruction. Immediately after a suitable factorial translate, an interval of length contains qualifying integers. Thus no answer of order can work for fixed . The real question is whether one can prove a matching upper bound uniformly in .

Where the earlier routes stalled #

The first exact approach used periodicity. For fixed , divisibility by some is periodic, so the problem has a precise period-density criterion. This led to a complete fixed- dichotomy: an eventual threshold exists exactly when exceeds the density in one period.

That result was correct but did not solve the asymptotic problem. Its period is enormous, and it left open the essential assertion that the density tends to zero with .

A Möbius expansion improved the local discrepancy dramatically, replacing the full period by a subexponential coefficient norm. But this route still needed a formally imported global multiplication-table theorem, such as Ford's deep density estimate. More importantly, it obscured the simpler structure needed for a linear bound.

The conceptual mismatch was this:

global density machinery was being asked to solve a local, adversarial-translate problem. What was needed instead was a statistic that both concentrates on every long enough interval and behaves predictably when a bad integer is factored as .## The key breakthrough: finite-prime scores

Fix a finite set of primes, all at least five, and define

A second, two-level score also records repeated selected prime factors:

The decisive pointwise inequality is

If a selected prime divides both factors, its second occurrence is exactly what the -term records. This turns the factorization , with , into a usable local trichotomy.

Let

Both scores are periodic modulo . Exact first and second moments over a complete period give

Chebyshev's inequality therefore controls integers with unusually low score. A Markov estimate for square divisibility controls integers with unusually high two-level score. Periodicity transfers these estimates to

every interval, with only one fixed period of boundary loss.## The three-class decomposition

For every bad integer , choose a divisor and write . Then at least one of the following holds:

• ;
• ;
• .

Indeed, if the first two alternatives fail, the product inequality forces the third.

The three classes can be counted uniformly in the translate. Once and , their weighted contributions are at most

• for low-score divisors;
• for low-score quotients;
• for high two-level score.

Thus

for every .

The sum of the reciprocals of the primes diverges, so for each one may choose a finite with . The preceding inequality then gives the desired bound at the linear scale .

Why the order is sharp #

The factorial dense block supplies the matching lower obstruction. At length , one explicit translate has exactly bad integers. For every fixed , this violates the requested estimate for all sufficiently large .

Consequently, every sufficient eventual threshold must exceed eventually, while the finite-prime argument gives a constant multiple of . The optimal fixed- growth order is therefore

.## Formal verification

The complete argument was formalized in Lean 4 with Mathlib. The formal statement uses open intervals, natural translates, the real inequality “at most ,” and requires the estimate for every length above the threshold.

The main theorem is:

theorem turanLinearAnswer_isSufficientScale :
    IsSufficientScale turanLinearAnswer

A second theorem proves the matching eventual lower bound for every .

The hostile checker rejects

sorry

,admit

, local axioms, and unsafe declarations before building the standalone proof project. It reports:

Build completed successfully (8567 jobs).
PASS: Lean build succeeded and local sources contain no forbidden escape hatch

The proof is archived in

verified_math/F-013_turan-linear-scale/

.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 12. Erdős Problem #489Erdős Problem www.erdosproblems.com/489## ›Question

Let be a set such that . LetIf then is it true thatexists (and is finite)?

(Erdős Problem #489 — number theory — https://www.erdosproblems.com/489)

›Result #

Yes. For every A ⊆ ℕ with |A ∩ [1,x]| = o(√x), whenever the positive integers divisible by no member of A form an infinite set B = {b₁ < b₂ < ⋯}, the quantity x⁻¹ Σ_{bᵢ<x}(bᵢ₊₁-bᵢ)² converges to a finite real limit.

/-- A positive answer to Erdős Problem 489. -/
theorem erdos489_statement :
    ∀ A : Set ℕ,
      (fun x : ℕ => (((Finset.Icc 1 x).filter (· ∈ A)).card : ℝ))
          =o[atTop] (fun x : ℕ => Real.sqrt (x : ℝ)) →
      (sievedSet A).Infinite →
      ∃ L : ℝ,
        Tendsto (fun x : ℕ => gapSumSq A x / (x : ℝ)) atTop (𝓝 L)

›Report #

The problem—and the hidden difficulty #

Let be extremely sparse,

and let be the positive integers divisible by no member of . Erdős asked whether

always has a finite limit.

At first sight this resembles a routine finite-sieve approximation. Any sieve using only finitely many forbidden divisors is periodic, so its gap statistics have exact limiting averages. Sparse also forces the reciprocals of its increasing enumeration to be summable. Neither observation is enough: the expression is a

second moment, and a tiny amount of mass can escape to increasingly long gaps. Pointwise convergence of every fixed gap-length contribution does not justify exchanging a limit with the infinite sum.That uniform-integrability obstruction is the real content of the problem.

Where the natural approaches stalled #

Several plausible routes fail at exactly this boundary.

Take larger finite periodic sieves and pass to the limit. This controls every bounded gap pattern, but not the squared mass of gaps whose lengths grow with the cutoff. We formalized an abstract escaping-mass counterexample to this limit-exchange step.Sum shifted CRT estimates term by term. Counting one congruence class costs a harmless endpoint error, but paying that error independently for every divisor pair and every shift produces a divergent rank error.Use a stronger reciprocal moment. A direct incidence argument works under an extra hypothesis such as , where is the forbidden enumeration. That misses the sharp regime allowed by , including the logarithmic boundary models that make the problem difficult.Rely only on a maximum-gap estimate. Thinness does prevent gaps comparable with the whole prefix eventually, but this alone gives no summable control of the collective squared tail.

The successful proof therefore needed two ingredients at once: a global charge for long gaps that does not accumulate CRT endpoint errors, and a separate finite-word argument for bounded gaps.

The breakthrough: charge primitive coprime witness pairs #

Write the infinite forbidden set increasingly as . Thinness gives three crucial consequences:

• eventually ;
• ;
• the rank-pair kernel

is summable, with uniformly small high-rank tails.

The task is to make every long actual gap pay into this kernel.

A Mertens-free affine sieve

Inside a long covered gap, we look only at positions

where for a suitably chosen roughness threshold . This coordinate change has two decisive effects.

• Any forbidden modulus sharing a prime factor with is automatically unable to divide such an .
• For the remaining moduli, affine finite-sieve density is the same periodic product density as in the ordinary sieve.

Thus no Mertens estimate is needed. The loss of density contributes a factor , while the bad-pair estimate below gains exactly ; those powers cancel after squaring the candidate density.

A uniform interval-density lemma supplies linearly many affine candidates in every sufficiently long gap. Because the reciprocal mass of remote forbidden ranks is small, a divisor-label counting inequality

forces linearly many

distinct high-rank divisor witnesses.### Quadratically many coprime pairs

Among affine positions, pairs with a common prime divisor are rare. A common prime forces their difference to be divisible by , so each prime fiber is widely spaced. Summing the exact fiber bounds shows that the linearly many witnesses contain quadratically many ordered pairs of coprime positions. Quantitatively, each long gap of length receives enough pairs to pay for with one fixed constant.

Coprimality is the key structural move. If positions labelled by are written as

then coprimality of makes the quotient vector primitive. Repeated scalar dilations—the obstruction that defeated the naive pair count—disappear.

Primitive-ray capacity and global charging

For fixed labels , all quotient vectors lie in a thin diagonal strip: their covered coordinates are bounded by the prefix, while their difference is bounded by the gap length. Sorting primitive lattice rays by slope and summing consecutive determinants gives a sharp fan-area estimate. In formal cross-multiplied form, the number of possible occurrences satisfies

Distinct successive gaps inject into distinct quotient pairs, so this is a

global capacity bound rather than a separate CRT estimate for each gap. Summing all pair payments yieldsThe first term is uniformly small for high ranks by kernel summability. The endpoint term is at most the square of the forbidden counting function, hence is . A witness-forced maximum-gap lemma ensures all charged coordinates lie below a controlled multiple of the prefix. Together these facts prove

uniform integrability of the actual squared gaps: for every , some makes the normalized contribution of all gaps at least eventually smaller than .## From uniform tails to an actual limit

Long-gap control solves only half the problem. For a fixed cutoff , define a local word cost at an integer : it is when a sieve gap of length starts at , and zero otherwise. Summing these local costs over is exactly the sum of squared enumerated gaps shorter than .

A finite forbidden prefix makes this local word periodic, so its normalized average converges to its one-period mean. The full sieve and a sufficiently remote finite prefix disagree on few points: a canonical tail divisor labels every disagreement, and the same reciprocal-mass inequality bounds their density by

\text{tail reciprocal mass}+ rac{A(x)}x.Only starts whose length- window meets such a disagreement can change their local cost. Therefore every fixed truncated full-sieve average is eventually approximated arbitrarily well by a convergent periodic average, and hence converges.

Finally, the exact gap sum is the truncated average plus its long-gap tail. Applying the same uniform-approximation principle a second time gives convergence of the full normalized second moment.

Finite forbidden sets require a small separate argument: the sieve is periodic after the initial point, every gap is at most one product period, and a shifted periodic Cesàro average converges.

Formal verification #

The proof was formalized in

Lean 4.31.0 against Mathlib revisionfabf563a7c95a166b8d7b6efca11c8b4dc9d911f

. It proves the exact statement audited incheck_answer/README.md

, including the original inclusive counting function, theNat.nth

gap enumeration, and real squared differences.Two independent project builds passed:

cd workspace/experiments/experiment_1_formal_statement/lean
PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH" LEAN_NUM_THREADS=28 lake build

The archival package contains the complete dependency closure:

cd verified_math/F-061_erdos-489-positive-answer
PATH="$HOME/.elan/bin:$PATH" lake update
LEAN_NUM_THREADS=28 lake build

A source audit also found no

sorry

oradmit

in the F-061 Lean files. The independent referee reran the verification, checked statement fidelity, and accepted the solution.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 13. Erdős Problem #521Erdős Problem www.erdosproblems.com/521## ›Question

Let be independently uniformly chosen at random from . If counts the number of real roots of then is it true that, almost surely,

(Erdős Problem #521 — analysis, polynomials, probability — https://www.erdosproblems.com/521)

›Result #

No — the almost-sure convergence fails: for i.i.d. ±1 coefficients, R_n/log n does not converge to 2/π almost surely (the real-root count fluctuates by ≫ log n along nearby degrees). Erdős–Offord's 1956 in-expectation asymptotic stands, and the almost-sure law does hold for the roots inside [−1,1] (Do 2024) — the divergence comes from the outer roots, so this also resolves Pritsker's 2019 full-line strong-law question (AIM Problem 1.2) in the negative.

/-- The proposed almost-sure convergence of the real-root count. -/
def Claim : Prop :=
  ∀ {Ω} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (ε : ℕ → Ω → Bool), (∀ k, Measurable (ε k)) → iIndepFun ε μ →
    (∀ k, μ {ω | ε k ω = true} = 1/2) →
    ∀ᵐ ω ∂μ,
      Tendsto (fun n => (realRootCount ε n ω : ℝ) / Real.log n)
        atTop (𝓝 (2 / Real.pi))

theorem erdos_521_negative : ¬ Claim

›Report #

The problem and its history #

Let be independent fair signs and let count the real roots of . Erdős–Offord (1956) proved the in-expectation asymptotic , and convergence in probability followed in the same tradition (Ibragimov–Maslova). Erdős Problem #521 asks whether the convergence is

almost sure:The same question was posed to the community by Pritsker at the 2019 AIM workshop on zeros of random polynomials (Problem 1.2). The state of the art before this work: Yen Do (arXiv:2403.06353, 2024) proved the almost-sure law for the roots

inside and explicitly noted his method's limitation on the full real line — the outer roots, governed by the newest high-degree coefficients, were the open case.## The answer: no

The formal theorem is a disproof:

Erdos521.erdos_521_negative : ¬ Erdos521.Claim

Almost surely, does

not converge to : along a sparse sequence of "record" degrees the real-root count fluctuates by a positive multiple of . Combined with Do's inner-interval theorem, the divergence is localized entirely in the roots outside — the two results are complementary, and together they resolve Pritsker's full-line question in the negative.## Why this is delicate

A second-moment computation makes the a.s. law

lookplausible: , so deviations of order at any fixed degree are rare. The failure mechanism is not one bad degree butinfinitely many mildly bad windows: each new block of high-degree coefficients re-randomizes the outer root count, and rare deviations recur infinitely often by independence across scales. Turning that heuristic into a proof requires quantitative lower bounds on the probability of large root-count deviations conditioned on the past — precisely what classical CLT-type results do not give.## Proof architecture

Reduction to a first-moment gate. Record times with positive-probability conditioning cones convert the asserted almost-sure limit into an upper bound for fourth-integrated crossing counts: if the a.s. law held, the late cone-conditioned crossing mean would eventually be at most .Sharp early crossing mean. The unconditioned iid crossing mean is computed exactly at the needed scale.Local limit for signed strips. Splitting crossing events into balanced horizontal/vertical coordinates, a critical-cutoff local limit theorem is proved with explicit constant (), then bridged to exact finite axis words with all perturbation tails .Transfer to conditioned paths. The four event types transfer to quadrant-good paths with an explicit conditioning factor and exponentially small schedule error; an odd-coefficient twist identifies with a schedule-complement rotation.The contradiction. Summing conditioning weights bounds the normalized late mean by — strictly below the gate. Hence the a.s. law fails.

All constants in the chain are explicit; nothing is asymptotic hand-waving, because every step had to pass the kernel.

Verification #

The statement quantifies over any probability space carrying iid fair Boolean coordinates (canonically, Mathlib's countable product measure), counts distinct real roots of the Littlewood polynomial, and asserts the a.s. limit; the theorem is its negation. The verifier rebuilds the source closure, rejects

sorry

/admit

/axiom

throughout, checks the exact theorem type, and prints the axiom audit:

Erdos521.erdos_521_negative : ¬Erdos521.Claim
axioms: [propext, Classical.choice, Quot.sound]

The download bundle contains the full proof project (3,770 build jobs) and the one-command verifier (

verified_math/F-123_erdos-521-negative/verify.sh

).## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 14. Erdős Problem #522Erdős Problem www.erdosproblems.com/522## ›Question

Let be a random polynomial, where independently uniformly at random for . Is it true that, if is the number of roots of in , thenalmost surely?

(Erdős Problem #522 — analysis, polynomials, probability — https://www.erdosproblems.com/522)

›Result #

For every i.i.d. fair ±1 (Rademacher) coefficient sequence, the number of roots of ε₀ + ε₁z + ⋯ + εₙzⁿ in the closed unit disk, divided by n/2, converges to 1 almost surely — the almost-sure strengthening of Yakir's 2021 in-probability theorem.

/-- Roots in |z| ≤ 1, counted with algebraic multiplicity. -/
noncomputable def R {Ω : Type*} (ξ : ℕ → Ω → Bool) (n : ℕ) (ω : Ω) : ℕ :=
  closedUnitRootCount (littlewoodPolynomial ξ n ω)

def Erdos522Claim : Prop :=
  ∀ {Ω : Type u_erdos} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (ξ : ℕ → Ω → Bool),
    (∀ k, Measurable (ξ k)) →
    iIndepFun ξ μ →
    (∀ k, μ {ω | ξ k ω = true} = (1 : ENNReal) / 2) →
    ∀ᵐ ω ∂μ,
      Tendsto (fun n => (R ξ n ω : ℝ) / ((n : ℝ) / 2)) atTop (𝓝 1)

theorem erdos_522 : Erdos522Claim

›Report #

The problem and why it is difficult #

Let be independent fair signs and let count the roots of in the closed unit disk . Erdős asked whether

Random Littlewood polynomials concentrate their roots near the unit circle, and by symmetry roughly half the roots fall inside the closed disk

on average. Yakir (2021) proved the corresponding statementin probability. The almost-sure statement is strictly stronger: it must control the entire sequence at once, ruling out rare-but-recurring degree ranges where the count drifts, and the natural route — Borel–Cantelli — needs deviation probabilities that aresummable in, far beyond what an in-probability argument provides.## Where the natural approaches stalled

Upgrading by subsequences fails. Almost-sure convergence along a fast subsequence plus interpolation works for monotone quantities; the disk root count is not monotone in , and consecutive-degree fluctuations are exactly the danger.Soft compactness arguments lose quantitative control. The root measure converges weakly to the uniform measure on the circle almost surely, but weak convergence says nothing about theclosed disk boundary countat the needed rate — half the roots sit within distance of the boundary circle.Direct small-ball estimates on near the circle are too weak per-degree. They give power decay for one radius, not the joint angular control over all radii and shifts that a summable bound requires.

The argument that works #

The engine is a quantitative

angular (radial-cosine) moment estimate: for explicit exponents,where is a high mixed moment of the polynomial's angular oscillation data and measures the frequency shift. The proof of this estimate combines an exact count of exceptional sign tuples with a sparse finite-type

van der Corput bound for the oscillatory sums that appear; the edge case is handled by the trivial probability-measure bound. Instantiating the general almost-sure root-count machinery with these exponents (, ) yields deviation bounds summable in , and Borel–Cantelli delivers the full almost-sure limit— the almost-sure strengthening of Yakir's theorem, with roots counted with algebraic multiplicity in the closed disk, exactly as the problem asks.

Verification #

The pinned statement is immutable and universe-polymorphic; the acceptance gate permits only

import Erdos522Statement

, so the 133 proof modules are amalgamated (dependency-closed, topologically ordered, freshly sectioned) into one candidate file with nosorry

,admit

, new axioms, unsafe code, or forbidden metaprogramming. The gate re-elaborates the candidate against the pinned statement and audits axioms:

PASS: kernel-checked proof of the pinned Erdős 522 statement
axioms: [propext, Classical.choice, Quot.sound]

The download bundle contains the pinned statement project, the exact accepted

Candidate.lean

with its SHA-256-logged transcript, the amalgamation script, and the one-command checker (check_answer/check.sh verified_math/F-132_erdos-522-final/Candidate.lean

).## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 15. Erdős Problem #538Erdős Problem www.erdosproblems.com/538## ›Question

Let and suppose that is such that, for any , there are at most solutions to where is prime and . Give the best possible upper bound for

(Erdős Problem #538 — number theory — https://www.erdosproblems.com/538)

›Result #

The best possible bound is Θ_r(log N / log log N): Erdős's 1973 upper bound Σ_{a∈A} 1/a ≪ r·log N/log log N is optimal up to constants, witnessed by an explicit construction achieving that order — answering how large the reciprocal sum can be.

-- upper bound (universal): for every admissible A ⊆ {1,…,N},
--   log(log(N+1)) · Σ_{a∈A} 1/a ≤ 2r(1 + log N²)
-- lower bound (construction): for every N there is an admissible A with
--   log(N+1) ≤ 4 + 8192·(1 + log₂ log₂ N) · Σ_{a∈A} 1/a
-- together: Σ_{a∈A} 1/a = Θ_r(log N / log log N)
theorem erdos538_matching_order : Erdos538.MatchingOrder

›Report #

The problem and why it is hard #

For fixed , let satisfy the condition that every integer has at most representations

with prime and . The problem asks for the best possible upper bound on

A weighted incidence count gives the natural upper scale

The difficulty was proving that this scale is attainable. On a squarefree layer with exactly prime factors, write an integer as its -element set of prime divisors. The representation condition becomes a hypergraph condition: among the facets of every -set, at most may be selected. For , this is the daisy problem.

The elementary upper density is of order , but previously available general constructions were only around , up to logarithmic improvements. That missing factor of became exactly the missing factor of in the number-theoretic problem.

Where the standard approaches stalled #

Many natural constructions impose a checksum, coloring, or deletion code on each -set. They generally need two independent rare events:

• enough distinct colors to identify a deleted coordinate; and
• a checksum or syndrome condition to limit the number of accepted facets.

Each event costs roughly , leaving density . We verified this obstruction for the balanced rainbow-checksum template and saw the same scale recur in extensive experiments with rooted trees, tries, permutations, cyclic orders, tournaments, Pfaffians, ordered words, and singular matrices.

The broader issue is that generic hypergraph coloring treats forbidden triples as unrelated local constraints. It throws away the decisive geometry: all facets of one parent live in a single two-dimensional relation space. The successful construction had to control that entire parent space at once rather than attach an almost-independent syndrome to each child.

Arithmetic detours did not remove the obstruction. Prime reciprocal weights, the product cutoff , and nonsquarefree exponent cores all reduce back to the same daisy coefficient under weighted blow-ups or square-kernel decomposition. The real bottleneck was genuinely combinatorial.

The key insight: safe isotropic kernels #

Fix and an odd finite field , with comparable to . Label each ground vertex by

For a -set , define

Call

favorable when:- is surjective, so its relation space is a line;

• a generator of that line has full support;
• ; and
• the coefficient vector is nonzero.

A favorable child is called

safe if no outside vertex extends it to a parent whose two-dimensional relation space is totally isotropic for the same diagonal bilinear form.### Why the family has cap two

Consider a -set . A selected facet missing contributes an isotropic relation in the parent relation space whose unique zero coordinate is . Full support makes the relation lines from distinct selected facets distinct.

One selected facet already forces the parent relation space to be two-dimensional. If three facets were selected, that plane would contain three distinct isotropic lines. For a symmetric bilinear form in odd characteristic, three such lines force the form to vanish identically: if are two isotropic generators and is a third distinct isotropic line, then and

so as well. The whole plane is therefore totally isotropic, contradicting the safety condition. Thus every parent contains at most two selected facets.

Why the density is

The favorable samples admit an injective finite-field parameterization. Its exact cardinality is

When , this gives favorable density at least .

After a favorable child is fixed, one outside label makes its parent relation plane totally isotropic only when two equations hold: one nonzero linear equation and one uniquely determined scalar equation. The dangerous fraction is exactly

On a ground set with , a union bound leaves at least half of the outside assignments safe. Averaging over all global labelings therefore yields a cap-two family of density at least .

Bertrand's postulate supplies an odd prime . Taking and gives, for every , a cap-two -uniform family of density at least

This closes the daisy density gap at the order needed here.

Returning to the integers #

A weighted coloring argument transfers the palette to any exact squarefree -prime-factor layer. First, color prime supports into colors so that at least half of the reciprocal weight is rainbow. Then average over permutations of the colors so that at least a fraction of that rainbow weight lands in the safe-kernel palette.

The resulting integer subfamily retains at least

of the reciprocal mass of that layer and satisfies the original representation cap two. Repeated colors do not create a hidden multiplicity problem: in a non-rainbow parent, at most the two occurrences in the unique repeated pair can yield rainbow facets.

Exact prime-factor layers can be united without adding their representation caps, because all representations of a fixed come from one -layer. Truncating at , and using the squarefree harmonic-mass and first-moment estimates, gives an admissible cap-two family satisfying the explicit inequality

Thus

Together with the incidence upper bound, the best possible order for every fixed is

Verification #

The entire argument was formalized in Lean 4 with Mathlib. The final theorem uses the exact audited definitions of:

• a finite set ;
• every solution pair to ;
• the universal cap over every ; and
• the rational reciprocal mass .

The verified chain includes the finite-field counts, injectivity of the favorable parameterization, the exact danger fraction, the parent cap, weighted relabeling, multiplicity-aware pattern transfer, integer-layer retention, harmonic truncation, and the final upper/lower theorem. The complete Lean project builds successfully, and the copied final artifact

verified_math/F-080_final-matching-order/Proof.lean

kernel-checks withoutsorry

,admit

, or additional axioms.## ›Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly down Mathlib.

• 16. Erdős Problem #584Erdős Problem www.erdosproblems.com/584## ›Question

Let be a graph with vertices and edges. Are there subgraphs such that has edges and every two edges in are contained in a cycle of length at most , and furthermore if two edges share a vertex they are on a cycle of length , and has edges and every two edges in are contained in a cycle of length at most .

(Erdős Problem #584 — graph theory, cycles — https://www.erdosproblems.com/584)

›Result #

The statement as written is false: there are graphs with δn² edges (with δ allowed to shrink) containing no cycle of length ≤ 8 at all, so no subgraph with ≫ δ²n² edges can have every two edges on a short cycle. The fixed-density version of the problem remains open.

/-- The literal second bullet of Erdős Problem 584 is false. -/
theorem not_secondBullet : ¬ SecondBullet.{0}

/-- Therefore the conjunction asked in the literal problem statement is false. -/
theorem not_problemStatement : ¬ ProblemStatement.{0}

›Report #

The problem, as printed #

Let be a graph with vertices and edges. The problem asserts the existence of two subgraphs: with edges in which every two edges lie on a cycle of length at most 6 (and edges sharing a vertex lie on a 4-cycle), and with edges in which every two edges lie on a cycle of length at most 8.

Read literally, nothing constrains : it is simply and may shrink with . That reading matters, because the statement is

falsein that generality — and the falsity is provable in Lean.## The counterexample mechanism

Take graphs with

no cycle of length at most 8 at all. In such a graph, any subgraph in which every two distinct edges must lie on a short internal cycle can contain at most one edge (there are no short cycles to lie on). So the bullet fails as soon as a short-cycle-free graph has

source & further reading

starfleetmath.com — original article