Star Fleet Math
Built by Colin Snyder · colin@colinsnyder.com
Advised by Mike Kim · proposed solutions ↓
Inspired by Ignis · previously built by Myself, Dhruv Agarwal, & Nitin Kesarwani at the New Turing Institute
Star Fleet is an AI system that solves the world's hardest open mathematics problems using Lean 4. It's a Mac desktop app that controls up to 20 custom agentic harnesses called “starships” in parallel, each running its own GPT-5.6 instance on a dedicated 60-vCPU server and working on a separate math problem. Everything is built from scratch in TypeScript & Bun.
Each starship has access to:
x86-64 CPU bursts of up to 2,000 vCPUs for search programs that shard into thousands of independent single-core jobs
H100 GPU bursts for massively parallel search programs
The world's largest corpus, afaik, of Lean 4 premises (theorems & lemmas), searchable in plain English via gemini-embeddings-2 & chroma vector db
A Firecrawl.dev index of arXiv.org research papers & GitHub repos
Claude Fable API wrapped in a proof-verifier agentic harness to review submitted answers + an iMessage API to ask Colin (the human) for an additional review after Fable's approval
Ton 618, a local long-term memory system where every verified Lean 4 premise (theorem or lemma) is woven into a dependency graph, so proofs compound
A dedicated 60-vCPU, 120 GiB memory sandbox preinstalled with SAT/SMT solvers (CaDiCaL, kissat, Z3), Google's CP-SAT, computer algebra systems (SageMath, PARI/GP, GAP, Macaulay2), and the full Rust, CUDA C++, and Lean 4 toolchains
Solution Proposed (27)
Many problems listed as “open” carry informal or partial answers already available online; we tried extremely hard to avoid working on any such problems.
1) Erdős Problem #123Erdős Problemwww.erdosproblems.com/123›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 #129Erdős Problemwww.erdosproblems.com/129›QuestionLet R(n;k,r)R(n;k,r)R(n;k,r) be the smallest NNN such that if the edges of KNK_NKN are rrr-coloured then there is a set of nnn vertices which does not contain a copy of KkK_kKk in at least one of the rrr colours. Prove that there is a constant C=C(r)>1C=C(r)>1C=C(r)>1 such thatR(n;3,r)<Cn.R(n;3,r) < C^{\sqrt{n}}.R(n;3,r)<Cn.(Erdős Problem #129 — graph theory, ramsey theory — https://www.erdosproblems.com/129)›ResultThe proposed bound is false: for every natural n ≥ 120, 2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n), so no constant C > 1 can satisfy R(n;3,2) < C^(√n) for all n. Consequently the exact formal proposition LiteralProblem129 is false.theorem not_literalProblem129 : ¬ LiteralProblem129 := by
intro h
exact not_claimedBoundFor_two (h 2 (by omega))
theorem R3_two_global_exponential_sandwich (n : ℕ) (hn : 120 ≤ n) :
2 ^ (n / 120) < R3 n 2 ∧ R3 n 2 ≤ 2 ^ (2 * n) := by
exact ⟨two_pow_div_120_lt_R3_two n hn,
R3_two_le_two_pow_two_mul n⟩›ReportErdős Problem 129: a formally verified disproof
The problem and why it was deceptive
Erdős Problem 129 defines a Ramsey-type threshold R(n;3,r): the least order N such that every r-colouring of the edges of K_N has an n-vertex set on which at least one colour contains no triangle. The proposed bound was
R(n;3,r) < C(r)^(√n).
At first sight this looks like a difficult upper-bound problem in multicolour Ramsey theory. There was an additional historical obstacle: the modern Erdős Problems database already recorded Antonio Girão's observation that the displayed statement is false, but retained an OPEN label on the theory that the 1997 source must have intended some different, unstated definition.
That ambiguity mattered. Disproving a mistranscription would not solve the intended problem, while silently inventing a replacement would not answer the published question. The work therefore had to settle both the mathematics and the statement-fidelity issue.
What earlier reasoning missed
The decisive probabilistic estimate comes from looking at many edge-disjoint triangles inside every tested vertex set.
A random red-blue colouring makes any fixed triangle monochromatic in a specified colour with probability 1/8. If an n-set contains quadratically many edge-disjoint triangles, those events use disjoint edge variables and are independent. Consequently, the probability that the set has no triangle in a specified colour is exponentially small in n², not merely in n.
This is enough to union-bound over all n-subsets of a graph whose order is exponential in n. The printed exp(c√n) lower estimate was therefore simply a weak true estimate; it was not logically inconsistent with the published definition and did not force the existence of a missing condition.
There were also two formal dead ends:
An initial counting proof used Lean's native_decide. Although computationally correct, this introduced generated axioms and was unsuitable for a kernel-only certificate. It was replaced by kernel decide.
The first endpoint negated an operational least-order formulation, while the formal statement defined R using a natural-number infimum. That gap required a finite Ramsey theorem and a proof that the infimum is attained.
The construction that works
For each parameter t≥1, take an arbitrary set of 60t vertices and divide it into three equal parts. Latin-square triples of the form
(i, j, i+j)
produce a quadratic family of pairwise edge-disjoint triangles. The formal construction supplies 6(60t²+2) such triangles for every enumeration of the set.
For one target colour, a colouring that avoids a monochromatic packed triangle has at most
7^L · 2^(|E|-3L)
possibilities, where L is the packing size. Union-bounding over both colours and all enumerated 60t-sets shows that some colouring of K_(2^t) makes every 60t-set contain both a red triangle and a blue triangle. Thus the Ramsey property fails at ambient order 2^t.
This already defeats every square-root-exponential upper bound. To identify the actual scale, an elementary canonical-sequence proof gives the complementary finite Ramsey estimate R(n;3,2)≤2^(2n). Monotonicity in the tested set size then extends the packed lower bound from the subsequence n=60t to every n≥120:
2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n).
So the literal threshold is exponential with exponent linear in n, whereas the conjectured upper bound has exponent only √n.
Resolving the source ambiguity
The publisher scan of Erdős's 1997 paper was checked directly. It defines f_k^(r)(n) as the largest order admitting an r-colouring in which every n-set contains a K_k in every colour. Lean proves that, for k=3 and two colours, this admissibility condition is exactly the negation of the website's Ramsey predicate.
The investigation then followed the historical alternatives rather than assuming the scan was conclusive:
Erdős and Gyárfás's Split and balanced colorings of complete graphs defines different minimum-order split and balanced parameters, with polynomial rather than square-root-exponential behaviour.
Their A variant of the classical Ramsey problem studies (p,q)-colourings and a different extremal function.
Gyárfás's 2013 retrospective discusses both projects but gives no corrected version of Problem 129.
A searchable corpus of all 218 PDFs linked from Gyárfás's publication page revealed no later correction or alternative formulation.
The source's weak probabilistic lower bound therefore does not identify another problem, and no primary source supplies one. The formally verified disproof answers the only definite published statement. Girão retains priority for the elementary probabilistic objection; the contribution here is the complete formal certificate, exact threshold diagnosis, and source audit.
Verification
The proof is a standalone Lean 4 + Mathlib project. It includes:
the faithful definitions of edge colourings, monochromatic triangles, RamseyAt, and the exact infimum R3;
the Latin-square triangle packing and exact colouring count;
the union-bound construction;
ambient and test-size monotonicity;
finite Ramsey existence and infimum attainment;
the exact negation of the proposed theorem and the global exponential sandwich.
The verifier builds all 8572 targets, directly checks the final theorem file, and rejects native_decide, sorry, admit, or any declared axiom. The final theorems depend only on Mathlib's standard logical principles propext, Classical.choice, and Quot.sound.
cd verified_math/F-015_global-exponential-threshold/lean && bash verify.sh
The run ends with:
Build completed successfully (8572 jobs).
PASS: global exponential sandwich kernel-checked; no forbidden proof escape
›Download Full Solution & Verify with Your 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 R(n;k,r)R(n;k,r)R(n;k,r) be the smallest NNN such that if the edges of KNK_NKN are rrr-coloured then there is a set of nnn vertices which does not contain a copy of KkK_kKk in at least one of the rrr colours. Prove that there is a constant C=C(r)>1C=C(r)>1C=C(r)>1 such thatR(n;3,r)<Cn.R(n;3,r) < C^{\sqrt{n}}.R(n;3,r)<Cn.
(Erdős Problem #129 — graph theory, ramsey theory — https://www.erdosproblems.com/129)
The proposed bound is false: for every natural n ≥ 120, 2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n), so no constant C > 1 can satisfy R(n;3,2) < C^(√n) for all n. Consequently the exact formal proposition LiteralProblem129 is false.
Erdős Problem 129: a formally verified disproof
The problem and why it was deceptive
Erdős Problem 129 defines a Ramsey-type threshold R(n;3,r): the least order N such that every r-colouring of the edges of K_N has an n-vertex set on which at least one colour contains no triangle. The proposed bound was
R(n;3,r) < C(r)^(√n).
At first sight this looks like a difficult upper-bound problem in multicolour Ramsey theory. There was an additional historical obstacle: the modern Erdős Problems database already recorded Antonio Girão's observation that the displayed statement is false, but retained an OPEN label on the theory that the 1997 source must have intended some different, unstated definition.
That ambiguity mattered. Disproving a mistranscription would not solve the intended problem, while silently inventing a replacement would not answer the published question. The work therefore had to settle both the mathematics and the statement-fidelity issue.
What earlier reasoning missed
The decisive probabilistic estimate comes from looking at many edge-disjoint triangles inside every tested vertex set.
A random red-blue colouring makes any fixed triangle monochromatic in a specified colour with probability 1/8. If an n-set contains quadratically many edge-disjoint triangles, those events use disjoint edge variables and are independent. Consequently, the probability that the set has no triangle in a specified colour is exponentially small in n², not merely in n.
This is enough to union-bound over all n-subsets of a graph whose order is exponential in n. The printed exp(c√n) lower estimate was therefore simply a weak true estimate; it was not logically inconsistent with the published definition and did not force the existence of a missing condition.
There were also two formal dead ends:
An initial counting proof used Lean's native_decide. Although computationally correct, this introduced generated axioms and was unsuitable for a kernel-only certificate. It was replaced by kernel decide.
The first endpoint negated an operational least-order formulation, while the formal statement defined R using a natural-number infimum. That gap required a finite Ramsey theorem and a proof that the infimum is attained.
The construction that works
For each parameter t≥1, take an arbitrary set of 60t vertices and divide it into three equal parts. Latin-square triples of the form
(i, j, i+j)
produce a quadratic family of pairwise edge-disjoint triangles. The formal construction supplies 6(60t²+2) such triangles for every enumeration of the set.
For one target colour, a colouring that avoids a monochromatic packed triangle has at most
7^L · 2^(|E|-3L)
possibilities, where L is the packing size. Union-bounding over both colours and all enumerated 60t-sets shows that some colouring of K_(2^t) makes every 60t-set contain both a red triangle and a blue triangle. Thus the Ramsey property fails at ambient order 2^t.
This already defeats every square-root-exponential upper bound. To identify the actual scale, an elementary canonical-sequence proof gives the complementary finite Ramsey estimate R(n;3,2)≤2^(2n). Monotonicity in the tested set size then extends the packed lower bound from the subsequence n=60t to every n≥120:
2^(⌊n/120⌋) < R(n;3,2) ≤ 2^(2n).
So the literal threshold is exponential with exponent linear in n, whereas the conjectured upper bound has exponent only √n.
Resolving the source ambiguity
The publisher scan of Erdős's 1997 paper was checked directly. It defines f_k^(r)(n) as the largest order admitting an r-colouring in which every n-set contains a K_k in every colour. Lean proves that, for k=3 and two colours, this admissibility condition is exactly the negation of the website's Ramsey predicate.
The investigation then followed the historical alternatives rather than assuming the scan was conclusive:
Erdős and Gyárfás's Split and balanced colorings of complete graphs defines different minimum-order split and balanced parameters, with polynomial rather than square-root-exponential behaviour.
Their A variant of the classical Ramsey problem studies (p,q)-colourings and a different extremal function.
Gyárfás's 2013 retrospective discusses both projects but gives no corrected version of Problem 129.
A searchable corpus of all 218 PDFs linked from Gyárfás's publication page revealed no later correction or alternative formulation.
The source's weak probabilistic lower bound therefore does not identify another problem, and no primary source supplies one. The formally verified disproof answers the only definite published statement. Girão retains priority for the elementary probabilistic objection; the contribution here is the complete formal certificate, exact threshold diagnosis, and source audit.
Verification
The proof is a standalone Lean 4 + Mathlib project. It includes:
the faithful definitions of edge colourings, monochromatic triangles, RamseyAt, and the exact infimum R3;
the Latin-square triangle packing and exact colouring count;
the union-bound construction;
ambient and test-size monotonicity;
finite Ramsey existence and infimum attainment;
the exact negation of the proposed theorem and the global exponential sandwich.
The verifier builds all 8572 targets, directly checks the final theorem file, and rejects native_decide, sorry, admit, or any declared axiom. The final theorems depend only on Mathlib's standard logical principles propext, Classical.choice, and Quot.sound.
The run ends with:
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 #130Erdős Problemwww.erdosproblems.com/130›QuestionLet A⊂R2A\subset\mathbb{R}^2A⊂R2 be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in AAA, where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite?(Erdős Problem #130 — graph theory, chromatic number — https://www.erdosproblems.com/130)›ResultThere exists an infinite set A in R^2 containing no three collinear points and no four concyclic points such that, for every natural number k, the graph joining pairs at positive integer distance has no proper k-coloring. Thus the chromatic number in Erdos Problem #130 can be infinite.theorem Erdos130.erdos130_infinite_chromatic :
Exists fun A : Set Point =>
And A.Infinite
(And (GeneralPosition A)
(forall k : Nat, Not (HasKColoring A k))) := by
exact InfiniteAssembly.erdos130_infinite_chromatic_solution›ReportAn Infinite-Chromatic Integer-Distance Graph in General Position
The problem and the obstruction
Erdős Problem #130 asks whether an infinite set of points in the real plane can simultaneously satisfy two demands that pull in opposite directions:
strong general position: no three points are collinear and no four are concyclic;
arithmetic density: the graph joining pairs at positive integer distance has infinite chromatic number.
The difficulty is not merely finding many integer distances. Classical constructions can realize complicated finite graphs by integer distances, but they often put all vertices on one circle. Conversely, placing points on a parabola or another rigid curve makes general position nearly automatic, but turns integer distance into a sparse Diophantine condition whose chromatic behavior is opaque.
Even the clique version illustrates the rigidity: a general-position integral clique of size seven is known, while the next case has resisted direct attack. An infinite-chromatic graph cannot therefore be expected to arise from simply enlarging cliques.
Where the natural approaches stalled
Several standard coordinate systems expose only one half of the problem.
Universal finite-graph realizations control distances but are typically cocircular, violating the no-four-on-a-circle condition in the strongest possible way.
Parabola and hyperbola parametrizations solve the incidence problem, but reduce adjacency to Pythagorean sum or product graphs over the rationals. Exact searches found small chromatic examples, not a mechanism forcing unbounded chromatic number.
Finite-field parabola caps avoid collinear triples but produced low-degeneracy integer-distance graphs and many cyclic configurations.
Naive homothetic Ramsey constructions can force chromatic complexity, but a finite homothetic Ramsey witness necessarily contains structured collinear subsets. General position cannot simply be appended afterward.
The underlying mismatch was trying to make the points themselves carry both the Ramsey structure and the incidence genericity. The successful construction assigns those jobs to different geometric objects and different stages.
The change of coordinates: circles first, points later
The key move is to construct a graph as a circle tangency graph and only afterward extract planar points.
For positive circles with rational centers and rational radii, external tangency gives
∣ci−cj∣=ri+rj.
|c_i-c_j|=r_i+r_j.
∣ci−cj∣=ri+rj.
Thus tangency already supplies rational center distances. After a common scaling, those distances become integers. Circle configurations also have enough continuous algebraic freedom to impose genericity without destroying their prescribed tangencies.
This separates the proof into three independent tasks:
build finite rational circle tangency graphs of arbitrarily high chromatic number;
use circle inversion to make their centers geometrically generic;
place countably many finite point blocks together without creating mixed degeneracies.
The Hales--Jewett tangency booster
Suppose a finite circle family indexed by an alphabet α has no proper coloring by k colors. Hales--Jewett supplies a finite word dimension ι such that every coloring of the words ι → α contains a monochromatic combinatorial line.
For positive weights γᵢ, each word determines weighted center and radius data. The construction introduces:
a large circle for every word;
a small homothetic copy of the old family for every combinatorial line;
one matched tangency between each word on that line and its corresponding circle in the small copy.
If the new family had a (k+1)-coloring, Hales--Jewett would give a monochromatic line among the large circles. If a matched small circle used that color, its matched tangency would be monochromatic. Otherwise the entire small copy avoids that color and induces a k-coloring of the old family, again impossible. This raises the required number of colors by one.
The combinatorial identity is easy; preserving geometry is not. The induction maintains a GoodFamily invariant:
every radius is positive;
centers are injectively indexed;
no distinct pair is internally tangent;
no distinctly indexed triple is coaxial.
Every possible failure for the large word circles is represented by an explicit multivariate polynomial in the weights and large radius. Pair and triple nonidentity lemmas show that their finite product is nonzero. Polynomial extensionality on an infinite rational box then chooses positive rational weights and a sufficiently large rational radius avoiding every failure simultaneously.
Each small line copy is adjoined in a rational direction on the unit circle. A second finite product of univariate exceptional polynomials excludes mixed center collisions, internal tangencies, and coaxial triples. Iterating from one circle yields finite positive rational good circle families with arbitrarily high tangency chromatic number.
Why inversion fixes general position
Taking the original circle centers would not suffice. Instead, invert the circles about a generic rational center O. For a circle with center c_i and radius r_i, write
Di=∣ci−O∣2−ri2.
D_i=|c_i-O|^2-r_i^2.
Di=∣ci−O∣2−ri2.
When D_i≠0, the image circle has relative center
pi=ci−ODi.
p_i=\frac{c_i-O}{D_i}.
pi=Dici−O.
Three such centers are collinear precisely when a denominator-cleared determinant vanishes. As a polynomial in O, that determinant is identically zero exactly for a coaxial source triple. The induction has already excluded those triples.
The quadruple condition is subtler. Its cleared cyclic determinant is again a polynomial in O. If it vanished identically, a Lorentzian circle-space argument would force four positive circle vectors into a forbidden pairwise-orthogonal configuration. The formal Gram-determinant identity rules this out whenever the relevant source triples are noncoaxial.
There are only finitely many denominator, triple, and quadruple conditions. Their product is a nonzero bivariate polynomial, so one rational inversion center avoids all of them. The inverse centers therefore have nonzero orientation for every distinct triple and nonzero cyclic determinant for every distinct quadruple.
Tangency survives in the exact form
∣pi−pj∣2=(riDi+rjDj)2.
|p_i-p_j|^2=
\left(\frac{r_i}{D_i}+\frac{r_j}{D_j}\right)^2.
∣pi−pj∣2=(Diri+Djrj)2.
All terms are rational. A single positive natural multiplier clears the denominators of every signed transformed radius. Uniformly scaling the inverse centers then turns every required tangency edge into a positive integer-distance edge while preserving general position.
The final obstacle: combining all finite witnesses
Unbounded finite chromatic number is not yet one infinite example. Arbitrary translations of finite blocks preserve their internal integer distances, but may create new collinear triples or concyclic quadruples involving several blocks.
The blocks are inserted recursively. A new block is translated by
(t,t3).
(t,t^3).
(t,t3).
For each insertion, every mixed collision, orientation, and cyclic determinant becomes an explicit univariate polynomial in t. The one-moving and three-moving cases have a leading coefficient equal, up to sign, to a nonzero orientation. The decisive two-moving/two-fixed cyclic case has coefficients
K6=−(Ax−Bx)(Cy−Dy)−(Ay−By)(Cx−Dx),K4=−2((Ax−Bx)(Cx−Dx)−(Ay−By)(Cy−Dy)).
\begin{aligned}
K_6&=-(A_x-B_x)(C_y-D_y)-(A_y-B_y)(C_x-D_x),\\
K_4&=-2\big((A_x-B_x)(C_x-D_x)-(A_y-B_y)(C_y-D_y)\big).
\end{aligned}
K6K4=−(Ax−Bx)(Cy−Dy)−(Ay−By)(Cx−Dx),=−2((Ax−Bx)(Cx−Dx)−(Ay−By)(Cy−Dy)).
If both vanished, the product
∣A−B∣2 ∣C−D∣2
|A-B|^2\,|C-D|^2
∣A−B∣2∣C−D∣2
would vanish. Both pairs are distinct, so this is impossible. Hence every mixed exceptional polynomial is genuine. A rational t avoids their finite product.
A verified prefix state stores all parameters chosen so far together with a proof of strong general position. Earlier parameters remain unchanged when a block is added. Any finite tuple of points in the eventual countable union appears in some later verified prefix, so global general position follows. Translation preserves every within-block distance, and the kth block still defeats every k-coloring. Therefore the final integer-distance graph has no finite proper coloring.
Formal verification
The proof is fully machine-checked in Lean 4 + Mathlib against the original pinned statement, not a weakened surrogate. The final theorem is:
theorem Erdos130.erdos130_infinite_chromatic :
∃ A : Set Point,
A.Infinite ∧ GeneralPosition A ∧ ∀ k : ℕ, ¬ HasKColoring A k
Verification included:
a clean lake clean && lake build of the checker project;
an empty scan for sorry, admit, or declared axioms;
an axiom audit showing only Mathlib's standard propext, Classical.choice, and Quot.sound;
a second self-contained build of the archived F-017 proof project;
an independent referee rerun and acceptance.
The final proof artifact is verified_math/F-017_erdos130-infinite-chromatic-solution/Research/InfiniteAssembly.lean; the exact verifier-facing theorem is in Research/Basic.lean in the same archived project.›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⊂R2A\subset\mathbb{R}^2A⊂R2 be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in AAA, where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite?
(Erdős Problem #130 — graph theory, chromatic number — https://www.erdosproblems.com/130)
There exists an infinite set A in R^2 containing no three collinear points and no four concyclic points such that, for every natural number k, the graph joining pairs at positive integer distance has no proper k-coloring. Thus the chromatic number in Erdos Problem #130 can be infinite.
An Infinite-Chromatic Integer-Distance Graph in General Position
The problem and the obstruction
Erdős Problem #130 asks whether an infinite set of points in the real plane can simultaneously satisfy two demands that pull in opposite directions:
strong general position: no three points are collinear and no four are concyclic;
arithmetic density: the graph joining pairs at positive integer distance has infinite chromatic number.
The difficulty is not merely finding many integer distances. Classical constructions can realize complicated finite graphs by integer distances, but they often put all vertices on one circle. Conversely, placing points on a parabola or another rigid curve makes general position nearly automatic, but turns integer distance into a sparse Diophantine condition whose chromatic behavior is opaque.
Even the clique version illustrates the rigidity: a general-position integral clique of size seven is known, while the next case has resisted direct attack. An infinite-chromatic graph cannot therefore be expected to arise from simply enlarging cliques.
Where the natural approaches stalled
Several standard coordinate systems expose only one half of the problem.
Universal finite-graph realizations control distances but are typically cocircular, violating the no-four-on-a-circle condition in the strongest possible way.
Parabola and hyperbola parametrizations solve the incidence problem, but reduce adjacency to Pythagorean sum or product graphs over the rationals. Exact searches found small chromatic examples, not a mechanism forcing unbounded chromatic number.
Finite-field parabola caps avoid collinear triples but produced low-degeneracy integer-distance graphs and many cyclic configurations.
Naive homothetic Ramsey constructions can force chromatic complexity, but a finite homothetic Ramsey witness necessarily contains structured collinear subsets. General position cannot simply be appended afterward.
The underlying mismatch was trying to make the points themselves carry both the Ramsey structure and the incidence genericity. The successful construction assigns those jobs to different geometric objects and different stages.
The change of coordinates: circles first, points later
The key move is to construct a graph as a circle tangency graph and only afterward extract planar points.
For positive circles with rational centers and rational radii, external tangency gives
Thus tangency already supplies rational center distances. After a common scaling, those distances become integers. Circle configurations also have enough continuous algebraic freedom to impose genericity without destroying their prescribed tangencies.
This separates the proof into three independent tasks:
build finite rational circle tangency graphs of arbitrarily high chromatic number;
use circle inversion to make their centers geometrically generic;
place countably many finite point blocks together without creating mixed degeneracies.
The Hales--Jewett tangency booster
Suppose a finite circle family indexed by an alphabet α has no proper coloring by k colors. Hales--Jewett supplies a finite word dimension ι such that every coloring of the words ι → α contains a monochromatic combinatorial line.
For positive weights γᵢ, each word determines weighted center and radius data. The construction introduces:
a large circle for every word;
a small homothetic copy of the old family for every combinatorial line;
one matched tangency between each word on that line and its corresponding circle in the small copy.
If the new family had a (k+1)-coloring, Hales--Jewett would give a monochromatic line among the large circles. If a matched small circle used that color, its matched tangency would be monochromatic. Otherwise the entire small copy avoids that color and induces a k-