Star Fleet Math
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 Problemwww.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
Solving Erdős Problem 123
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 by
Apply 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 downloading Mathlib.
- 2) Erdős Problem #129Erdős Problemwww.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
Erdős Problem 129: a formally verified disproof
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)
makes every60t
-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 graphs defines different minimum-order split and balanced parameters, with polynomial rather than square-root-exponential behaviour.
- Their A variant of the classical Ramsey problem studies
(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 downloading Mathlib.
- An initial counting proof used Lean's
- 3) Erdős Problem #130Erdős Problemwww.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
An Infinite-Chromatic Integer-Distance Graph in General Position
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 downloading Mathlib.
- 4) Erdős Problem #254Erdős Problemwww.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
A Formal Proof of Erdős Problem #254
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 of distinct 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 downloading Mathlib.
- 5) Erdős Problem #267Erdős Problemwww.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
Irrationality of Lacunary Fibonacci Reciprocal Sums
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 across all selected 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 long equal / mismatch / equal comparison 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 downloading Mathlib.
- 6) Erdős Problem #320Erdős Problemwww.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
Erdős Problem 320: the number of distinct unit-fraction subset sums
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 is
ResearchPNT.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 downloading Mathlib.
- 7) Erdős Problem #321Erdős Problemwww.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
Solving Erdős Problem 321
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 , then
This 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 downloading Mathlib.
- 8) Erdős Problem #336Erdős Problemwww.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
Erdős Problem 336: why the constant is one third
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 a uniform 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 gives3|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 letD = (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 rectifiable
3n-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 downloading Mathlib.
- 9) Erdős Problem #394Erdős Problemwww.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
A Proof of Erdős Problem 394
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 satisfying
obeys
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 least positive 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 downloading Mathlib.
- 10) Erdős Problem #415Erdős Problemwww.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 Ordering Patterns of Consecutive Totients: All Three Questions
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 cannot be 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 downloading Mathlib.
- 11) Erdős Problem #450Erdős Problemwww.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
A Linear-Scale Solution to Erdős Problem 450
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 downloading Mathlib.
- 12) Erdős Problem #489Erdős Problemwww.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
A Positive Answer to Erdős Problem 489
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 yields
The 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 revision
fabf563a7c95a166b8d7b6efca11c8b4dc9d911f
. 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 # Build completed successfully (8618 jobs).
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 # Build completed successfully (8608 jobs).
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 downloading Mathlib.
- 13) Erdős Problem #521Erdős Problemwww.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 Almost-Sure Law for Real Roots of Random ±1 Polynomials Fails
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 look plausible: , so deviations of order at any fixed degree are rare. The failure mechanism is not one bad degree but infinitely 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 downloading Mathlib.
- 14) Erdős Problem #522Erdős Problemwww.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
Almost-Sure Root Concentration for Random ±1 Polynomials
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 statement in 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 are summable 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 the closed disk boundary count at 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 downloading Mathlib.
- 15) Erdős Problem #538Erdős Problemwww.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
Erdős Problem #538: the matching-order bound
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 downloading Mathlib.
- 16) Erdős Problem #584Erdős Problemwww.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
Erdős Problem #584: The Literal Statement Is False
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 false in 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 for the proposed implicit constant — i.e., as soon as high-girth graphs can have super-linear edge counts, which they famously can.
A self-contained high-girth construction
Standard sources invoke algebraic constructions (generalized hexagons, graphs) for dense high-girth graphs. Formalizing those would drag in heavy finite-field machinery. The accepted proof instead uses a short maximal-graph argument, fully self-contained:
Given a target constant , set , , , . Among graphs on vertices with maximum degree and no cycle of length , pick one maximal under edge inclusion. Maximality forces any two low-degree vertices to be within distance (otherwise the connecting edge could be added, preserving both constraints). Fixing one low-degree vertex, all others lie in its radius- ball, which has at most vertices. Hence at least vertices have full degree ; handshaking gives , so — while the graph still has no cycle of length . The obstruction lemma then rules out every witness, refuting the second bullet and with it the conjunction:
theorem not_secondBullet : ¬ SecondBullet.{0} theorem not_problemStatement : ¬ ProblemStatement.{0}
What remains open — stated honestly
The historically intended problem plausibly carries a fixed-density qualifier (fixed , ), under which the question remains open and interesting. The supplied problem text does not include one, and the fidelity audit records this interpretation point explicitly rather than silently repairing the statement. What is proved here is exactly: the statement as printed, quantified over all densities, is false.
Verification
The final project is self-contained (definitions, obstruction, high-girth construction, negation) and passes the acceptance gate: pinned Mathlib fetch, full
lake build
(1,147 jobs), and rejection ofsorry
/admit
/user axioms, ending inPASS: Lean verified ¬SecondBullet and ¬ProblemStatement (sorry/admit/axiom-free).
The download bundle contains the faithful definitions, the complete proof project, and the line-by-line fidelity audit in
check_answer/README.md
.›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 downloading Mathlib.
- 17) Erdős Problem #638Erdős Problemwww.erdosproblems.com/638
›Question
Let be a family of finite graphs such that for every there is some such that if the edges of are coloured with colours then there is a monochromatic triangle.Is it true that for every infinite cardinal there is a graph of which every finite subgraph is in and if the edges of are coloured with many colours then there is a monochromatic triangle.
(Erdős Problem #638 — graph theory, ramsey theory — https://www.erdosproblems.com/638)
›Result
The answer is no, even for the substantive hereditary reading: there is a subgraph-closed family of finite graphs containing n-color triangle-Ramsey members for every finite n, yet admitting no graph whose finite subgraphs all lie in the family and which is triangle-Ramsey for infinitely many colors.
/-- The triangle-containing family meets every finite-color Ramsey hypothesis. -/ theorem triangleContainingFamily_finitelyTriangleRamseyRich : triangleContainingFamily.FinitelyTriangleRamseyRich /-- The literal assertion in problem.md is false, uniformly in the universe of infinite cardinals. -/ theorem erdos638_literal_answer_is_no.{u} : ¬ LiteralClaim.{u}
›Report
Erdős Problem #638: No — Even for the Hereditary Reading
The problem
Let be a family of finite graphs such that for every there is some that is -color triangle-Ramsey: every -coloring of 's edges contains a monochromatic triangle. Erdős asked: must there then be, for every infinite cardinal , a graph all of whose finite subgraphs lie in , such that every -coloring of 's edges contains a monochromatic triangle?
Two readings, both answered no
The literal reading. The printed text does not require to be closed under subgraphs. Under that reading the answer is no, by a formal counterexample family:
theorem erdos638_literal_answer_is_no.{u} : ¬ LiteralClaim.{u}
The independent referee accepted this theorem as genuine but ruled that the substantive question requires closed under taking ordinary (not merely induced) subgraphs — otherwise membership can be gerrymandered. That strengthened target was then also proved:
theorem erdos638_ordinaryHereditary_answer_is_no.{u} : HereditaryTarget.{u}
So the answer is no even when the isomorphism-closed family is required to be closed under ordinary finite subgraphs — the strongest natural version. Both statements are universe-polymorphic, so "every infinite cardinal" genuinely means every one.
The mathematical heart: sparse triangle-Ramsey graphs
The counterexample family needs finite graphs that are simultaneously (a) triangle-Ramsey for arbitrarily many colors and (b) globally sparse in a strong incidence sense, so that no infinite graph with all finite subgraphs in the family can stay Ramsey for infinitely many colors. The key constructive theorem: for every and every , there is a finite -color triangle-Ramsey graph whose edge/triangle incidence graph has ordinary girth greater than .
The construction formalizes Nešetřil–Rödl-style partite amalgamation with Hales–Jewett focusing:
- Finite multicolor triangle-Ramsey hosts exist (classical, formalized from Hales–Jewett).
- Bipartite partite focusing plus a strict Berge/incidence-girth induction produces Ramsey constituent systems of arbitrary incidence girth.
- Induced full graph-partite amalgamation with an edge-star encoding lifts the sparsity through each amalgamation round; a sheet-tag argument shows no new triangle ever crosses amalgamation sheets, so triangle structure stays exactly controlled.
- Distinguished labels biject with geometric triangles (a repeated triangle would force an incidence cycle of length , contradicting girth), and explicit isomorphisms transfer everything to a canonical
Fin
-labeled host.
A verified compactness/core/block reduction then converts these sparse Ramsey graphs into an isomorphism-closed, ordinary-hereditary family witnessing the negative answer.
Verification
Three independent gates pass: the sparse-triangle-Ramsey verifier, the hereditary-target verifier, and the final checker, which byte-compares the pinned statement files against immutable copies, scans all sources for
sorry
/admit
/native_decide
/local axioms, rebuilds the project, and audits the final theorems:axioms: [propext, Classical.choice, Quot.sound]
The download bundle contains the pinned statements, the F-027/F-028 proof projects, the reduction, and the fidelity audit documenting both readings and why the hereditary one is the substantive target.
›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 downloading Mathlib.
- 18) Erdős Problem #662Erdős Problemwww.erdosproblems.com/662
›Question
Consider the triangular lattice with minimal distance between two points . Denote by the number of distances from any points . For example , , and .Let be such that for all . Is it true that, provided is sufficiently large depending on , the number of distances is less than or equal to with equality perhaps only for the triangular lattice?In particular, is it true that the number of distances is less than ?
(Erdős Problem #662 — geometry, distances — https://www.erdosproblems.com/662)
›Result
The source-authenticated absolute-threshold/triangular-shell conjecture in Erdős Problem #662 is false: arbitrarily large one-separated planar sets exceed the triangular-lattice short-pair comparison under both closed and strict shell readings, with either the printed or corrected comparison values. In particular, a rational oblique lattice has 128 radius-6 offsets versus 126 triangular offsets, while another has 1078 offsets strictly below the genuine shell sqrt(300) versus corrected comparison 1074.
Closed shell witness: basis u=(1,0), v=(136/305,273/305). The identity 305m^2+305n^2+272mn = 136(m+n)^2+169m^2+169n^2 proves one-separation. It has 128 nonzero offsets of radius at most 6, versus 126 for the triangular lattice. A 365x365 patch has 16,786,618 directed short pairs, exceeding 126*133,225 by 268; separated replicas make the counterexamples arbitrarily large. Strict shell witness: basis u=(1,0), v=(276/565,493/565). At squared radius 300 it has 1078 strict offsets, versus triangular closed comparison 1074. A 4535x4535 patch exceeds the directed allowance by 3296 and the unordered allowance by 1648. The key Lean conclusions are `Research.triangular_shell_six_global_average_reading_false` and `Research.strict_shell_readings_false`.
›Report
Solving Erdős Problem #662
Why this problem was unusually difficult
Erdős Problem #662 asks whether the triangular lattice is extremal for the number of short distances in a large one-separated planar set. The natural comparison function counts triangular-lattice neighbours up to a threshold, and Erdős also proposed a stronger version at the lattice’s distance shells.
The main obstacle was not initially the geometry. The surviving statement is corrupt. Its sample values disagree with the natural cumulative lattice count, its final “less than 1” clause is impossible as printed, and the total/local normalization is unclear. This created two incompatible historical narratives:
- a threshold or shell extremal conjecture, which might be false;
- Vesztergombi’s theorem on the multiplicities of the two smallest distances, which is true and was published in 1987.
The maintained problem page consequently remained open and explicitly said that Erdős’s intent was unknown. A proof about any self-selected repair could be mathematically correct yet fail to answer the historical problem.
There was a second trap. The triangular lattice is the densest planar lattice packing, so it is tempting to expect it to maximize every fixed-radius neighbour count. Density is an asymptotic invariant; finite-shell coordination is not. A slightly less dense oblique lattice can place more lattice points inside one particular ball.
Where the earlier routes stalled
Several natural attacks clarified the ambiguity but did not resolve it.
- Square-grid blocks immediately defeat continuous-threshold average-degree readings between the first triangular shells. This is elementary, however, and does not address a conjecture restricted to genuine triangular-lattice shell radii.
- A 38-point packing gives one point 37 neighbours below radius 3, beating the corrected triangular local count 36. That disproves a local interpretation, but not the global average-degree version suggested by the “sufficiently large” qualifier.
- Formalizing Vesztergombi’s bound proved a beautiful theorem, but primary literature showed that it was already known and concerned the first two distinct distance values—not an absolute threshold.
- Even exact counterexamples to closed shell readings were not enough while the 1997 source remained unauthenticated. The possible interpretations gave opposite answers.
The recurring mistake was to treat statement repair and mathematical proof as one task. They had to be separated: first identify the historical subject externally, then cover the remaining damaged formula conventions rather than silently choosing one.
Breakthrough 1: recovering the primary passage
The missing source was found in the National Diet Library of Japan:
- NDL PID
10996926
; - DOI
10.11501/10996926
; - Mathematica Japonica 46(3), November 1997;
- P. Erdős, “Some of my favourite unsolved problems,” pp. 527–537.
The scan images require authorized library or personal transmission, but the NDL explicitly permits anonymous full-text snippets. Twenty-eight exact-phrase responses from the target content were captured. Their OCR windows overlap to reconstruct 943 consecutive characters with no gap and no conflicting character.
The primary text itself contains, in order:
- the triangular lattice and the function
f(t)
; - an arbitrary separated point sequence;
- the comparison between its number of short distances and
f(t)
; - the possible triangular-lattice equality case;
- the particular sub-
√3
question; and - Erdős’s stronger conjecture over the distance shells of the triangular lattice.
This settled the historical fork. The 1997 problem really is about absolute thresholds and triangular shells. It is not Vesztergombi’s separate 1987 multiplicity theorem. The OCR is poor on displayed formulas, so it does not justify inventing one missing factor; instead, all natural local/global and printed/corrected conventions were treated separately.
Breakthrough 2: finite-shell coordination beats density
For the corrected closed global reading, consider the rational oblique lattice with basis
u = (1,0), v = (136/305, 273/305).
It is one-separated because every integer offset satisfies
305m² + 305n² + 272mn = 136(m+n)² + 169m² + 169n² ≥ 305
when
(m,n) ≠ (0,0)
.At ordinary radius 6, exact enumeration gives:
triangular lattice: 126 nonzero offsets oblique lattice: 128 nonzero offsets.
A finite patch needs boundary correction; an infinite-lattice count alone is not a counterexample to an eventual finite statement. For a
365 × 365
patch, exact incidence counting givesn = 133,225 directed short pairs = 16,786,618 126n = 16,786,350 excess = 268.
Equivalently, there are 8,393,309 unordered short pairs, 134 more than
63n
. Far-separated translated copies preserve the excess and produce counterexamples above every requested cardinality. Thus “sufficiently large” cannot rescue the conjecture.Breakthrough 3: the strict shell version also fails
The quoted stronger conjecture uses strict inequalities at shell thresholds. A second rational lattice handles that version:
u = (1,0), v = (276/565, 493/565).
Its separation follows from
565m² + 565n² + 552mn = 276(m+n)² + 289m² + 289n² ≥ 565.
Squared radius 300 is a genuine triangular shell, since
300 = 10² + 10² + 10·10
. Exact counts areoblique offsets strictly below 300: 1078 triangular offsets through 300: 1074 triangular offsets strictly below: 1068.
For a
4535 × 4535
patch:n = 20,566,225 directed strict pairs = 22,088,128,946 1074n = 22,088,125,650 excess = 3,296 unordered excess = 1,648.
Again, separated replicas remove every cutoff. Under the printed comparison
f(3)=18
, the exact 38-point block already has 710 directed and 355 unordered pairs strictly below 3, exceeding18·38=684
and9·38=342
; its central degree 37 also defeats both the printed local bound 18 and corrected local bound 36.The answer to the shell-extremality question is therefore no, under closed or strict thresholds and under the printed or corrected comparison conventions. The natural repaired particular statement below
√3
is nevertheless true: angular separation gives fewer than 12 neighbours at every point and fewer than6n
unordered pairs.Verification
Every geometric and counting claim was formalized in Lean 4 with Mathlib.
- One-separation is derived symbolically from the displayed positive quadratic decompositions.
- Offset windows are proved complete, not sampled.
- Small finite censuses use kernel
decide
, never floating point ornative_decide
. - Huge patch counts are proved through dependent incidence types and injective endpoint maps; Lean does not enumerate billions of pairs.
- Replication theorems quantify over every requested cutoff.
- Independent Python scripts recompute all integer counts and boundary sums.
- The source gate hash-checks the NDL captures and semantically verifies all 28 OCR overlaps offline.
Running
check_answer/verify.sh
checks provenance hashes, reconstructs the primary OCR, runs both independent arithmetic audits, clean-builds 8570 Lean jobs, rejectssorry
,admit
, andnative_decide
, and prints an axiom audit. The only reported axioms are the standard Mathlib axiomspropext
,Classical.choice
, andQuot.sound
.›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 downloading Mathlib.
- 19) Erdős Problem #709Erdős Problemwww.erdosproblems.com/709
›Question
Let be minimal such that, for any of size , in any interval of consecutive integers there exist distinct such that .Obtain good bounds for , or even an asymptotic formula.
(Erdős Problem #709 — number theory — https://www.erdosproblems.com/709)
›Result
log₂n/(log₂(log₂n+1)+1) ≤ f(n) ≤ 7(⌊(n³)^(1/7)⌋+1) ≤ 14·n^(3/7) — first improvement of the Erdős–Surányi (1959) √n upper bound
›Report
Erdős Problem #709 — f(n) ≤ 14·n^(3/7) (accepted 2026-07-14)
Resubmission fixing the sole issue in the latest review. The referee explicitly confirmed that the canonical statement is faithful and successfully force-compiled the full three-sevenths proof with only standard Mathlib axioms; it rejected only because the exact script could not find lake when sandbox HOME differed from /root.
That exact portability defect is fixed in check_answer/verify.sh: it now prepends /root/.elan/bin and /root/.cargo/bin, sets fallback ELAN_HOME=/root/.elan, also checks caller-HOME locations, and emits a clear error if lake is absent. I tested the unchanged command under a deliberately hostile environment:
env -u ELAN_HOME HOME=/tmp/f030-hostile-home PATH=/usr/bin:/bin LEAN_NUM_THREADS=28 ./check_answer/verify.sh PASS: canonical Erdos 709 statement and all attached proofs compile without proof escapes
The log is attached as F-030/verification-hostile-home.txt.
Mathematical claim (already force-compiled by the latest referee): for the faithful natural least scale f(n), ScaleWorks n (7*(Nat.nthRoot 7 (n^3)+1)), (f(n):R) <= 14n^(3/7) for n>=1. Thus delta=1/14 below the historical 1/2 exponent. The explicit binary-log lower endpoint remains proved. The new #709 contribution is the Katz--Tao four-projection transfer through multiples 0,3,4,6, disjoint 7max(A) blocks, aggregation, and exact Hall.
Exact verifier required by the project: ./check_answer/verify.sh Current output: PASS: canonical Erdos 709 statement and all attached proofs compile without proof escapes
Referee
The agent claims a machine-verified exponent improvement for Erdős #709: the exact minimal natural scale satisfies log₂n/(log₂(log₂n+1)+1) ≤ f(n) ≤ 7(⌊(n³)^{1/7}⌋+1) ≤ 14n^{3/7}, beating the 1959 Erdős–Surányi √n upper bound via a self-contained Lean formalization of the Katz–Tao four-projection theorem. I audited the canonical statement quantifier-by-quantifier against problem.md (faithful), re-ran the exact claimed verifier in both normal and hostile-HOME environments (exit 0, PASS), and independently rebuilt everything in a clean workspace from sources only with pinned Mathlib fetched fresh from official servers (8043 jobs, success) with my own #print axioms showing only propext/Classical.choice/Quot.sound. This meets the acceptance bar explicitly set in the prior referee round (an exponent change, f(n) ≤ n^{1/2−δ}, here δ=1/14); note for human review that this is a strict improvement of the published upper-bound exponent on a still-open problem, not a matching-order asymptotic formula.
Independent verification (separate hardware)
Self-contained archive rebuilt on a fresh GCP box: portable verifier PASS (8,043 jobs), axiom audit exactly [propext, Classical.choice, Quot.sound].
Public bundles
https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-709/erdos-709-solution.zip (+ verify-cursor / verify-claude-code / verify-codex)
›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 downloading Mathlib.
- 20) Erdős Problem #769Erdős Problemwww.erdosproblems.com/769
›Question
Let be minimal such that if then the -dimensional unit cube can be decomposed into homothetic -dimensional cubes. Give good bounds for - in particular, is it true that ?
(Erdős Problem #769 — number theory, geometry — https://www.erdosproblems.com/769)
›Result
c(n) ≫ n^n is FALSE: c(n) = o(n^n) along odd dimensions (explicit threshold n·2^n·⌈49n/100⌉^n + 2)
›Report
Erdős Problem #769 — negative resolution (accepted 2026-07-14)
Unconditional negative solution to Erdős Problem 769: for every odd n>=201, every k >= n2^nceil(49n/100)^n+2 is an exact cubical tiling count, and this threshold is o(n^n). Hence c(n)/n^n tends to zero along odd dimensions and c(n) >> n^n is false. The self-contained Lean theorem is Erdos769.erdos769_lower_bound_false : ¬ Erdos769LowerBound. Exact verification: cd verified_math/F-020_elementary-asymptotic-disproof/lean && /root/.elan/bin/lake update && /root/.elan/bin/lake exe cache get && LEAN_NUM_THREADS=28 /root/.elan/bin/lake build && cd ../../.. && check_answer/verify.sh --disproof verified_math/F-020_elementary-asymptotic-disproof/lean. Output: PASS: canonical Erdős 769 lower-bound proposition disproved by Lean with no sorry/admit/custom axioms (only propext, Classical.choice, Quot.sound).
Referee
The agent claims a negative resolution of Erdős 769: Lean proves ¬Erdos769LowerBound, because for odd n ≥ 201 every k ≥ n·2^n·⌈49n/100⌉^n + 2 = o(n^n) is an exact homothetic-cube tiling count of the unit n-cube, so c(n) ≫ n^n is false. I audited the canonical formal statement line-by-line against problem.md (axis-parallel positive homothets, half-open exact cover equivalent to the standard closed decomposition, IsCutoff pinning the true minimal c(n), A/B-rational rendering of ≫ — all faithful, with no vacuous-negation loophole since the disproof must and does construct genuine tilings and a genuine minimal cutoff via well-ordering), confirmed the spec/lakefile/toolchain are byte-identical to the checker's pinned copies, scanned all local sources for sorry/admit/axiom/native_decide/extern/unsafe (none), and re-ran the official verifier myself: PASS with only propext, Classical.choice, Quot.sound. To rule out tampered build artifacts I additionally copied the project, deleted all local build products, revalidated the Mathlib cache against the official origin, recompiled all 13 Research modules from source (all freshly Built, zero errors), and re-ran the gate on that clean copy: PASS again. The mathematical chain (regular-grid tilings, substitution increments m^n−1, gcd-one for the 49/100-truncated increments in odd dimensions, quantitative Bézout conductor mod 2^n−1, o(n^n) decay, negation bridge) is internally coherent, elementary, consistent with the ledger and with known bounds; the kernel certifies the rest.
Independent verification (separate hardware)
Fresh GCP box, source-only archive:
lake exe cache get && lake build
→ Build completed successfully (8,571 jobs);#print axioms Erdos769.erdos769_lower_bound_false
→ [propext, Classical.choice, Quot.sound]; escape-hatch grep clean.Public bundles
https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-769/erdos-769-solution.zip (+ verify-cursor / verify-claude-code / verify-codex variants)
›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 downloading Mathlib.
- 21) Erdős Problem #793Erdős Problemwww.erdosproblems.com/793
›Question
Let be the maximum possible size of a subset such that whenever with and . Is there a constant such that
(Erdős Problem #793 — number theory — https://www.erdosproblems.com/793)
›Result
F(n) = π(n) + (27/2 + o(1))·n^(2/3)/log²(n) — exact second-order asymptotic with constant 27/2 for the a∤bc extremal family problem
›Report
Erdős Problem #793 — F(n) = π(n) + (27/2+o(1))·n^(2/3)/log²n (accepted 2026-07-14)
Affirmative solution of Erdős Problem #793: for the exact condition allowing b=c, the extremal function satisfies F(n)=pi(n)+(27/2+o(1))*n^(2/3)/log(n)^2. The final Lean theorem is Erdos793.affirmative_target : erdos793 in verified_math/F-036_erdos793-affirmative/ExtremalAsymptotic.lean; its statement module is byte-for-byte identical to the pinned F-001 statement. The exact standalone verifier is the verifier: command in F-036's entry.md. It rebuilt PrimeNumberTheoremAnd.Consequences, rejected sorry/admit/axiom in every copied source, compiled the complete copied chain, and accepted the final file. Final output: 'Erdos793.affirmative_target' depends on axioms: [propext, Classical.choice, Quot.sound]. No sorryAx occurs; build.log records the run.
Referee
The agent claims an affirmative solution of Erdős #793: F(n) = π(n) + (27/2 + o(1))·n^(2/3)/log²n, backed by a sorry-free Lean 4 (Mathlib 4.21.0) proof whose final theorem 'Erdos793.affirmative_target : erdos793' I audited line-by-line against problem.md and found faithful (exact ground set {1,…,n}, the a∤bc condition with only a≠b and a≠c so b=c is allowed, true max-cardinality F(n), exact π(n), scale n^(2/3)/(log n)², and existence of C with an explicit ε(n)→0 in an eventual exact equality — no weakening). I re-ran the exact verifier command from entry.md myself (exit 0, sorry/admit/axiom gate clean, all 32 dependency modules recompiled, final axiom report exactly [propext, Classical.choice, Quot.sound] — no sorryAx, no ofReduceBool), and additionally performed my own clean-room rebuild of the entire 33-module chain from the audited sources in a fresh directory with the experiment's prebuilt oleans excluded from LEAN_PATH, which also passed with the identical clean axiom report, closing the stale-artifact hole in the original verifier. Supporting checks: all attached sources are byte-identical to the ledger and experiment copies; the pinned statement file is byte-identical across F-001, the experiment, and F-036; the external PrimeNumberTheoremAnd checkout and Mathlib sources match their pristine tarballs; the external package's four known sorried theorems (pn_asymptotic, lambda_pnt, mu_pnt, mu_pnt_alt) provably do not enter the closure since the kernel's axiom report is clean, and the chain only uses the fully-proved pi_alt. Residual trust base Colin should confirm in human review: the Mathlib/PNT tarballs against upstream GitHub hashes (no network access here) and the stock Lean 4.21.0 toolchain binary; an external lean4checker pass over the final environment would be a worthwhile belt-and-suspenders step before any announcement.
Independent verification
Canonical entry.md verifier reproduced end-to-end after a full rebuild of the required Research modules: all 31 F-036 chain modules re-elaborated from source, final gate compiled, in-file axiom audits print exactly [propext, Classical.choice, Quot.sound] for Erdos793.affirmative_target (also exists_extremal_family, tendsto_normalizedExtremal); chain escape-hatch grep clean.
Priority disclosure
An informal sketch of this asymptotic (with openly-discussed gaps, no formalization, no exact constant) was posted to the erdosproblems forum ~13h before our submission (Chojecki, 2026-07-13). Colin ruled this archive stands as the first complete machine-verified proof with the exact constant 27/2, with this disclosure attached.
Public bundles
https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-793/erdos-793-solution.zip (+ verify-cursor / verify-claude-code / verify-codex)
›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 downloading Mathlib.
- 22) Erdős Problem #796Erdős Problemwww.erdosproblems.com/796
›Question
Let and let be the largest possible size of such that every has solutions to with .Is it true thatfor some constant ?
(Erdős Problem #796 — number theory — https://www.erdosproblems.com/796)
›Result
(g₃(n) − n·loglog n/log n)/(n/log n) → M + variationalLimit — the second-order term of g₃ converges to an explicit constant (answers the open follow-up on the problem thread)
›Report
Erdős Problem #796 — exact second-order constant (accepted 2026-07-14)
Proved an affirmative answer to Erdős Problem 796 in Lean. The closed theorem
Erdos796.erdos796_statement : Erdos796.Statement
proves that the faithful normalized residual converges toMertens.M + variationalLimit
, hence the requested constant exists. The two-gate upper reduction is closed bysmoothRemainderGate_proved
and the newextractedTailGate_proved
; F-032 supplies the matching lower bound.Exact verifier command: cd /root/snapshot && check_answer/verify.sh workspace/experiments/experiment_4_upper_decomposition/lean Most recent output ends: Build completed successfully (8737 jobs). PASS: authored sources are placeholder-free and Lean accepts the project
Axiom audit for both
Erdos796.extractedTailGate_proved
andErdos796.erdos796_statement
reports exactly[propext, Classical.choice, Quot.sound]
, with nosorryAx
. Final verified record: F-054.Referee
The agent claims a Lean-verified affirmative answer to Erdős 796: a closed theorem erdos796_statement proving ∃c with (g₃(n) − n·loglog n/log n)/(n/log n) → c (c = Mertens.M + variationalLimit). I audited the formal statement line-by-line against problem.md (faithful, quantifier-for-quantifier, identical to the pre-registered canonical file), re-ran the verifier myself (PASS, 8737 jobs), independently re-ran #print axioms (only propext/Classical.choice/Quot.sound — no sorryAx and no ofReduceBool, so the native_decide lemmas and the sorried PrimeNumberTheoremAnd declarations are provably outside the final proof's dependency cone), and re-elaborated Basic.lean and CanonicalTail.lean live from source. The proof is closed, hypothesis-free, machine-checked, and answers exactly the posed problem.
Independent verification (separate hardware)
Full environment reconstruction on a fresh GCP box (project + pinned sorry-free PrimeNumberTheoremAnd fork):
lake build
clean, pinned verifier PASS,#print axioms Erdos796.erdos796_statement
→ [propext, Classical.choice, Quot.sound]. The workspace's incidental native_decide lemmas and upstream sorried PNT declarations are provably outside the dependency cone.Public bundles
https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-796/erdos-796-solution.zip (+ verify-cursor / verify-claude-code / verify-codex)
›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 downloading Mathlib.
- 23) Erdős Problem #959Erdős Problemwww.erdosproblems.com/959
›Question
Let be a set of size and let be the set of distinct distances determined by . Let be the number of times the distance is determined, and suppose the are ordered such thatEstimatewhere the maximum is taken over all of size .
(Erdős Problem #959 — geometry, distances — https://www.erdosproblems.com/959)
›Result
M(n) ≥ n^(1 + 1/(50000·log log n)) for all large n — superlinear lower bound on the top-two distance-multiplicity gap (previous best Ω(n log n))
›Report
Erdős Problem #959 — superlinear lower bound (accepted 2026-07-14)
Proved a fully formal explicit superlinear lower estimate for the faithful maximum-gap reformulation of Erdos Problem 959: with c=1/50000, for every sufficiently large n, (n : R)^(1 + c/log(log n)) <= M(n)=extremalGap(n). This resolves the explicit modern question whether M(n) >= n^(1+c/log log n); it does not claim a matching upper bound or exact asymptotic order. The proof constructs normalized replicated lattice disks indexed by subsets of primes 1 mod 4, suppresses every competitor by reduced-denominator support, places blocks and padding points generically, chooses replication adaptively for every n, and uses a formal PNT in arithmetic progressions for the asymptotics.
Exact local verifier command: check_answer/verify.sh Exact final output: PASS: faithful formal quantity and all current Lean proofs compile without placeholders The verifier also prints: 'chebyshev_asymptotic_pnt' depends on axioms: [propext, Classical.choice, Quot.sound], and rejects sorryAx. Final theorem: Erdos959.erdos959_superlinear_lower_bound in Research/FinalLowerBound.lean and verified_math/F-044_erdos959-superlinear-lower-bound/FinalLowerBound.lean.
Post-referee hardening
Two trivial native_decide certificates (both
Nat.totient 4 = 2
) were replaced with kerneldecide
after referee approval; the full pinned verifier re-ran PASS.Referee
The agent claims a fully formal Lean proof that Erdős #959's extremal top-two distance-multiplicity gap satisfies M(n) ≥ n^(1+1/(50000·log log n)) for all sufficiently large n — a superlinear lower bound resolving the modern lower-bound question (previous best was Ω(n log n)); it explicitly does not claim a matching upper bound or exact order. I audited the formal definitions line-by-line against problem.md (faithful: exact real squared distances, unordered pairs, correct gap semantics including ties, true maximum over all n-point sets), rebuilt the entire 8624-job Lean project from a cleared build cache and reproduced the verifier's PASS (exit 0), and ran my own #print axioms on the final theorem: clean except two native_decide certificates that reduce to Nat.totient 4 = 2, which I re-proved by kernel decide. The result is machine-verified, honestly scoped, and answers the explicit superlinear-gap question; note when reviewing that the exact asymptotic order of M(n) (versus the O(n^(4/3)) unit-distance ceiling) remains open and is not claimed.
Independent verification (separate hardware)
Fresh GCP box, correct snapshot layout (project + pinned PNT fork): full
lake build
PASS;#print axioms Erdos959.erdos959_superlinear_lower_bound
→ [propext, Classical.choice, Quot.sound]; word-boundary escape-hatch grep clean.Public bundles
https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-959/erdos-959-solution.zip (+ verify-cursor / verify-claude-code / verify-codex)
›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 downloading Mathlib.
- 24) Erdős Problem #1183Erdős Problemwww.erdosproblems.com/1183
›Question
Let be maximal such that in any -colouring of the subsets of there is always a monochromatic family of at least sets which is closed under taking unions and intersections. Estimate .Let be defined similarly, except that we only require the family be closed under taking unions. Estimate . In particular, is it true that for some as , and ?
(Erdős Problem #1183 — combinatorics, ramsey theory — https://www.erdosproblems.com/1183)
›Result
For every k and every n >= 2^(2^(2^(k+16))), F(n) >= n^k, while for n >= 121 one has F(n) <= n^(floor(sqrt(n))+1); hence F(n) is superpolynomial and subexponential. For every n, the lattice parameter satisfies (n+2)/2 <= f(n) <= n^2+n+1.
def quantitativeUnionThreshold (k : Nat) : Nat := 2 ^ (2 ^ (2 ^ (k + 16))) theorem unionRamsey_quantitative_lower : forall k n : Nat, quantitativeUnionThreshold k <= n -> n ^ k <= unionRamseyNumber n theorem unionRamsey_superpolynomial : Superpolynomial unionRamseyNumber theorem unionRamsey_subexponential : Subexponential unionRamseyNumber theorem latticeRamsey_estimate : forall n : Nat, (n + 2) / 2 <= latticeRamseyNumber n /\ latticeRamseyNumber n <= n + n * n + 1
›Report
Solving Erdős Problem #1183
The problem and why it is difficult
Given a red-blue colouring of every subset of an
n
-element set, letF(n)
be the largest size of a monochromatic family that is closed under unions. Letf(n)
be the analogous quantity when the family must be closed under both unions and intersections.A chain immediately gives a lower bound of about
n/2
, but a chain does not reveal the true scale of the problem. The central question was whether arbitrary colourings must contain union-closed families that are simultaneously superpolynomial inn
and subexponential in2^n
. These requirements pull in opposite directions: closure gives useful algebraic structure, but an adversarial colouring can destroy most familiar structured subfamilies.The difficulty is especially sharp for lower bounds. Producing one fixed-dimensional monochromatic Boolean cube is a finite Ramsey statement; producing
n^k
compatible sets for every fixedk
, in every sufficiently large dimension, requires a supersaturation mechanism and a way to make many local cubes coexist inside one closed family.Where the established approaches stalled
Several natural routes expose real structure but do not solve the arbitrary-colouring lower bound.
- Chains only give the classical linear lower bound.
- Rank colourings are too special. Howorka's restricted result concerns colourings determined by set size, whereas the problem quantifies over every colouring.
- Free tuples and VC dimension are powerful for upper bounds: complements convert free union generators into shattered sets, and a random-colouring argument suppresses high free rank. This yields subexponential upper bounds, but it does not force large monochromatic families.
- A recent preprint obtained a quasipolynomial upper bound for
F(n)
and anO(n log n)
upper bound forf(n)
, while explicitly leaving open whetherF(n)
is polynomial or superpolynomial. - A bare finite Hales--Jewett theorem supplies a monochromatic block cube of each fixed dimension, but its seed is only existential. By itself it gives no usable dependence between the target power and the ambient dimension.
Computational reconnaissance also ruled out tempting shortcuts. Products of chains did not amplify the lower bound in small exact cases; standard set-family compressions could increase the objective; and a lazy SAT search for the next small value thrashed without producing asymptotic structure.
The approach that worked
1. Turn one Ramsey cube into many same-shaped cubes
Fix a target exponent
k
and setd=k+2
. Begin with a dimensionN
in which every two-colouring contains a monochromaticd
-dimensional block cube.Now count all
N
-coordinate intervals inside2^[n]
. Each interval contains such a cube. Double-counting interval-cube incidences, followed by pigeonholing the ordered block-size vector and the common top, produces more thann^(s-1)
monochromatic cubes of one shape, whered≤s≤N
is their support size.This is the first key change of viewpoint: instead of asking one Ramsey theorem to produce a huge family directly, use it only as a local seed, then obtain abundance from the ambient Boolean lattice.
2. Colour-code the cubes into globally disjoint atoms
Many cubes are not automatically compatible: their blocks may overlap in arbitrary ways. A finite colour-coding argument labels every ground-set point by a block type and one of
2n
slots. Averaging shows that one labelling retains more thann^(d-2)
cubes while assigning each block to its own reserved label fibre.Those fibres are globally disjoint atoms. Each retained cube becomes a
d
-edge on the atom pool, and every subedge corresponds to a monochromatic face. Taking the downward closure of the edges and mapping an atom set to the corresponding block deletion gives a monochromatic union-closed family. Union of deletion sets becomes intersection of atom-index sets, exactly the operation preserved by downward closure.Thus the construction yields more than
n^(d-2) = n^k
monochromatic union-closed sets.
3. Make the Ramsey seed quantitative via Lubell mass
The qualitative proof still hid the seed dimension
N
. The decisive quantitative insight was to replace general Hales--Jewett bounds by a direct Boolean-cube theorem based on random maximal chains.For a family on at most
N
points, define recursivelyT(N,0) = 1, T(N,r+1) = 1 + sqrt(2 N T(N,r)).
Lubell mass is the expected number
Y
of family members met by a uniformly random maximal chain. The second factorial momentE[choose(Y,2)]
admits an exact decomposition over nonempty gapsS
: each term is the reciprocal-binomial weight ofS
multiplied by the Lubell mass of the paired lower-endpoint family associated with that gap.If no
(r+1)
-cube exists, none of those paired families contains anr
-cube. Induction bounds their masses, while convexity gives the matching lower boundL(L-1)/2 ≤ E[choose(Y,2)].
This proves that Lubell mass above
T(N,r)
forces an(r+1)
-cube. Iterating the recurrence givesT(N,r)^(2^r) ≤ (8N)^(2^r-1),
and hence
T(N,r)<N/2
wheneverN>16^(2^r)
.The two colour classes have Lubell masses summing to
N+1
, so one exceedsN/2
. Therefore an explicit double-exponential dimension suffices for the block-cube seed. Substitutingd = k+2, N = 2^(2^(k+4))
into the supersaturation construction and bounding both finite construction constants by
2^(4N²)
yields the fully explicit theoremn ≥ 2^(2^(2^(k+16))) ⇒ F(n) ≥ n^k.
This proves that
F(n)
is superpolynomial. Independently, the free-rank/VC-dimension argument gives the explicit upper boundF(n) ≤ n^(floor(sqrt(n))+1) for n≥121,
which is subexponential.
4. Give a direct estimate for the lattice parameter
A separate canonical encoding gives a concise all-
n
estimate forf(n)
. For a nonempty familyL
closed under union and intersection, letB
be its bottom element. For each coordinatei
, letG_i
be the intersection of all members containingi
, usingB
if there is no such member. ThenA = B ∪ ⋃_{i∈A} G_i for every A∈L.
Thus
L
is reconstructed injectively fromB
and the functioni↦G_i
. There are at most2^n (2^n)^n = 2^(n+n²)
such codes. An exact property-B union bound produces a colouring with no monochromatic lattice family of size
n²+n+2
. Together with the chain construction, this gives(n+2)/2 ≤ f(n) ≤ n²+n+1
for every natural
n
.Verification
The entire argument was formalised in Lean 4 with Mathlib. The canonical file contains faithful finite definitions of subsets, colourings, monochromaticity, union/intersection closure, both exact Ramsey maxima, and all four final theorems.
The verifier does more than grep for proof holes:
- it compiles the complete self-contained Lean source;
- it rejects custom
axiom
andconstant
declarations; - it rejects any target depending on
sorryAx
; - it audits
#print axioms
for every final theorem; - it permits only Mathlib's standard
propext
,Classical.choice
, andQuot.sound
dependencies.
The final command is
./check_answer/verify.sh final
and its final line is
PASS: Lean accepted all four faithful target theorems without proof holes or custom axioms
An independent referee reran the verifier, audited statement fidelity against the original problem, 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 downloading Mathlib.
- 25) Erdős Problem #1186Erdős Problemwww.erdosproblems.com/1186
›Question
Let be such that in any -colouring of there exist at least many monochromatic -term arithmetic progressions. Give reasonable bounds (or even an asymptotic formula) for .
(Erdős Problem #1186 — additive combinatorics, arithmetic progressions — https://www.erdosproblems.com/1186)
›Result
δ₃ = 117/2192 exactly: every 2-coloring of {1,…,n} contains at least (117/2192 + o(1))·n² monochromatic 3-term arithmetic progressions, and the known 548-bead coloring attains it — settling the Parrilo–Robertson–Saracino conjecture (2008) and the question Graham put a prize on in 1999. The matching lower bound is an exact rational sum-of-squares certificate verified by two independent exact-arithmetic checkers; its discrete-to-continuum reduction is hand-verified. Update (2026-07-13): the 548-cell census at the heart of the upper bound is now additionally kernel-checked in Lean itself (theorem Erdos1186Census.score_eq, axiom audit: [propext] only, no native_decide) — the first brick of the in-progress full formalization.
/-- A finite, division-free formulation of the two bounds on δ_k. -/ theorem erdos1186_explicit_bounds {k W : ℕ} (hk : 2 ≤ k) (hvdw : VanDerWaerdenProperty k W) : (∀ (n : ℕ) (c : ℕ → Bool), 4 * (W - 1) * ((W - 1) / (k - 1)).factorial ≤ n → ((W - 1) / (k - 1)).factorial.totient * (n * n) ≤ 16 * (W - 1) * ((W - 1) / (k - 1)).factorial * (W - k + 1) * (monochromaticAPs n k c).card) ∧ (∀ n : ℕ, ∃ c : ℕ → Bool, 2 ^ k * (k - 1) * (monochromaticAPs n k c).card ≤ n * n) -- plus the exact rational RLT/PSD certificate: delta_3 = 117/2192 -- (checker: check_answer/, exact integer arithmetic, two independent verifiers)
›Report
δ₃ = 117/2192: The Exact Minimum Density of Monochromatic 3-APs
The problem and its history
For a 2-coloring of , count the monochromatic 3-term arithmetic progressions (positive common difference, each progression once). Let be the liminf over of the minimum over colorings, normalized by . Erdős Problem #1186 asks for bounds — Graham attached prize money to the question in 1999.
Parrilo, Robertson and Saracino (2007–08) proved and conjectured the upper bound is exact, the extremal coloring being a specific twelve-block pattern. Later work (2023) verified optimality only within restricted classes (anti-symmetric colorings with at most 12 blocks). The full conjecture — every coloring, including arbitrarily rapid alternation — remained open.
This solve determines the constant exactly: , settling the PRS conjecture.
Why the lower bound is the hard direction
The upper bound is a construction: the 548-bead periodic word with run lengths achieves , verified by exact counting. The lower bound must defeat every coloring. SDP relaxations asymptote strictly below the target; block-structure assumptions (periodicity, bounded block count, anti-symmetry) exclude exactly the adversarial colorings that matter. The proof must be simultaneously exact (no floating point at the extremal value — the bound is attained) and assumption-free.
The final argument
Work with the continuum quadratic form over . The PRS three-role identity gives, for every coloring, with the omitted endpoint-parity term provably nonnegative. A fixed 548-cell macroscopic partition makes this uniform in the coloring — full lattice rectangles give products of cell color proportions, boundary polygons obey one-sided bounds, and the fixed partition contributes only — with no block-count, periodicity, or regularity assumption.
Let be the twelve-run candidate, with . Writing an arbitrary spin profile as a perturbation (complementing so the perturbation mass is at most ), exact expansion produces a first-variation field plus a signed quadratic kernel. The checker proves the field values are uniformly distributed on integer intervals cell-by-cell; a bathtub bound and conservative cell-rectangle classification reduce everything to a finite optimization and the certificate exhibits this quantity as an exact sum of PSD, nonnegative-matrix, , mass-slack, and linear nonnegative terms. Reflection splits the PSD check into two 274-dimensional sectors, each certified by integer factor matrices plus diagonally-dominant residuals — a proof of positive semidefiniteness that needs only integer arithmetic. Hence for every profile, and the matching lower bound follows.
What is machine-checked, and how
- The certificates (field distributions, row budgets, both PSD sectors, the candidate score) are verified by an exact Rust checker using checked integer arithmetic, and independently re-verified by an arbitrary-precision Python implementation sharing no code.
- The certificate schemas (Bell/SOS and RLT soundness: "any certificate of this shape implies the inequality") are sorry-free Lean theorems.
- The discrete-to-continuum reduction (the three-role identity and the partition bookkeeping) is a short, fully written-out double-counting argument — the same architecture as PRS's peer-reviewed paper, checked by hand.
This is a computer-assisted proof in the classical sense of the four-color theorem or Kepler: exact certificates, independent checkers, and a short human-checkable core. A full Lean-kernel formalization of the remaining reduction is in progress as a follow-up project.
Verification
The download bundle contains the exact 548-cell certificate, both independent checkers with their test fixtures, the Lean schema proofs, and the reduction write-up. One command rebuilds and re-verifies everything:
PASS: all 548 field distributions and RLT row budgets exact PASS: symmetric/antisymmetric PSD residual margins … PASS: continuum lower bound equals candidate; delta_3 = 117/2192
Formalization progress (2026-07-13)
The 548-cell census — the exact combinatorial count anchoring the upper bound — is now kernel-checked in Lean directly:
Erdos1186Census.score_eq
proves the extremal word's weighted monochromatic score is exactly 128232 (bitmask-encoded word, balanced-split evaluation, 2m19s in the kernel, axiom audit[propext]
only, nonative_decide
), andword_density_eq
closes the arithmetic to 117/2192. Both modules ship in the download bundle and build with the project. The remaining non-Lean steps (the 548×548 PSD certificate in-kernel and the discrete-to-continuum reduction) are an active formalization 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 downloading Mathlib.
- 26) Erdős Problem #1188Erdős Problemwww.erdosproblems.com/1188
›Question
Call a set of distinct integers with associated congruence classes a distinct covering system if every integer satisfies at least one of these congruences. A minimal distinct covering system is one such that no proper subset forms a covering system.Let count the number of minimal distinct covering systems with all moduli in . Estimate .
(Erdős Problem #1188 — number theory, covering systems — https://www.erdosproblems.com/1188)
›Result
The number F(x) of minimal covering systems with all moduli in [1,x] satisfies log log F(x) / log x → 1 — that is, F(x) = exp(x^{1+o(1)}). Erdős expected F(x) to grow 'very slowly'; it in fact grows nearly double-exponentially.
theorem erdos1188_loglog_ratio_tendsto_one : Tendsto (fun x : ℕ => Real.log (Real.log (coveringCount x : ℝ)) / Real.log (x : ℝ)) atTop (𝓝 1)
›Report
Counting Minimal Covering Systems: F(x) = exp(x^{1+o(1)})
The problem
A distinct covering system is a finite set of congruences with pairwise distinct moduli whose classes cover every integer; it is minimal if no proper subset covers. Let count the minimal distinct covering systems with all moduli in . Erdős asked to estimate — he reportedly expected slow growth.
The answer is nearly doubly exponential:
theorem erdos1188_loglog_ratio_tendsto_one : Tendsto (fun x => Real.log (Real.log (coveringCount x)) / Real.log x) atTop (𝓝 1)
that is, , equivalently .
Why matching bounds are the whole game
The upper bound at this scale is straightforward — there are at most ways to pick at most one residue per modulus, and being a covering system only cuts this down. The problem lives entirely in the lower bound: one must construct enormously many genuinely distinct, minimal covering systems with bounded moduli. An earlier squarefree construction here produced a much weaker lower scale, and the first submission was rejected by the independent referee precisely because the lower and upper estimates did not meet. The accepted proof closes that gap with a sparser construction.
The sparse no-axis construction
Classical covering systems lean on a "primorial axis" — congruences whose moduli are products of all small primes — which is rigid and wastes modulus budget. The construction removes it entirely.
Fix base CRT prime coordinates and a closing prime . For each late coordinate , set and a window , and assign every nonzero residue of injectively to a cross-pair support with ; an explicit prime estimate guarantees enough pairs. Every residue of the closing coordinate receives its own support (empty, singletons, then cross-pairs), with reserved singletons keeping each base spike private — this yields coverage and a private witness for every congruence, which is exactly minimality. CRT transport converts the abstract frame into a minimal distinct integer covering system.
Counting. At every late coordinate the range of the residue-to-support injection is a free choice, and the finished system determines every choice (the family map is injective). This gives at least systems with , while every support uses at most three primes of controlled size, so all moduli fit under an explicit cutoff polynomial in (up to log factors). Interpolating the parametric family at all cutoffs and comparing with the upper bound yields the limit statement.
Verification
The faithful counting object pins the exact convention: canonical residues, pairwise distinct moduli , coverage quantified over all integers, minimality as "no proper subfamily covers", systems counted as unordered sets. The final theorem builds sorry-free from a fresh directory with pinned toolchain and manifest, rejecting
sorry
/admit
/native_decide
(8,592 jobs; axioms[propext, Classical.choice, Quot.sound]
). A concrete 70-class witness below modulus 1000 is verified by an independent exact Rust checker (with negative tests), tying the abstract construction to a concrete covering system anyone can inspect.The download bundle contains the pinned definitions, the full proof chain, the witness and checker, and the one-command verifier.
›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 downloading Mathlib.
- 27) Erdős Problem #1189Erdős Problemwww.erdosproblems.com/1189
›Question
Call a set of distinct integers a covering set if there is a choice of for such that every integer satisfies at least one of these congruences. A set is an irreducible covering set if no proper subset is a covering set. How many irreducible covering sets of size are there?What is the minimum and maximum that can be?Determine or estimate , where the maximum ranges over all irreducible covering sets of size .Are there infinitely many such that the divisors of (which are ) form an irreducible covering set?
(Erdős Problem #1189 — number theory, covering systems — https://www.erdosproblems.com/1189)
›Result
Kernel-proved in Lean: the largest possible modulus of an irreducible covering set of size k is EXACTLY 3·2^{k−3} for every k ≥ 5 (sharpening Simpson's 1985 bound); the least possible maximum modulus is k^{1+o(1)}; the maximal reciprocal sum is Θ(log k); and there are infinitely many n whose nontrivial divisors form an irreducible covering set (the family 2^{p−1}p of Z.-W. Sun, formalized). The count of irreducible covering sets of size k, exp((4√τ/3 + o(1))·k^{3/2}/√(log k)), is proved modulo the published BBMST enumeration theorem, carried as an explicit named hypothesis in the Lean statement — every other step is kernel-checked.
/-- Exact answer to the maximum-largest-modulus question. -/ theorem maximum_largest_modulus_answer {k : ℕ} (hk : 5 ≤ k) : IsGreatest (LargestModulusValues k) (3 * 2 ^ (k - 3)) /-- Near-linear answer to the minimum-largest-modulus question. -/ theorem minimum_largest_modulus_answer : (∀ k m : ℕ, m ∈ LargestModulusValues k → k + 1 ≤ m) ∧ (∃ K₀ : ℕ, ∀ k ≥ K₀, ∃ S : Finset ℕ, Irreducible S ∧ S.card = k ∧ ∀ d ∈ S, d ≤ minimumConstant * k * (logScale k) ^ 6) -- plus reciprocal_sum_answer (Θ(log k)) and count_answer_reduction -- (the BBMST-conditional counting asymptotic), all in Research/FinalClaims.lean
›Report
Irreducible Covering Sets: Four Questions, Four Answers
The problem
Call a set of distinct integers a covering set if some choice of residues covers every integer, and irreducible if no proper subset is a covering set (even with entirely fresh residues — irredundancy of one displayed cover is not enough, and the formalization is careful to use the stronger notion). Erdős Problem #1189 asks: (1) how many irreducible covering sets of size are there? (2) what are the minimum and maximum possible values of ? (3) determine or estimate the maximal reciprocal sum ; (4) are there infinitely many whose nontrivial divisors form an irreducible covering set?
The answers
Writing for the count, for the max/min largest modulus, and for the maximal reciprocal sum:
- , where — proved modulo the published BBMST enumeration theorem, carried as explicit named hypotheses in the Lean statement (see below).
- exactly, for every — sharpening Simpson's 1985 bound to equality; and , with kernel-proved bounds eventually.
- : a harmonic upper bound and an explicit base-64 logarithmic construction.
- Yes: for every odd prime , the nontrivial divisors of form an irreducible covering set (an infinite family due to Z.-W. Sun, formalized here), so infinitely many such exist.
Exact gated small values: and , cross-checked by an exhaustive census through and an independent exact Rust checker.
The mathematics
Maximum modulus. The arithmetic Simpson argument is pushed to an exact extremal analysis: doubling chains force the largest modulus to at most , and an explicit chain construction attains it for every .
Minimum modulus. The near-linear upper bound comes from a mixed frame with regular seed prime-power digits and exact-cardinality seed pairs — enough congruence classes are packed under a nearly-linear modulus cutoff while preserving irreducibility via private witnesses (fresh-residue frame obstructions). The kernel theorem exhibits, for every large , an irreducible size- set with all moduli .
Reciprocal sum. Upper: harmonic comparison. Lower: an explicit construction pushing reciprocal mass through the frame.
The count, and exactly what is conditional. The Lean development machine-checks the entire reduction around the literature: finite-fiber and arbitrary-gap reductions, the upper injection, strong-frame conversion under fresh residues, and division by the residue multiplicity. The single external input is BBMST (arXiv:1904.04806, Theorem 1.1 with their Section 5/6 counting) — their enumeration of minimal systems at the dense sizes. It enters as two explicit named hypotheses (
BBMSTLowerDatum
,BBMSTUpperHypothesis
) in the final statement, so a reader can see precisely what is assumed and what is proved. Nothing else in any of the four answers is conditional. (The paper's all-size padding step repeats a modulus, so the reduction deliberately avoids it; the injectivity cost is in the log count.)Verification
The final wrappers expose all quantifiers for the four questions, with the count's external hypotheses retained visibly and
#print axioms
output recorded; everything else is sorry-free with standard axioms only. The download bundle contains the complete pinned Lean project (with build-and-audit instructions), the census checker with fixtures, and the reduction documents including the line-by-line BBMST audit.
Update 2026-07-13 — COUNT lower bound now UNCONDITIONAL in Lean (mission deliverable 1/3, accepted)
The dedicated formalization mission proved the LOWER half of the count asymptotic with no BBMST hypothesis:
BBMSTLower.explicitLowerDatum
constructs an explicit frame family (fiber bound 1) along dense sizes k_m, andBBMSTLower.eventually_log_irreducible_count_lower
gives(log 2 / 4096) * k * sqrt(k / log(k+1)) <= log |IrreducibleOfSize k|
i.e. the strong irreducible-modulus-set count is exp(Omega(k^(3/2)/sqrt(log k))) unconditionally.
Verification: independent rebuild on separate hardware (fresh GCP box, byte-identical pinned archive, sha256 12151af2…) —
lake build
clean, axioms exactly [propext, Classical.choice, Quot.sound], no sorry/admit/native_decide (grep-clean). Referee approved (R-78ffbd).Evidence bundle (public): https://pub-23f3a588e04a481196ed22d7e3a6f48d.r2.dev/verify/erdos-1189/erdos-1189-bbmst-lower-update.zip
Remaining for 100%% end-to-end: the UPPER half (deliverable 2), in progress.
›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 downloading Mathlib.
Untested (623)
- 1) Erdős Problem #1Erdős Problemwww.erdosproblems.com/1
›Question
If with is such that the subset sums are distinct for all then
(Erdős Problem #1 — prize: $500 — number theory, additive combinatorics — https://www.erdosproblems.com/1)
- 2) Erdős Problem #3Erdős Problemwww.erdosproblems.com/3
›Question
Erdős–Turán Conjecture on Arithmetic Progressions (Erdős Problem #3).
If has , then must contain arbitrarily long arithmetic progressions?
Prove (or disprove) this conjecture.
Equivalently, this is asking for good bounds on , the size of the largest subset of without a non-trivial -term arithmetic progression. For example, a bound like would be sufficient.
- 3) Erdős Problem #5Erdős Problemwww.erdosproblems.com/5
›Question
Let . Is there an infinite sequence of such that
(Erdős Problem #5 — number theory, primes — https://www.erdosproblems.com/5)
- 4) Erdős Problem #7Erdős Problemwww.erdosproblems.com/7
›Question
Is there a distinct covering system all of whose moduli are odd?
(Erdős Problem #7 — number theory, covering systems — https://www.erdosproblems.com/7)
- 5) Erdős Problem #9Erdős Problemwww.erdosproblems.com/9
›Question
Let be the set of all odd integers not of the form (where and is prime). Is the upper density of positive?
(Erdős Problem #9 — number theory, additive basis, primes — https://www.erdosproblems.com/9)
- 6) Erdős Problem #10Erdős Problemwww.erdosproblems.com/10
›Question
Is there some such that every large integer is the sum of a prime and at most powers of 2?
(Erdős Problem #10 — number theory, additive basis, primes — https://www.erdosproblems.com/10)
- 7) Erdős Problem #11Erdős Problemwww.erdosproblems.com/11
›Question
Is every large odd integer the sum of a squarefree number and a power of 2?
(Erdős Problem #11 — number theory, additive basis — https://www.erdosproblems.com/11)
- 8) Erdős Problem #12Erdős Problemwww.erdosproblems.com/12
›Question
Let be an infinite set such that there are no distinct such that and . Is there such an withDoes there exist some absolute constant such that there are always infinitely many withIs it true that
(Erdős Problem #12 — number theory — https://www.erdosproblems.com/12)
- 9) Erdős Problem #14Erdős Problemwww.erdosproblems.com/14
›Question
Let . Let be the set of integers which are representable in exactly one way as the sum of two elements from .Is it true that for all and large Is it possible that
(Erdős Problem #14 — number theory, sidon sets, additive combinatorics — https://www.erdosproblems.com/14)
- 10) Erdős Problem #15Erdős Problemwww.erdosproblems.com/15
›Question
Is it true thatconverges, where is the sequence of primes?
(Erdős Problem #15 — number theory, primes — https://www.erdosproblems.com/15)
- 11) Erdős Problem #17Erdős Problemwww.erdosproblems.com/17
›Question
Are there infinitely many primes such that every even number can be written as a difference of primes where ?
(Erdős Problem #17 — number theory, primes — https://www.erdosproblems.com/17)
- 12) Erdős Problem #18Erdős Problemwww.erdosproblems.com/18
›Question
We call practical if every integer is the sum of distinct divisors of . If is practical then let be such that many divisors always suffice.Are there infinitely many practical such thatIs it true that ? Or perhaps even ?
(Erdős Problem #18 — number theory, divisors, factorials — https://www.erdosproblems.com/18)
- 13) Erdős Problem #19Erdős Problemwww.erdosproblems.com/19
›Question
If is an edge-disjoint union of copies of then is ?
(Erdős Problem #19 — prize: $500 — graph theory, chromatic number — https://www.erdosproblems.com/19)
- 14) Erdős Problem #20Erdős Problemwww.erdosproblems.com/20
›Question
Let be minimal such that every family of -uniform sets with contains a -sunflower. Is it true thatfor some constant ?
(Erdős Problem #20 — prize: $1000 — combinatorics — https://www.erdosproblems.com/20)
- 15) Erdős Problem #23Erdős Problemwww.erdosproblems.com/23
›Question
Can every triangle-free graph on vertices be made bipartite by deleting at most edges?
(Erdős Problem #23 — graph theory — https://www.erdosproblems.com/23)
- 16) Erdős Problem #25Erdős Problemwww.erdosproblems.com/25
›Question
Let be an arbitrary sequence of integers, each with an associated residue class . Let be the set of integers such that for every either or . Must the logarithmic density of exist?
(Erdős Problem #25 — number theory — https://www.erdosproblems.com/25)
- 17) Erdős Problem #28Erdős Problemwww.erdosproblems.com/28
›Question
If is such that contains all but finitely many integers then .
(Erdős Problem #28 — prize: $500 — number theory, additive basis — https://www.erdosproblems.com/28)
- 18) Erdős Problem #30Erdős Problemwww.erdosproblems.com/30
›Question
Let be the maximum size of a Sidon set in . Is it true that, for every ,
(Erdős Problem #30 — prize: $1000 — number theory, sidon sets, additive combinatorics — https://www.erdosproblems.com/30)
- 19) Erdős Problem #32Erdős Problemwww.erdosproblems.com/32
›Question
Is there a set such thatand such that every large integer can be written as for some prime and ? Can the bound be achieved? Must such an satisfy
(Erdős Problem #32 — number theory, additive basis — https://www.erdosproblems.com/32)
- 20) Erdős Problem #33Erdős Problemwww.erdosproblems.com/33
›Question
Let be such that every large integer can be written as for some and . What is the smallest possible value ofIs
(Erdős Problem #33 — number theory, additive basis — https://www.erdosproblems.com/33)
- 21) Erdős Problem #36Erdős Problemwww.erdosproblems.com/36
›Question
Find the optimal constant such that the following holds. For all sufficiently large , if is a partition into two equal parts, so that , then there is some such that the number of solutions to with and is at least .
(Erdős Problem #36 — number theory, additive combinatorics — https://www.erdosproblems.com/36)
- 22) Erdős Problem #39Erdős Problemwww.erdosproblems.com/39
›Question
Is there an infinite Sidon set such thatfor all ?
(Erdős Problem #39 — prize: $500 — number theory, sidon sets, additive combinatorics — https://www.erdosproblems.com/39)
- 23) Erdős Problem #40Erdős Problemwww.erdosproblems.com/40
›Question
For what functions is it true thatimplies ?
(Erdős Problem #40 — prize: $500 — number theory, additive basis — https://www.erdosproblems.com/40)
- 24) Erdős Problem #41Erdős Problemwww.erdosproblems.com/41
›Question
Let be an infinite set such that the triple sums are all distinct for (aside from the trivial coincidences). Is it true that
(Erdős Problem #41 — prize: $500 — number theory, sidon sets, additive combinatorics — https://www.erdosproblems.com/41)
![[image →]](https://wexfordlocal.com/wp-content/uploads/2024/12/uisce-eireann.jpg?w=750){kind=link}
![[image →]](https://substackcdn.com/image/fetch/$s_!gWeJ!,w_1456,c_limit,f_auto,q_auto:good,fl_progressive:steep/https%3A%2F%2Fsubstack-post-media.s3.amazonaws.com%2Fpublic%2Fimages%2F361d81ef-7faf-4d8e-8028-5d5e03432a9a_2329x551.png){kind=link}
![[image →]](https://substackcdn.com/image/fetch/$s_!ZnxH!,w_1456,c_limit,f_auto,q_auto:good,fl_progressive:steep/https%3A%2F%2Fsubstack-post-media.s3.amazonaws.com%2Fpublic%2Fimages%2F10f7db70-0c90-4b49-acbf-615db3f3790b_1600x114.png){kind=link}
![[image →]](https://substackcdn.com/image/fetch/$s_!i8Y0!,w_1456,c_limit,f_auto,q_auto:good,fl_progressive:steep/https%3A%2F%2Fsubstack-post-media.s3.amazonaws.com%2Fpublic%2Fimages%2F520dfed9-3048-4ad4-92fe-29e8dff5abe7_1600x114.png){kind=link}