Star Fleet Math
Built by Colin Snyder · colin@colinsnyder.com
Advised by Mike Kim · proposed solutions ↓
Inspired by Ignis · previously built by Myself, Dhruv Agarwal, & Nitin Kesarwani at the New Turing Institute
These are “proposed solutions”, so if you take issue with any of them, please let us know.
Star Fleet is an AI system that solves the world's hardest open mathematics problems using Lean 4. It's a Mac desktop app that controls up to 20 custom agentic harnesses called “starships” in parallel, each running its own GPT-5.6 instance on a dedicated 60-vCPU server and working on a separate math problem. Everything is built from scratch in TypeScript & Bun.
Each starship has access to:
x86-64 CPU bursts of up to 2,000 vCPUs for search programs that shard into thousands of independent single-core jobs
H100 GPU bursts for massively parallel search programs
The world's largest corpus, afaik, of Lean 4 premises (theorems & lemmas), searchable in plain English via gemini-embeddings-2 & chroma vector db
A Firecrawl.dev index of arXiv.org research papers & GitHub repos
Claude Fable API wrapped in a proof-verifier agentic harness to review submitted answers + an iMessage API to ask Colin (the human) for an additional review after Fable's approval
Ton 618, a local long-term memory system where every verified Lean 4 premise (theorem or lemma) is woven into a dependency graph, so proofs compound
A dedicated 60-vCPU, 120 GiB memory sandbox preinstalled with SAT/SMT solvers (CaDiCaL, kissat, Z3), Google's CP-SAT, computer algebra systems (SageMath, PARI/GP, GAP, Macaulay2), and the full Rust, CUDA C++, and Lean 4 toolchains
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 Problemwww.erdosproblems.com/123›QuestionLet a,b,c≥1a,b,c\geq 1a,b,c≥1 be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form akblcma^kb^lc^makblcm (k,l,m≥0k,l,m\geq 0k,l,m≥0), none of which divide any other?(Erdős Problem #123 — prize: $250 — number theory — https://www.erdosproblems.com/123)›ResultFor 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›ReportSolving Erdős Problem 123
The problem and why it resisted the usual induction
For pairwise-coprime integers a,b,c>1a,b,c>1a,b,c>1, consider the numbers
aibjck(i,j,k≥0).
a^i b^j c^k \qquad (i,j,k\ge 0).
aibjck(i,j,k≥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][N,CN][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 B0+rdB_0+r dB0+rd carries a large positive baseline B0B_0B0. 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.
i+j+k=D.
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 cnc^ncn primitive subset sums on one level with distinct residues modulo cnc^ncn 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.
1<a<c<b.
1<a<c<b.
Choose
H=edgeDigitDepth(c),u=H+2,
H=\operatorname{edgeDigitDepth}(c),\qquad u=H+2,
H=edgeDigitDepth(c),u=H+2,
and then choose v>0v>0v>0 so that
2bav≤cv.
2b a^v\le c^v.
2bav≤cv.
Define two coprime homogeneous translation weights
A=au+v,B=bucv.
A=a^{u+v},\qquad B=b^u c^v.
A=au+v,B=bucv.
Copies of one AP digit family are translated by the weights
AM−rBr.
A^{M-r}B^r.
AM−rBr.
The choice u>H+1u>H+1u>H+1 places different copies in disjoint bands of the bbb-exponent. Multiplying every term by abcabcabc makes every AP term strict-interior. All copies then lie on one exact exponent degree.
A bounded homogeneous-radix lemma proves that coefficient sums
∑r=0MsrAM−rBr,0≤sr<4AB,
\sum_{r=0}^{M} s_r A^{M-r}B^r,
\qquad 0\le s_r<4AB,
r=0∑MsrAM−rBr,0≤sr<4AB,
contain a full interval of width at least 2ABM+12AB^{M+1}2ABM+1. Replacing each coefficient by the corresponding AP digit set realizes this as an interval on a lattice of step abc dabc\,dabcd, where ddd 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
CcorrcD.
C_{\mathrm{corr}}c^D.
CcorrcD.
Apply this with modulus abc dabc\,dabcd, on the same exact degree as the AP-radix construction. Face-supported corrections are disjoint from the strict-interior AP terms. Moreover,
Bcu+v=(bc)u>1,
\frac{B}{c^{u+v}}=\left(\frac bc\right)^u>1,
cu+vB=(cb)u>1,
so exponential domination gives
CcorrcD=o(BM).
C_{\mathrm{corr}}c^D=o(B^M).
CcorrcD=o(BM).
Thus the correction spread is eventually smaller than the radix width. Residue gluing converts the lattice interval into an ordinary consecutive interval [LM,UM][L_M,U_M][LM,UM] satisfying
abc BM≤UM−LM,LM≤KBM+1
abc\,B^M\le U_M-L_M,
\qquad
L_M\le K B^{M+1}
abcBM≤UM−LM,LM≤KBM+1
for a fixed constant KKK.
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 sss, fix a bbb-exponent just beyond every AP band. Among the remaining a,ca,ca,c-exponents, choose the last point of the geometric grid
bsaR−kck
b^s a^{R-k}c^k
bsaR−kck
below a target of size cvMc^{vM}cvM. Because consecutive grid points differ by the fixed factor c/ac/ac/a, the selected monomial lies in a controlled multiplicative window. After restoring the common factors, this produces at least M−O(1)M-O(1)M−O(1) distinct optional monomials zzz satisfying
z≤X,aX≤cz,X=abc BM.
z\le X,
\qquad
aX\le cz,
\qquad X=abc\,B^M.
z≤X,aX≤cz,X=abcBM.
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
Ω(MBM),
\Omega(MB^M),
Ω(MBM),
while the lower endpoint remains O(BM)O(B^M)O(BM). Hence the ratio of the upper endpoint to the lower endpoint grows linearly with MMM. For every requested R>1R>1R>1, and beyond every requested lower threshold, this constructs a primitively represented interval
[N,RN].
[N,RN].
[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 N0N_0N0 and C>1C>1C>1 such that any represented interval [N,CN][N,CN][N,CN] with N≥N0N\ge N_0N≥N0 implies d-completeness.
Applying the arbitrary-width construction with R=CR=CR=C proves d-completeness for ordered bases 1<a<c<b1<a<c<b1<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≥1a,b,c\ge1a,b,c≥1; that universal formulation is false at (1,1,1)(1,1,1)(1,1,1). The project records this separately and proves the intended nondegenerate a,b,c>1a,b,c>1a,b,c>1 conjecture used in the source literature and independent formal-conjecture encoding.›Download Full Solution & Verify with Your AIThe 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
Let a,b,c≥1a,b,c\geq 1a,b,c≥1 be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form akblcma^kb^lc^makblcm (k,l,m≥0k,l,m\geq 0k,l,m≥0), none of which divide any other?
(Erdős Problem #123 — prize: $250 — number theory — https://www.erdosproblems.com/123)
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.
Solving Erdős Problem 123
The problem and why it resisted the usual induction
For pairwise-coprime integers a,b,c>1a,b,c>1a,b,c>1, consider the numbers
The question asks whether every sufficiently large integer is a sum of distinct such numbers, with the additional requirement that no chosen summand divides another.
The divisibility condition is the real source of difficulty. Ordinary completeness arguments can use many terms from different scales, but terms from different scales tend to be comparable by divisibility. Conversely, a set chosen to be a divisibility antichain can be too arithmetically sparse to fill consecutive integers.
Earlier work had developed a powerful reduction scheme: choose a correction with the required residue modulo one base, subtract it, divide by that base, and induct. For particular triples this succeeds after a finite computer check. In general, however, it leaves a stubborn finite-seed problem: one must first represent every integer in a multiplicatively wide interval [N,CN][N,CN][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 B0+rdB_0+r dB0+rd carries a large positive baseline B0B_0B0. Replicating such progressions increases width and baseline at the same rate, so it need not produce the multiplicatively wide seed required by induction.
The important lesson was that large additive width is not enough. The lower endpoint has to remain under quantitative control.
The homogeneous-level coordinate system
The first structural simplification is to work on one homogeneous exponent level
For pairwise-coprime bases greater than one, divisibility of monomials is coordinatewise comparison of their exponents. Therefore two distinct monomials on the same level can never divide one another. Every subset of a homogeneous level is automatically primitive.
This turns the problem into an additive question about subset sums while making primitiveness essentially free—as long as all pieces of the construction can be placed on the same exact degree.
An edge-code construction supplies cnc^ncn primitive subset sums on one level with distinct residues modulo cnc^ncn and a bounded carry. Coloring by that carry and applying finite van der Waerden, itself obtained from Mathlib’s Hales–Jewett theorem, gives arbitrarily long exact arithmetic progressions of primitive homogeneous subset sums.
Turning one AP into a large lattice interval
Order the bases as
Choose
and then choose v>0v>0v>0 so that
Define two coprime homogeneous translation weights
Copies of one AP digit family are translated by the weights
The choice u>H+1u>H+1u>H+1 places different copies in disjoint bands of the bbb-exponent. Multiplying every term by abcabcabc makes every AP term strict-interior. All copies then lie on one exact exponent degree.
A bounded homogeneous-radix lemma proves that coefficient sums
contain a full interval of width at least 2ABM+12AB^{M+1}2ABM+1. Replacing each coefficient by the corresponding AP digit set realizes this as an interval on a lattice of step abc dabc\,dabcd, where ddd is the AP difference.
Filling residues with face corrections
The next ingredient constructs, on every sufficiently high exact degree, a primitive correction for each residue modulo any prescribed modulus. The corrections are supported on the three coordinate faces and, in the ordered case, have total size bounded by
Apply this with modulus abc dabc\,dabcd, on the same exact degree as the AP-radix construction. Face-supported corrections are disjoint from the strict-interior AP terms. Moreover,
so exponential domination gives
Thus the correction spread is eventually smaller than the radix width. Residue gluing converts the lattice interval into an ordinary consecutive interval [LM,UM][L_M,U_M][LM,UM] satisfying
for a fixed constant KKK.
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 sss, fix a bbb-exponent just beyond every AP band. Among the remaining a,ca,ca,c-exponents, choose the last point of the geometric grid
below a target of size cvMc^{vM}cvM. Because consecutive grid points differ by the fixed factor c/ac/ac/a, the selected monomial lies in a controlled multiplicative window. After restoring the common factors, this produces at least M−O(1)M-O(1)M−O(1) distinct optional monomials zzz satisfying
Every optional term is therefore no larger than the already available interval width. Adding such a term optionally—either use it or do not—extends a consecutive interval without changing its lower endpoint. Since all optional terms remain on the same exact level and lie beyond the AP exponent bands, primitiveness and disjointness are preserved.
Their combined contribution is
while the lower endpoint remains O(BM)O(B^M)O(BM). Hence the ratio of the upper endpoint to the lower endpoint grows linearly with MMM. For every requested R>1R>1R>1, and beyond every requested lower threshold, this constructs a primitively represented interval
This interior-shell amplification is what removes the finite-seed obstruction. The successful coordinate change was not merely “work on a homogeneous level,” but “place the main growth along an interior homogeneous ray, then use the unused transverse strip as optional mass.”
Completing the induction
The residue-reduction argument was strengthened to a flexible finite-seed gate: there are constants N0N_0N0 and C>1C>1C>1 such that any represented interval [N,CN][N,CN][N,CN] with N≥N0N\ge N_0N≥N0 implies d-completeness.
Applying the arbitrary-width construction with R=CR=CR=C proves d-completeness for ordered bases 1<a<c<b1<a<c<b1<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
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
with no sorryAx. The webpage literally writes a,b,c≥1a,b,c\ge1a,b,c≥1; that universal formulation is false at (1,1,1)(1,1,1)(1,1,1). The project records this separately and proves the intended nondegenerate a,b,c>1a,b,c>1a,b,c>1 conjecture used in the source literature and independent formal-conjecture encoding.
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/ Cursor
Download & Verify w/ Claude Code
Download & Verify w/ Codex
↓ Download full solution raw
2) Erdős Problem #254Erdős Problemwww.erdosproblems.com/254›QuestionLet A⊆NA\subseteq \mathbb{N}A⊆N be such that∣A∩[1,2x]∣−∣A∩[1,x]∣→∞ as x→∞\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty∣A∩[1,2x]∣−∣A∩[1,x]∣→∞ as x→∞and∑n∈A{θn}=∞\sum_{n\in A} \{ \theta n\}=\inftyn∈A∑{θn}=∞for every θ∈(0,1)\theta\in (0,1)θ∈(0,1), where {x}\{x\}{x} is the distance of xxx from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of AAA.(Erdős Problem #254 — number theory — https://www.erdosproblems.com/254)›ResultErdő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›ReportA 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
∑n∈A∥θn∥=∞
\sum_{n\in A}\|\theta n\|=\infty
n∈A∑∥θn∥=∞
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
∑n∈A∥θn∥,
\sum_{n\in A}\|\theta n\|,
n∈A∑∥θ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:
∑k∣Φ^(k)∣2=N∑j∣Φ(j)∣2.
\sum_k |\widehat\Phi(k)|^2
=N\sum_j|\Phi(j)|^2.
k∑∣Φ(k)∣2=Nj∑∣Φ(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
1N∑n<N∣μ^(n)∣2⟶0.
\frac1N\sum_{n<N}|\widehat\mu(n)|^2\longrightarrow0.
N1n<N∑∣μ(n)∣2⟶0.
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 AIThe 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
Let A⊆NA\subseteq \mathbb{N}A⊆N be such that∣A∩[1,2x]∣−∣A∩[1,x]∣→∞ as x→∞\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty∣A∩[1,2x]∣−∣A∩[1,x]∣→∞ as x→∞and∑n∈A{θn}=∞\sum_{n\in A} \{ \theta n\}=\inftyn∈A∑{θn}=∞for every θ∈(0,1)\theta\in (0,1)θ∈(0,1), where {x}\{x\}{x} is the distance of xxx from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of AAA.
(Erdős Problem #254 — number theory — https://www.erdosproblems.com/254)
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.
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
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
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:
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
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:
Its final output was:
Thus the proof uses only Lean/Mathlib’s standard quotient, extensionality, and classical-choice axioms, with no project-added axiom or proof placeholder.
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/ Cursor
Download & Verify w/ Claude Code
Download & Verify w/ Codex
↓ Download full solution raw
3) Erdős Problem #267Erdős Problemwww.erdosproblems.com/267›QuestionLet F1=F2=1F_1=F_2=1F1=F2=1 and Fn+1=Fn+Fn−1F_{n+1}=F_n+F_{n-1}Fn+1=Fn+Fn−1 be the Fibonacci sequence. Let n1<n2<⋯n_1<n_2<\cdots n1<n2<⋯ be an infinite sequence with nk+1/nk≥c>1n_{k+1}/n_k \geq c>1nk+1/nk≥c>1. Must∑k1Fnk\sum_k\frac{1}{F_{n_k}}k∑Fnk1be irrational?(Erdős Problem #267 — irrationality — https://www.erdosproblems.com/267)›ResultFor 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)›ReportIrrationality of Lacunary Fibonacci Reciprocal Sums
The problem and why it is difficult
Let F1=F2=1F_1=F_2=1F1=F2=1, Fn+1=Fn+Fn−1F_{n+1}=F_n+F_{n-1}Fn+1=Fn+Fn−1, and let n1<n2<⋯n_1<n_2<\cdotsn1<n2<⋯ be any infinite index sequence with a uniform ratio gap nk+1/nk≥cn_{k+1}/n_k\ge cnk+1/nk≥c for some c>1c>1c>1. Erdős asked whether
∑k1Fnk
\sum_k \frac{1}{F_{n_k}}
k∑Fnk1
must be irrational.
For fast-growing gaps this is classical territory: when c≥2c\ge 2c≥2 the series is covered by known irrationality criteria for lacunary series (Badea, 1993). The genuinely open range was 1<c<21<c<21<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=2c=2c=2, the tail ∑j>k1/Fnj\sum_{j>k}1/F_{n_j}∑j>k1/Fnj can be comparable to 1/Fnk1/F_{n_k}1/Fnk, so the classical "the fractional part cannot be that small" argument does not close.
Working modulo one denominator loses the structure. Individual FnF_nFn 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/Fn=5∑j(−1)njφ−(2j+1)n1/F_n=\sqrt5\sum_j(-1)^{nj}\varphi^{-(2j+1)n}1/Fn=5∑j(−1)njφ−(2j+1)n converts the series into a Lambert-type series in φ−1\varphi^{-1}φ−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.
- Exact Lambert and quadratic-norm infrastructure. The reciprocal Fibonacci expansion is collected into a locally finite integer coefficient word over Z[φ]\mathbb Z[\varphi]Z[φ]. 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 000 and 111 — impossible. The rest of the proof engineers such a comparison.
- 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.
- 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>1c>1c>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>1c>1c>1 with c≤nk+1/nkc\le n_{k+1}/n_kc≤nk+1/nk for all kkk. 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 AIThe 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
Let F1=F2=1F_1=F_2=1F1=F2=1 and Fn+1=Fn+Fn−1F_{n+1}=F_n+F_{n-1}Fn+1=Fn+Fn−1 be the Fibonacci sequence. Let n1<n2<⋯n_1<n_2<\cdots n1<n2<⋯ be an infinite sequence with nk+1/nk≥c>1n_{k+1}/n_k \geq c>1nk+1/nk≥c>1. Must∑k1Fnk\sum_k\frac{1}{F_{n_k}}k∑Fnk1be irrational?
(Erdős Problem #267 — irrationality — https://www.erdosproblems.com/267)
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.
Irrationality of Lacunary Fibonacci Reciprocal Sums
The problem and why it is difficult
Let F1=F2=1F_1=F_2=1F1=F2=1, Fn+1=Fn+Fn−1F_{n+1}=F_n+F_{n-1}Fn+1=Fn+Fn−1, and let n1<n2<⋯n_1<n_2<\cdotsn1<n2<⋯ be any infinite index sequence with a uniform ratio gap nk+1/nk≥cn_{k+1}/n_k\ge cnk+1/nk≥c for some c>1c>1c>1. Erdős asked whether
must be irrational.
For fast-growing gaps this is classical territory: when c≥2c\ge 2c≥2 the series is covered by known irrationality criteria for lacunary series (Badea, 1993). The genuinely open range was 1<c<21<c<21<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=2c=2c=2, the tail ∑j>k1/Fnj\sum_{j>k}1/F_{n_j}∑j>k1/Fnj can be comparable to 1/Fnk1/F_{n_k}1/Fnk, so the classical "the fractional part cannot be that small" argument does not close.
Working modulo one denominator loses the structure. Individual FnF_nFn 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/Fn=5∑j(−1)njφ−(2j+1)n1/F_n=\sqrt5\sum_j(-1)^{nj}\varphi^{-(2j+1)n}1/Fn=5∑j(−1)njφ−(2j+1)n converts the series into a Lambert-type series in φ−1\varphi^{-1}φ−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.
- Exact Lambert and quadratic-norm infrastructure. The reciprocal Fibonacci expansion is collected into a locally finite integer coefficient word over Z[φ]\mathbb Z[\varphi]Z[φ]. 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 000 and 111 — impossible. The rest of the proof engineers such a comparison.
- 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.
- 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>1c>1c>1.
Verification
The faithful statement quantifies over all index sequences with the exact quotient condition from the problem:
where reciprocalFibSeries is the real tsum of (Nat.fib (n k))⁻¹ and HasRatioGap asserts one real c>1c>1c>1 with c≤nk+1/nkc\le n_{k+1}/n_kc≤nk+1/nk for all kkk. 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.
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/ Cursor
Download & Verify w/ Claude Code
Download & Verify w/ Codex
↓ Download full solution raw
4) Erdős Problem #320Erdős Problemwww.erdosproblems.com/320›QuestionLet S(N)S(N)S(N) count the number of distinct sums of the form ∑n∈A1n\sum_{n\in A}\frac{1}{n}∑n∈An1 for A⊆{1,…,N}A\subseteq \{1,\ldots,N\}A⊆{1,…,N}. Estimate S(N)S(N)S(N).(Erdős Problem #320 — number theory, unit fractions — https://www.erdosproblems.com/320)›ResultLet 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
posi