Proposed Solutions (19)

Many problems listed as “open” carry informal or partial answers already available online; we tried extremely hard to avoid working on any such problems (but most likely failed in certain cases). If there are attribution mistakes, please let us know.

Full Solutions (13)

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

  Let $a,b,c\geq 1$ be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form $a^kb^lc^m$ ($k,l,m\geq 0$), 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 $a,b,c>1$, consider the numbers

  $$a^i b^j c^k \qquad (i,j,k\ge 0).$$

  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 $[N,CN]$. 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 $B_0+r d$ carries a large positive baseline $B_0$. 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

  $$i+j+k=D.$$

  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 $c^n$ primitive subset sums on one level with distinct residues modulo $c^n$ 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

  $$1<a<c<b.$$

  Choose

  $$H=\operatorname{edgeDigitDepth}(c),\qquad u=H+2,$$

  and then choose $v>0$ so that

  $$2b a^v\le c^v.$$

  Define two coprime homogeneous translation weights

  $$A=a^{u+v},\qquad B=b^u c^v.$$

  Copies of one AP digit family are translated by the weights

  $$A^{M-r}B^r.$$

  The choice $u>H+1$ places different copies in disjoint bands of the $b$-exponent. Multiplying every term by $abc$ makes every AP term strict-interior. All copies then lie on one exact exponent degree.

  A bounded homogeneous-radix lemma proves that coefficient sums

  $$\sum_{r=0}^{M} s_r A^{M-r}B^r, \qquad 0\le s_r<4AB,$$

  contain a full interval of width at least $2AB^{M+1}$. Replacing each coefficient by the corresponding AP digit set realizes this as an interval on a lattice of step $abc\,d$, where $d$ 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

  $$C_{\mathrm{corr}}c^D.$$

  Apply this with modulus $abc\,d$, on the same exact degree as the AP-radix construction. Face-supported corrections are disjoint from the strict-interior AP terms. Moreover,

  $$\frac{B}{c^{u+v}}=\left(\frac bc\right)^u>1,$$

  so exponential domination gives

  $$C_{\mathrm{corr}}c^D=o(B^M).$$

  Thus the correction spread is eventually smaller than the radix width. Residue gluing converts the lattice interval into an ordinary consecutive interval $[L_M,U_M]$ satisfying

  $$abc\,B^M\le U_M-L_M, \qquad L_M\le K B^{M+1}$$

  for a fixed constant $K$.

  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 $s$, fix a $b$-exponent just beyond every AP band. Among the remaining $a,c$-exponents, choose the last point of the geometric grid

  $$b^s a^{R-k}c^k$$

  below a target of size $c^{vM}$. Because consecutive grid points differ by the fixed factor $c/a$, the selected monomial lies in a controlled multiplicative window. After restoring the common factors, this produces at least $M-O(1)$ distinct optional monomials $z$ satisfying

  $$z\le X, \qquad aX\le cz, \qquad X=abc\,B^M.$$

  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

  $$\Omega(MB^M),$$

  while the lower endpoint remains $O(B^M)$. Hence the ratio of the upper endpoint to the lower endpoint grows linearly with $M$. For every requested $R>1$, and beyond every requested lower threshold, this constructs a primitively represented interval

  $$[N,RN].$$

  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 $N_0$ and $C>1$ such that any represented interval $[N,CN]$ with $N\ge N_0$ implies d-completeness.

  Applying the arbitrary-width construction with $R=C$ proves d-completeness for ordered bases $1<a<c<b$. 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 $a,b,c\ge1$; that universal formulation is false at $(1,1,1)$. The project records this separately and proves the intended nondegenerate $a,b,c>1$ 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $A\subseteq \mathbb{N}$ be such that$$\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty$$and$$\sum_{n\in A} \{ \theta n\}=\infty$$for every $\theta\in (0,1)$, where $\{x\}$ is the distance of $x$ from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of $A$.

  (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 of A in every dyadic shell (x,2x] tends to infinity, and that

  $$\sum_{n\in A}\|\theta n\|=\infty$$

  for 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 of A.

  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

  $$\sum_{n\in A}\|\theta n\|,$$

  two sufficiently close phases cannot both satisfy that bound. Indeed, if their difference is δ, look at a dyadic shell at scale about 1/(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:

  $$\sum_k |\widehat\Phi(k)|^2 =N\sum_j|\Phi(j)|^2.$$

  Weighting the Nth 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

  $$\frac1N\sum_{n<N}|\widehat\mu(n)|^2\longrightarrow0.$$

  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 or admit, 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $F_1=F_2=1$ and $F_{n+1}=F_n+F_{n-1}$ be the Fibonacci sequence. Let $n_1<n_2<\cdots$ be an infinite sequence with $n_{k+1}/n_k \geq c>1$. Must$$\sum_k\frac{1}{F_{n_k}}$$be 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 $F_1=F_2=1$, $F_{n+1}=F_n+F_{n-1}$, and let $n_1<n_2<\cdots$ be any infinite index sequence with a uniform ratio gap $n_{k+1}/n_k\ge c$ for some $c>1$. Erdős asked whether

  $$\sum_k \frac{1}{F_{n_k}}$$

  must be irrational.

  For fast-growing gaps this is classical territory: when $c\ge 2$ the series is covered by known irrationality criteria for lacunary series (Badea, 1993). The genuinely open range was $1<c<2$, 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 $c=2$, the tail $\sum_{j>k}1/F_{n_j}$ can be comparable to $1/F_{n_k}$, so the classical "the fractional part cannot be that small" argument does not close.
  • Working modulo one denominator loses the structure. Individual $F_n$ 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 $1/F_n=\sqrt5\sum_j(-1)^{nj}\varphi^{-(2j+1)n}$ converts the series into a Lambert-type series in $\varphi^{-1}$, 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 $\mathbb Z[\varphi]$. 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 $0$ and $1$ — 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 $c>1$.

  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 real tsum of (Nat.fib (n k))⁻¹ and HasRatioGap asserts one real $c>1$ with $c\le n_{k+1}/n_k$ for all $k$. 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $S(N)$ count the number of distinct sums of the form $\sum_{n\in A}\frac{1}{n}$ for $A\subseteq \{1,\ldots,N\}$. Estimate $S(N)$.

  (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

  $$S(N)=\left|\left\{\sum_{n\in A}\frac1n:A\subseteq\{1,\dots,N\}\right\}\right|.$$

  There are $2^N$ subsets, but many can have the same sum. Estimating $S(N)$ therefore means understanding an enormous family of exact rational collisions. Neither extreme is informative: counting subsets ignores collisions, while putting every fraction over $\operatorname{lcm}(1,\dots,N)$ gives a support interval far too large to reveal the true scale.

  The answer contains not just $N/\log N$, but a product of iterated logarithms. That makes the problem especially unforgiving: a fixed inefficiency at each renewal step becomes a factor such as $c^{\log^*N}$, 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 $\log^*N$ 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 (Erdős's own starting point)

  This reformulation is not ours: it is the classical opening move of this subject, used by Bleicher and Erdős themselves in their 1975 lower-bound paper [BlEr75], as Xiao_Hu pointed out on the erdosproblems forum. Full credit to them; we state it here because everything after builds on it. Two subsets give the same value precisely when their symmetric difference yields

  $$\sum_{n=1}^N \frac{\varepsilon_n}{n}=0, \qquad \varepsilon_n\in\{-1,0,1\}.$$

  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

  $$|U(N)|\log 2\le \log S(N).$$

  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 $\lfloor N/p\rfloor$.

  The key technical device is an exact discrete benchmark

  $$B_k(n)=n(n+1)P_k(\log_2 n) \bigl(\log_2(n+1)-\log_2n\bigr).$$

  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 $m$ is good and $p$ is prime with $p>m\operatorname{lcm}(1,\dots,m)$, then $mp$ is good.

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

  A crude but explicit estimate

  $$m\operatorname{lcm}(1,\dots,m)<65536^m$$

  is sufficient. It permits all $m$ up to a constant multiple of $\log N$.

  4. Preserve coefficient one

  The lower recurrence closes in the form

  $$A(N)\ge \frac{N}{\log N} \sum_{2\le v<\log_{65536^2}N}\frac{A(v)}{v(v+1)},$$

  with coefficient exactly one. Two effects make this possible:

  • since $m\ge2$, the strict gain $\log(N/m)<\log N$ 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 $k$, the proof evaluates a power tail $x^{1-\varepsilon_k}$ with

  $$\varepsilon_k=2^{-2k-10}.$$

  The iterated-log product loses at most a factor $(1-\varepsilon_k)^k$. These losses are summable, and their total leaves a uniform coefficient at least $1/2$, 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

  $$P(x)= \begin{cases} 1,&x\le e^3,\\ (\log x)P(\log x),&x>e^3. \end{cases}$$

  Then there are constants $c,C>0$ such that, for all sufficiently large $N$,

  $$c\frac{N}{\log N}P(\log_2N) \le \log S(N)\le C\frac{N}{\log N}P(\log_2N).$$

  Equivalently,

  $$S(N)=\exp\!\left(\Theta\!\left( \frac{N}{\log N} \prod_{j\ge3\,\text{until stopped}}\log_jN \right)\right).$$

  Verification

  The complete argument was formalized in Lean 4 + Mathlib. The final theorem is ResearchPNT.exists_two_sided_full_product_estimate in verified_math/F-038_two-sided-full-product-estimate/lean/ResearchPNT/FinalEstimate.lean.

  Verification is deliberately strict:

  • the checker rejects sorry, admit, custom axioms, opaque, and unsafe 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, and Quot.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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  What is the size of the largest $A\subseteq \{1,\ldots,N\}$ such that all sums $\sum_{n\in S}\frac{1}{n}$ are distinct for $S\subseteq A$?

  (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 $R(N)$ be the largest size of a set $A\subseteq\{1,\ldots,N\}$ for which all sums

  $$\sum_{n\in S}\frac1n,\qquad S\subseteq A,$$

  are distinct. The answer is

  $$R(N)=\Theta\!\left(\frac{N}{\log N} \prod_{j=3}^{k(N)}\log_j N\right),$$

  where $k(N)$ is the last iterated logarithm above a fixed absolute threshold.

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

  $$\sum_{a\in A}\frac{\varepsilon_a}{a}=0, \qquad \varepsilon_a\in\{-1,0,1\},$$

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

  There is a second, analytic difficulty. Each useful recursion replaces $N$ by a quantity on the scale of $\log N$, so iterating it generates the factors $\log_3N,\log_4N,\ldots$. A proof at any fixed number of iterations is not enough: the number of relevant iterations tends to infinity, albeit as slowly as $\log^*N$. 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 $\log_3N\log_4N$, but loses a factor such as $1/2$ 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 $S(N)$ be the number of all reciprocal subset-sum values from $\{1,\ldots,N\}$, and put $H(N)=\log S(N)$. Since every valid set of size $R(N)$ creates $2^{R(N)}$ values,

  $$R(N)\log 2\le H(N).$$

  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

  $$(\mathcal D_T f)=\sum_{t=2}^{T} \frac{f(t)}{(t+1)\log t},$$

  with a common adaptive endpoint $T\asymp\log N$.

  2. Replace the recurrences by one positive Neumann model

  After normalization by $\log N/N$, 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

  $$M_A(N)=1+\mathcal D^{A}_{\nu(N)}M_A,$$

  where $A$ is a fixed terminal threshold and $\nu(N)\asymp\log N$.

  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:

  $$\left| \frac1{(t+1)\log t} -\bigl(\log\log(t+1)-\log\log t\bigr) \right| \le \frac1{t(t+1)}.$$

  Consequently, every truncated operator mass differs from its exact $\log\log$ difference by at most $1/A$. 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 $r$, only a fraction on the order of $2^{-r}$ 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 $B\ge4$, then

  $$2^d\log^{[j+d]}x\le \log^{[j]}x.$$

  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 $B$, every possible leaf belongs to one fixed finite range. The model is bounded on that range by a fixed constant $K$. Positivity then bounds the whole unexpanded remainder by $K$ 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 $B$. Hence their sum is bounded by the deepest product.

  Combining both sides gives

  $$M_A(N)\asymp \prod_{j=3}^{k(N)}\log_jN,$$

  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 $R(N)$;
  • 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 $N$, 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  For $r\geq 2$ let $h(r)$ be the maximal finite $k$ such that there exists a basis $A\subseteq \mathbb{N}$ of order $r$ (so every large integer is the sum of at most $r$ integers from $A$) and exact order $k$ (so every large integer is the sum of exactly $k$ integers from $A$). Find the value of$$\lim_r \frac{h(r)}{r^2}.$$

  (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, let h(r) be the largest exact order of an asymptotic basis of variable order at most r. The problem asks for the limit of h(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 moderate-torsion route was sharper, but formalization exposed two genuine obstructions in the natural argument.

  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 and 4x. Their unavoidable endpoint loads are 1 and 3, not the balanced bound 2 needed by the generic counting argument. Reorienting the progression does not fix this. Pure deficiency arithmetic remains short by exactly one far-fibre term, and treating the progression quotient as an immediate rank-one certificate is unsafe because its lift can retain two independent directions.

  These failures identified the real bottleneck: the proof needed exact endpoint geometry, not a broader inverse theorem.

  The route that worked

  The proof first transfers the infinite problem to a finite cyclic removal statement. A dyadic high-power argument finds a scale with doubling below 9/4. Dense alternatives, bounded quotient alternatives, and rank-one alternatives are then handled separately. The rank-one endgame is encoded by an exact two-generator lattice diagram; its L-shape area inequality gives

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

  which is the geometric source of the coefficient 1/3.

  The central structural step rectifies a cyclic set into a graph

  T ⊂ ℤ × ZMod N
  

  supported between two occupied integer fibres, 0 and l. Quotienting by the displacement between these endpoints produces a finite endpoint quotient B. Let F be the Kneser stabilizer of B+B, let C=B/F, and let

  D = (C+C) \ C
  

  be the genuinely new sum classes.

  The proof then exhausts the endpoint possibilities:

  • |D|=0 gives the desired progression-plus-subgroup certificate directly;
  • |D|=1 is excluded by a sharp two-piece projection inequality;
  • |D|≥3 in the nonvertical branch is excluded by representation selection or a two-class/three-sum-class quotient;
  • a vertical stabilizer forces the double-set saturation defect to be no larger than the original-set defect, contradicting full primitivity;
  • the remaining |D|=2 nonvertical case is resolved by a complete classification of three-point critical sumsets.

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

  1. a load-two selector exists;
  2. a subgroup quotient has two classes for the set and three for its double;
  3. 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 each r≥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:

  1. validates a SHA-256 manifest of all 191 research source files;
  2. builds the complete final dependency graph (8729 build jobs);
  3. checks an independently duplicated, nonvacuous statement of the problem;
  4. rejects sorry, admit, and project-declared axioms throughout the research tree;
  5. runs #print axioms on the final theorem.

  The only reported dependencies are Lean’s standard propext, Classical.choice, and Quot.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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $t_k(n)$ denote the least $m$ such that$$n\mid m(m+1)(m+2)\cdots (m+k-1).$$Is it true that$$\sum_{n\leq x}t_2(n)\ll \frac{x^2}{(\log x)^c}$$for some $c>0$?Is it true that, for $k\geq 2$,$$\sum_{n\leq x}t_{k+1}(n) =o\left(\sum_{n\leq x}t_k(n)\right)?$$

  (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 $k,n$, let $t_k(n)$ be the least positive integer $m$ such that

  $$n\mid m(m+1)\cdots(m+k-1).$$

  Erdős Problem 394 asks two average-order questions. Does some $c>0$ satisfy

  $$\sum_{n\le x}t_2(n)\ll \frac{x^2}{(\log x)^c}?$$

  And, for every fixed $k\ge2$, is

  $$\sum_{n\le x}t_{k+1}(n) =o\!\left(\sum_{n\le x}t_k(n)\right)?$$

  The difficulty is not merely that $t_k(n)$ is irregular. Its large values are structurally unavoidable. If $p\ge k$ is prime, then

  $$t_k(p)=p+1-k;$$

  in particular, $t_2(p)=p-1$. Thus no uniform pointwise saving can prove either assertion. Even the elementary monotonicity $t_{k+1}(n)\le t_k(n)$ 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 $c=1/2048$, and the adjacent sums satisfy the requested little-o relation for every fixed $k\ge2$.

  Why the natural attacks stalled

  The failed approaches exposed four distinct traps.

  • Pointwise estimates attack the wrong phenomenon. Prime inputs keep $t_k(n)$ nearly as large as $n$. 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 $t_{k+1}$-sum small by sieving medium prime factors, but comparison with $t_k$ also requires a denominator lower bound that preserves a stronger Euler factor.
  • Crude Euler estimates destroy the adjacent-length gap. The saving between $k$ and $k+1$ 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-$x$ asymptotic. An early hierarchy at cutoffs $16^{j^D}$ 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 $K$, a cutoff $X$, and an interval of medium primes $P=(z,y]$. For each $n\le X$, extract the squarefree product $q\mid n$ of the primes from $P$ which divide $n$. Integers divisible by some $p^2$, with $p\in P$, 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

  $$S_{K+1}(X)=\sum_{n\le X}t_{K+1}(n),$$

  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 $q$, attach a prime $\ell$ larger than every medium prime and consider $n=q\ell$. Most unit residue classes of $\ell\pmod q$ 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 $t_K(q\ell)$.

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

  $$(q,\ell)\longmapsto q\ell$$

  injective. No denominator mass is counted twice.

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

  $$S_K(X)=\sum_{n\le X}t_K(n)$$

  with an enhancement factor

  $$\prod_{p\in P}\left(1+\frac1{Kp}\right).$$

  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

  $$M=(K+1)(2K+1),$$

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

  $$(A/E)^M\le B^{M+1}.$$

  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

  $$X_N=16^N, \qquad h=\lfloor\log_2N\rfloor,$$

  and choose the lower and upper medium-prime scales using the exponents $h^2$ and $\lfloor N/h^4\rfloor$. 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 $K\ge2$, the formal proof establishes that, eventually in $N$, every natural cutoff satisfying

  $$16^N\le X\le16^{N+1}$$

  obeys

  $$\boxed{ \lfloor\log_2N\rfloor\,S_{K+1}(X) \le 3S_K(X). }$$

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

  For a large real $x$, take $X=\lfloor x\rfloor_+$ and $N=\lfloor\log_{16}X\rfloor$. Exact natural-logarithm inequalities place $X$ in the required interval. Since $\lfloor\log_2N\rfloor\to\infty$, for every $\varepsilon>0$ it eventually exceeds $3/\varepsilon$. The boxed estimate then gives

  $$S_{K+1}(X)\le\varepsilon S_K(X),$$

  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 over Finset.Icc 1 ⌊x⌋₊;
  • the conclusions use Mathlib's IsBigO atTop and IsLittleO atTop;
  • the second assertion quantifies over every fixed natural $k\ge2$.

  The final archive contains 106 Lean source files. Its verifier scans every source for sorry, admit, and added axiom 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  How large must $y=y(\epsilon,n)$ be such that the number of integers in $(x,x+y)$ with a divisor in $(n,2n)$ is at most $\epsilon y$?

  (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 $y=y(\epsilon,n)$ must be before the integers in $(x,x+y)$ having a divisor in $(n,2n)$ occupy at most an $\epsilon$-fraction of the interval.

  The natural uniform reading is adversarial in the translate: the estimate must hold for every $x$, 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 $n$ contains $n-1$ qualifying integers. Thus no answer of order $o(n)$ can work for fixed $0<\epsilon<1$. The real question is whether one can prove a matching $O_\epsilon(n)$ upper bound uniformly in $x$.

  Where the earlier routes stalled

  The first exact approach used periodicity. For fixed $n$, divisibility by some $d\in(n,2n)$ is periodic, so the problem has a precise period-density criterion. This led to a complete fixed-$n$ dichotomy: an eventual threshold exists exactly when $\epsilon$ 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 $n$.

  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 $m=dk$.

  The key breakthrough: finite-prime scores

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

  $$U(m)=\#\{p\in S:p\mid m\}.$$

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

  $$W(m)=U(m)+\#\{p\in S:p^2\mid m\}.$$

  The decisive pointwise inequality is

  $$U(d)+U(k)\le W(dk).$$

  If a selected prime divides both factors, its second occurrence is exactly what the $p^2$-term records. This turns the factorization $m=dk$, with $n<d<2n$, into a usable local trichotomy.

  Let

  $$\mu=\sum_{p\in S}\frac1p, \qquad Q=\prod_{p\in S}p^2.$$

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

  $$\sum_{m<Q}(U(m)-\mu)^2\le Q\mu.$$

  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 $m$, choose a divisor $d\in(n,2n)$ and write $m=dk$. Then at least one of the following holds:

  1. $U(d)\le 3\mu/4$;
  2. $U(k)\le 3\mu/4$;
  3. $W(m)\ge 3\mu/2$.

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

  The three classes can be counted uniformly in the translate. Once $Q\le n$ and $y\ge n(Q+2)$, their weighted contributions are at most

  • $64y$ for low-score divisors;
  • $32y$ for low-score quotients;
  • $56y$ for high two-level score.

  Thus

  $$\#\{m\in(x,x+y):m\text{ has a divisor in }(n,2n)\}\,\mu\le 152y$$

  for every $x$.

  The sum of the reciprocals of the primes diverges, so for each $\epsilon>0$ one may choose a finite $S_\epsilon$ with $\mu>152/\epsilon$. The preceding inequality then gives the desired $\epsilon y$ bound at the linear scale $n(Q_\epsilon+2)$.

  Why the order is sharp

  The factorial dense block supplies the matching lower obstruction. At length $y=n$, one explicit translate has exactly $n-1$ bad integers. For every fixed $0<\epsilon<1$, this violates the requested estimate for all sufficiently large $n$.

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

  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 $\epsilon y$,” 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 $0<\epsilon<1$.

  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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$. Let$$B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}.$$If $B=\{b_1<b_2<\cdots\}$ then is it true that$$\lim \frac{1}{x}\sum_{b_i<x}(b_{i+1}-b_i)^2$$exists (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 $A\subseteq\mathbb N$ be extremely sparse,

  $$|A\cap[1,x]|=o(\sqrt x),$$

  and let $B=\{b_1<b_2<\cdots\}$ be the positive integers divisible by no member of $A$. Erdős asked whether

  $$\frac1x\sum_{b_i<x}(b_{i+1}-b_i)^2$$

  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 $A$ 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 $\sum r/a_r<\infty$, where $a_r$ is the forbidden enumeration. That misses the sharp regime allowed by $a_r/r^2\to\infty$, 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 $a_0<a_1<\cdots$. Thinness gives three crucial consequences:

  1. eventually $(r+1)^2\le a_r$;
  2. $\sum_r 1/a_r<\infty$;
  3. the rank-pair kernel

  $$\sum_{r,s}\frac{\min(r+1,s+1)}{a_ra_s}$$

  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

  $$n\equiv1\pmod Q,$$

  where $Q=Y!$ for a suitably chosen roughness threshold $Y$. This coordinate change has two decisive effects.

  • Any forbidden modulus sharing a prime factor with $Q$ is automatically unable to divide such an $n$.
  • 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 $Q^{-1}$, while the bad-pair estimate below gains exactly $Q^{-2}$; 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

  $$|S|\le G\sum_{r\in\mathrm{labels}(S)}\frac1{a_r}+|\mathrm{labels}(S)|$$

  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 $p>Y$ forces their difference to be divisible by $Qp$, 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 $G$ receives enough pairs to pay for $G^2$ with one fixed constant.

  Coprimality is the key structural move. If positions labelled by $a_r,a_s$ are written as

  $$n=a_ru, \qquad m=a_sv,$$

  then coprimality of $n,m$ makes the quotient vector $(u,v)$ primitive. Repeated scalar dilations—the obstruction that defeated the naive pair count—disappear.

  Primitive-ray capacity and global charging

  For fixed labels $(r,s)$, 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

  $$a_ra_s\,\mathrm{capacity} \le 4XC\min(r+1,s+1)+2a_ra_s.$$

  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

  $$\sum G^2 \le K\left( X\sum_{(r,s)\in J} \frac{\min(r+1,s+1)}{a_ra_s} + |J| \right).$$

  The first term is uniformly small for high ranks by kernel summability. The endpoint term $|J|$ is at most the square of the forbidden counting function, hence is $o(X)$. 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 $\varepsilon>0$, some $H$ makes the normalized contribution of all gaps at least $H$ eventually smaller than $\varepsilon$.

  From uniform tails to an actual limit

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

  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-$H$ 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 in check_answer/README.md, including the original inclusive counting function, the Nat.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 or admit 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $r\geq 2$ and suppose that $A\subseteq\{1,\ldots,N\}$ is such that, for any $m$, there are at most $r$ solutions to $m=pa$ where $p$ is prime and $a\in A$. Give the best possible upper bound for$$\sum_{n\in A}\frac{1}{n}.$$

  (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 $r\ge 2$, let $A\subseteq\{1,\dots,N\}$ satisfy the condition that every integer $m$ has at most $r$ representations

  $$m=pa,$$

  with $p$ prime and $a\in A$. The problem asks for the best possible upper bound on

  $$S(A)=\sum_{a\in A}\frac1a.$$

  A weighted incidence count gives the natural upper scale

  $$S(A)=O_r\!\left(\frac{\log N}{\log\log N}\right).$$

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

  The elementary upper density is of order $1/k$, but previously available general constructions were only around $1/k^2$, up to logarithmic improvements. That missing factor of $k$ became exactly the missing factor of $\log\log N$ in the number-theoretic problem.

  Where the standard approaches stalled

  Many natural constructions impose a checksum, coloring, or deletion code on each $k$-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 $1/k$, leaving density $1/k^2$. 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 $a\le N$, 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 $k=d+1$ and an odd finite field $K=\mathbb F_q$, with $q$ comparable to $k$. Label each ground vertex $v$ by

  $$(\phi_v,c_v)\in K^d\times K.$$

  For a $k$-set $S$, define

  $$\Psi_S(\lambda)=\sum_{v\in S}\lambda_v\phi_v, \qquad B_S(\lambda,\mu)=\sum_{v\in S}c_v\lambda_v\mu_v.$$

  Call $S$ favorable when:

  • $\Psi_S$ is surjective, so its relation space is a line;
  • a generator $\lambda$ of that line has full support;
  • $B_S(\lambda,\lambda)=0$; and
  • the coefficient vector $(c_v)_{v\in S}$ 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 $(k+1)$-set $T$. A selected facet missing $x$ contributes an isotropic relation in the parent relation space whose unique zero coordinate is $x$. 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 $u,v$ are two isotropic generators and $w=au+bv$ is a third distinct isotropic line, then $a,b\ne0$ and

  $$0=B(w,w)=2abB(u,v),$$

  so $B(u,v)=0$ 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 $\Omega(1/k)$

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

  $$(q-1)^d \left(\prod_{i=0}^{d-1}(q^d-q^i)\right) (q^d-1).$$

  When $q\ge 2k$, this gives favorable density at least $1/(8q)$.

  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

  $$\frac1{q^2}.$$

  On a ground set with $2(m-k)\le q^2$, 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 $1/(16q)$.

  Bertrand's postulate supplies an odd prime $2k<p\le4k$. Taking $q=p$ and $m=2k^2$ gives, for every $k\ge2$, a cap-two $k$-uniform family of density at least

  $$\frac1{64k}.$$

  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 $k$-prime-factor layer. First, color prime supports into $2k^2$ colors so that at least half of the reciprocal weight is rainbow. Then average over permutations of the colors so that at least a $1/(64k)$ fraction of that rainbow weight lands in the safe-kernel palette.

  The resulting integer subfamily retains at least

  $$\frac1{128k}$$

  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 $m$ come from one $\Omega$-layer. Truncating at $K\asymp\log\log N$, and using the squarefree harmonic-mass and first-moment estimates, gives an admissible cap-two family satisfying the explicit inequality

  $$\log(N+1) \le 4+8192\bigl(1+\lfloor\log_2\lfloor\log_2N\rfloor\rfloor\bigr)S(A).$$

  Thus

  $$S(A)=\Omega\!\left(\frac{\log N}{\log\log N}\right).$$

  Together with the incidence upper bound, the best possible order for every fixed $r\ge2$ is

  $$\boxed{\Theta_r\!\left(\frac{\log N}{\log\log N}\right)}.$$

  Verification

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

  • a finite set $A\subseteq[1,N]$;
  • every solution pair $(p,a)$ to $m=pa$;
  • the universal cap over every $m$; and
  • the rational reciprocal mass $\sum_{a\in A}1/a$.

  The verified chain includes the finite-field counts, injectivity of the favorable parameterization, the exact $1/q^2$ 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 without sorry, 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Consider the triangular lattice with minimal distance between two points $1$. Denote by $f(t)$ the number of distances from any points $\leq t$. For example $f(1)=6$, $f(\sqrt{3})=12$, and $f(3)=18$.Let $x_1,\ldots,x_n\in \mathbb{R}^2$ be such that $d(x_i,x_j)\geq 1$ for all $i\neq j$. Is it true that, provided $n$ is sufficiently large depending on $t$, the number of distances $d(x_i,x_j)\leq t$ is less than or equal to $f(t)$ with equality perhaps only for the triangular lattice?In particular, is it true that the number of distances $\leq \sqrt{3}-\epsilon$ is less than $1$?

  (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 gives

  n = 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 are

  oblique 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, exceeding 18·38=684 and 9·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 than 6n 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 or native_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, rejects sorry, admit, and native_decide, and prints an axiom audit. The only reported axioms are the standard Mathlib axioms propext, Classical.choice, and Quot.sound.

  Prior work

  Przemek Chojecki's April 2026 note, "Reconstructing a corrupted Erdos problem on small distances" (posted on the problem's erdosproblems thread), diagnosed the corrupted printed text first and worked out two repaired variants: a threshold-count repair with true breakpoint sqrt(2), and the historically intended shell-multiplicity reading via Vesztergombi's 1987 theorem. Full credit to him for the first public diagnosis and those repairs. Our submission treats different readings of the extremality question (closed and strict thresholds, both comparison conventions, at general radius), proved in 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Let $k\geq 2$ and let $g_k(n)$ be the largest possible size of $A\subseteq \{1,\ldots,n\}$ such that every $m$ has $<k$ solutions to $m=a_1a_2$ with $a_1<a_2\in A$.Is it true that$$g_3(n)=\frac{\log\log n}{\log n}n+(c+o(1))\frac{n}{\log n}$$for some constant $c$?

  (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 to Mertens.M + variationalLimit, hence the requested constant exists. The two-gate upper reduction is closed by smoothRemainderGate_proved and the new extractedTailGate_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 and Erdos796.erdos796_statement reports exactly [propext, Classical.choice, Quot.sound], with no sorryAx. 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw

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

  Call a set of distinct integers $1<n_1<\cdots<n_k$ with associated congruence classes $a_i\pmod{n_i}$ 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 $F(x)$ count the number of minimal distinct covering systems with all moduli in $[1,x]$. Estimate $F(x)$.

  (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 $a_i\pmod{n_i}$ with pairwise distinct moduli $1<n_1<\cdots<n_k$ whose classes cover every integer; it is minimal if no proper subset covers. Let $F(x)$ count the minimal distinct covering systems with all moduli in $[1,x]$. Erdős asked to estimate $F(x)$ — 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, $\log\log F(x)\sim\log x$, equivalently $F(x)=\exp\!\big(x^{1+o(1)}\big)$.

  Why matching bounds are the whole game

  The upper bound at this scale is straightforward — there are at most $\prod_{n\le x}(n+1)=\exp(O(x\log x))$ 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 $p_0,\dots,p_{m-1}$ and a closing prime $p_m$. For each late coordinate $i$, set $r_i=\lfloor\log_2(i+1)\rfloor+1$ and a window $h_i=2048\,r_i$, and assign every nonzero residue of $p_i$ injectively to a cross-pair support $\{u,v\}$ with $u<h_i\le v<i$; 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 $2^{E_m}$ systems with $E_m\ge\binom{m-B}{2}$, while every support uses at most three primes of controlled size, so all moduli fit under an explicit cutoff polynomial in $m$ (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 $>1$, 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.

  Download & Verify w/ CursorDownload & Verify w/ Claude CodeDownload & Verify w/ Codex

  ↓ Download full solution raw