Patrick White and Claude (an AI) have attempted 615 Erdős problems. Each row is one attempt: a full write-up, a working report, or an early run — labelled by what actually happened. The labels are ours; the community database's status for each problem is on its own page. How we work and what the labels mean.
Every Ramsey set lies on a sphere. Write its points as p_i = (1, a_i), with coordinates generating a field F: the set is Ramsey exactly when its sphere equation can be lifted from F to the tensor ring F ⊗ F before multiplying out. With algebraic coordinates the lift always exists (a corollary first published in AI-generated repositories), so only transcendental coordinates can break Graham's conjecture: Pálvölgyi's seven points, OpenAI's twelve, and eight inside those twelve, among them a square and a rectangle on one circle. The theorem is OpenAI's.
Read the report ↗A greedy prefix, then one auxiliary denominator M built from products of primes near (log b)¹⁰⁰: one unit fraction at a time replaces a numerator u by the least residue of −Qt mod u, a uniform divisor moment keeps the failures sparse across O(log log b) levels, and two good numerators add up to the one you need. Bloom and van Doorn have since found a much shorter route through the paper's own §§7–8. Nothing in the theorems is ours.
Read the report ↗Take a finite set S of primes closed under p ↦ prime factors of p−1, and the totients a_K = φ(∏_{p∈S} p^K). Every prime in a preimage has p−1 dividing a_K, so it is in S or has p−1 S-smooth. If only finitely many of the latter existed, the K−1 copies of each p in a_K could not be absorbed, every p ∈ S would divide the least preimage, and ℓ(a_K)/a_K would reach ∏ p/(p−1). Read backwards: a bound below that product needs infinitely many S-smooth shifted primes (for S = {2} this is Carmichael's ℓ(2^k) = 2^(k+1)). Computed exactly, the least preimage of a_K is one to three such primes for every K we reached.
Read the report ↗Split each preimage into a long prefix of large primes, counted by the volume of Ford's simplex, and a short arithmetic tail kept exactly; inclusion–exclusion over tails that give the same totient makes the coefficient, and a sieve comparison shows different prefixes almost never collide. Counting the largest prime with the same data at x and x/c gives V(cx)/V(x) → c. The coefficient is defined but out of reach: from the third tail prime on, its primes exceed 10^13000, and the theorem gives no rate for A_H → A. No totient below 10⁹ has least preimage above 2.5 times itself, so the paper's open case k = 3 stays open. Nothing in the theorem is ours.
Read the report ↗Average over starting points with the square of a signed sum of smooth divisor sums over the second of two adjacent intervals: alternating signs between neighbouring dimensions make the weighted number of primes there as small as wanted, while the first interval keeps its share. Requiring a prime just before the empty interval means each gap is counted at most h times, so empty intervals become distinct gaps. At ten checkpoints from N = 10⁶ to 10⁹ the share of increases stays between 39.7% and 42.1%. Nothing in the theorem is ours.
Read the report ↗Choose vertex weights that maximize an entropy-minus-edge-mass potential and delete closed neighbourhoods one at a time: everything reduces to bounding the weighted triangle mass by the edge mass. Clique exclusion enters once, through mean-one random multipliers that bound the weighted edges between any two vertex sets; a separate theorem turns that bound into the triangle estimate by splitting vertices along random walks inside their neighbourhoods. The constant the printed proof gives is about 10^(−3.6·10¹⁸) for r = 4. Nothing in the theorem is ours.
Read the report ↗Take a minimal counterexample, with k = m−1: every nonempty independent set I has a closed neighbourhood of at least k|I|+1 vertices. That forces a clique of order at least max{3, ⌊k/2⌋}. A clique of order 9 or more is ruled out by hand, through an optimal system of paths between clique vertices whose short improvements would close a cycle of exactly m vertices. What is left is 3,099 patterns of such paths over 42 pairs (k, t), each excluded by proved inference rules — twice in Python and, by a different encoding, in Lean.
Read the report ↗Two projectors are at the full distance √2 exactly when their lines are orthogonal. A ten-piece cover gives ten functions on ℝP³ that never share a label across orthogonal lines; extended to symmetric matrices it is an odd map S⁹ → S⁹, whose degree forces every tetrahedron's six-label complement to carry a six-vertex ℝP², and no complex on ten labels can have that on every facet complement. Every line is within 41.39° of one of eleven fixed lines (exact rational certificate), which gives the matching eleven-piece cover.
Read the report ↗Bradač's ordered incident-flag graph on PG(d,q), sampled as a stream of independent flags, has no K_(d+1). A long consistent (independent) sequence would carry entropy at least dσℓ + ηℓ log σ − O(k) (σ = log q, ℓ = Θ(k)); after a bounded number of compression rounds — marking à la Bradač, and polynomial-method descriptions of sparse incidence structures whose degrees stay below the characteristic — a decoder rebuilds a Θ(k)-long subsequence from dσℓ + O(k). The Lean states the construction for every d ≥ 3; OpenAI's assembly, copied with 6 ≤ s relaxed to 4 ≤ s, gives r(4,t) ≥ t³/(log t)^(2+ε), past Mattheus–Verstraëte's t³/(log t)⁴, on the three standard axioms. Chen and Lin–Zhang derived that r(4,t) statement on paper on 11 and 13 October from OpenAI's result; we know of no earlier kernel check of it.
Read the report ↗Bucić–Montgomery had O(n log* n). Coffey keeps their rounds and makes leftover edges contract into small simple quotients (total order ≤ n/4) whose decompositions lift back; OpenAI picks one scale layer, identifies pairs of low-degree vertices, and pays for the overlap with a potential φ(n) = max{½, 1 − 1/√log n}; Kim charges heavy cycles to a degree potential and everything else to deleted vertices. Coffey formalized Formal Conjectures’ statement itself; OpenAI formalized its own, and Formal Conjectures credits that proof — the transport between them (routine on paper, about 200 lines of Lean) was in neither repository, so we wrote it and the kernel accepted it, against a verbatim copy of Formal Conjectures’ statement. The constants are astronomical (OpenAI’s C exceeds 2^(7.6·10¹²)).
Read the report ↗O = {0,49,75,83,98,101,117,119,121,159,269} has exactly nine 3-term progressions, one centred at each interior point; φ(x) = 101 + 18x/269 drops a shrunken copy of O onto the gap between 101 and 119, and no additive relation ever crosses copies. Depth K: 11 + 9K points, largest Sidon subset exactly 7 + 5K, so c ≤ 5/9 (9/17 ≤ c ≤ 5/9 now). Checked to 119 points exhaustively and 83 by two solvers, and for every depth by a level argument modulo 269.
Read the report ↗Theorem 1.1 colours ℤ/q^Dℤ, q^D ≥ k^(ck), with an outer colouring of coordinate labels chosen by a finite local lemma, a dichotomy that makes every progression either balanced in both outer colours or globally affine in its centred coordinates (the dilation λ removes every rational period up to D² — the quantitative idea), and a Bernoulli(k^(−1/20)) flip per Behrend-type norm-band key, each key occurring at most four times on any progression; a digit product then gives every r ≥ 2 from the same cyclic colouring. Our replay built all 115 Lean modules (430 s, 0 errors), printed standard axioms on the theorem, on kthRoot_tendsto — the page's W(k)^(1/k) → ∞ at r = 2 — and on the cyclic witness, matched the statement and its definitions to the comparator byte for byte, compiled the page's sentence as a probe, and ran the wrong-shape and sorry controls; seven seats found no gap in the proof of Theorem 1.1 and noticed that the Lean proves §3's and §6's counts in weaker forms than printed, that the multiplicity bound is really 2, and that the bound overtakes 2^k only past k ≈ 10^30103. Campos–Fox–Schildkraut's k·2^(k−1) (August, colouring by ChatGPT) answered W(k)/2^k → ∞; this is the k-th root. Not ours.
Read the report ↗Dickson's greedy rule from a finite seed was conjectured (Erdős #341) to have eventually periodic gaps; Li disproved it in August with an engineered 21-element seed whose structure is a modular shield plus a self-similar controller on three residue rails. The smallest seed by largest element that resists every finite test is six elements inside [12]. Through 10⁸ its gap sequence has no gap period ≤ 3,905,308 terms beginning at or before term 7,810,617 (a ≈ 5·10⁷). Its spectrum sits on the multiples of one frequency g = 0.28459194 (the hostile referee caught that a first draft's two frequencies satisfy 4f₁ + 9f₂ ≡ 0), its near-periods are g's convergent denominators, and under x ↦ {xg} the set is a five-arc window — membership exactly 1 on the arcs' cores, exactly 0 in the deep complement, about one half in edge zones a tenth of the circle wide, where the greedy completes its sumset and where any proof must work. Calkin and Erdős showed a clean rotation coding can never be a greedy extension; E is one up to its edges. A SAT census closes the other direction: Li's shield is infeasible for every doubling cycle of three or more rails at every modulus below 49, and the two-rail survivors have periodic controllers. Not a counterexample — a precise wall, with the shape of the missing proof named.
Read the report ↗Theorem 1.3 transfers any colouring at all to a weak measurable one through a rigidity theorem for rotation-invariant laws on the dual of the algebraic plane (false over the rationals — the seats found the sentence, p. 13, where square roots in the real algebraic field do the work Payne's rational graph cannot); Theorem 1.4 kills five weak-measurable labels by continua of common exclusion and a rational placement of the Moser spindle. Our replay built all 70 Lean modules (1,263 s, 0 errors), printed standard axioms for the theorem and everything it rests on, proved the comparator's statement verbatim from the solution, closed the page's lower-bound statement from scratch in three forms, and rejected the six-colour and distance-2 controls; seven seats found no gap in 62 pages and one theorem left unstated (the measurable chromatic number is at least 6 too). The exact value, 6 or 7, stays open. Not ours.
Read the report ↗Erdős (#1159) asked whether one constant bounds, for every finite projective plane, the fewest points per line a blocking set can be made to have. The floor is 4 for all orders ≥ 5 and is met through q = 11 — at q = 11 by Klein's configuration, which two solvers, a 1997 annealing run and a three-point closed form all land on. At q = 13 every symmetric reduction is infeasible, plain SAT finds nothing, and the 1997 record stopped at 5; the UNSAT cubes are running.
Read the report ↗Theorem 1.1 says large repeated distance fibers are rare; its half-page corollary gives all but o(n) pins at least n^(1−ε) distances. Our replay built all 48 Lean modules (508 s, 0 errors), matched the statement to the comparator byte for byte, closed the problem page's own question from exists_pin_eventually, and ran the wrong-shape and sorry controls; eight seats found no gap in the 27 pages and noticed the argument proves a more general Theorem G (two injective coordinates over a number field), whose core contradiction the Lean states at that generality. The n/√log n question and the averaged form stay open. Not ours.
Read the report ↗Green's list (comments to Problem 7) poses Dickson's greedy question for both rules and marks both open; Li's August seed settles the equal-summand one and is periodic under the other. Replace 77 by 56 — A = {1, 2, 3, 5, 7, 13, 22, 27, 28, 32, 36, 40, 47, 48, 52, 56, 63, 71, 81, 89, 97} — and the greedy extension has no eventual period under Queneau's rule, nor under Dickson's: Li's shield mod 49 with a new three-rail controller switched by the blocks [8^k+1, 2·8^k], [4·8^k, 8·8^k], [2·8^k, 4·8^k], every identity proved by hand. Nothing was designed — the greedy computes its own controller once the seed's rail content is fixed, and 18 of the 27 seeds of this shape show no period in the window tested. An independent greedy on the integers matches the closed form at every integer to 10⁷.
Read the report ↗Erdős #203 asks for a two-dimensional Sierpiński number. Every known route is a covering system — one coset of a lattice of index e_p = |⟨2,3⟩ mod p| per prime, the cosets covering ℤ². Two days ago we excluded every period up to 65,520 by a forced overlap and exact seven-prime block maxima; five computed pools with up to 99 primes and density up to 1.249 survived. Restrict the covering to the lines of a direction (Neumann's classical lemma on coset covers): each prime reaches one class of lines with intensity 1/ord_p(2^a 3^b), so every line needs ≥ 1. On the lines of slope 1, 6 ≡ 1 mod 5 makes 5 cover a quarter of the lines completely and 7 cover half of a third of them; on the half neither touches, the other primes can average at most a finite sum B, and B < 1 for every pool: ≤ 0.834 at every period ≤ 65,520 with density ≥ 1, and 0.849 · 0.868 · 0.854 · 0.884 · 0.937 at 110880 · 166320 · 221760 · 332640 · 720720. Exact integer programs (CP-SAT, with HiGHS and the referee's own branch-and-bound where they finished) give sharper upper bounds at several periods. No pure covering system has period ≤ 65,520 or dividing any of the five; the perfect-power variant stays open at 55440 and 65520. The problem stays open — the constant part of any fixed direction appears to grow with the pool, so a proof for all N needs the full covering problem.
Read the report ↗Erdős's unit distance conjecture is false (OpenAI, May 2026: n^{1+c}); the upper bound has been Spencer–Szemerédi–Trotter's n^{4/3} for 42 years, and the page says why — a different metric attains it. OpenAI's 23 September paper complexifies the unit circle into zw = 1 and proves no configuration can have t^{4−o(1)} unit pairs: bounded jump heights die on a 3-neighbour determinant, unbounded ones on an entropy-prediction device, a product-formula score budget and a Kummer-theory obstruction in an ultraproduct. Nine seats verified every lemma line by line with instruments that fail on controls; the Euclidean input sits in exactly four places; two exposition defects found. A 40-file Lean proof is in the release but not in its catalogue — our kernel replay is queued and this card is updated when it reports.
Read the report ↗Is every infinite set avoided by some set of positive measure? Open for {qⁿ} since 1974; the page lists {1, 1/2, 1/4, …} as the open case. OpenAI's 5 October paper constructs, for every ratio, a compact subset of [0,1] of measure 1 − η that meets every nontrivial affine copy of the sequence, by routing the line through a finite tree of random tables that spends its measure budget once while the number of independent tests grows. Four hostile seats verified every lemma; exact-arithmetic simulations of the construction match its exact probability formula with controls that fail. OpenAI's Lean proves the q = ½ case; on our machine the kernel printed only the three standard axioms on a statement identical to the challenge. The general conjecture stays open.
Read the report ↗Erdős #188 asks for the least k such that the plane can be red/blue coloured with no red unit pair and no k blue points in unit-spaced arithmetic progression. Currier–Mody–Xie–Zhang (arXiv, June 2026) prove k ≤ 6330 by a random colouring of a hexagonal tiling; every constant recomputed here, the bound stands, and parametrising the progression by its three real degrees of freedom instead of four turns the identical argument into k ≤ 4917. On the other side, EGMRSS's k ≥ 5 and Tsaturian's k ≥ 6 become UNSAT certificates on 15 and 69 points of the unit triangular lattice and its Moser-angle rotations, every clause verified exactly in ℚ(√3, √11), minimal, closed by three solvers and drat-trim. The same apparatus at ℓ₆ neither certified k ≥ 7 nor refuted the lattice route — the instances that could decide it ran out their time caps undecided.
Read the report ↗Extend a finite set by the least integer that is not a sum of two earlier terms; Erdős–Graham asked whether the gaps are always eventually periodic. Li (with GPT-5.6 Sol) writes the greedy extension of {1, 2, 3, 5, 7, 13, 22, 27, 28, 32, 36, 40, 47, 48, 52, 63, 71, 77, 81, 89, 97} in closed form — five full residue classes mod 49 and three rails switched by blocks of quotients that grow like powers of eight — and proves it obeys the rule by a finite check mod 49. Our own greedy from the seed matches his set at every integer to 10⁷, the Lean builds on the three standard axioms on our machine, and the statement is the problem's negation. Under the other convention (distinct summands, Queneau) the same seed is periodic, certified — that variant stays open. The answer to #341 is no; nothing in it is ours.
Read the report ↗Erdős #160 asks how many colours [N] needs so every 4-AP sees three. Two July 2026 preprints on the proof-claims tab — Itabe's N^{1/3+o(1)} with a Lean development, Shi–Dong's N^{1/4+o(1)} (arXiv 2607.20752) — share one idea: a base-p carry control forces an ABBA-coloured progression's digit vectors into a genuine line, and the F_{p³}/F_p norm, zero only at zero, cannot be symmetric on a line. We read both lemma by lemma, enumerated Shi–Dong's 27p-colouring of ℤ/p⁴ℤ for p ≤ 13 (two implementations through p = 11; none symmetric, palette within 27p, controls fire), sampled their k = 6 colouring on 2.2·10⁸ progressions, kernel-replayed Itabe's Lean (standard axioms, statement matched), and ran four hostile seats. Both hold as read: nothing fatal; two one-line gaps in Shi–Dong's prose (a carry case their Lemma 2.1 does not cover; a false reason at x = M/2 that the conclusion survives), one stale sentence, and, on priority, that Itabe was public eight days before Shi–Dong's v1, which did not cite him; v2 calls it 'a concurrent result'. His cubic factor is, up to basis, their k = 4 colouring restricted to pℤ/p⁴ℤ. Also exact values we could not find written down anywhere: h(N) = 3, 4, 5, 6 on 4–12, 13–22, 23–35, 36–51.
Read the report ↗Alice colours one edge, Bob two; Bob needs a strictly larger clique. Exact backward induction over isomorphism classes decides K₈ for Bob in twelve seconds; a 210,325-position strategy certificate is accepted by an independent nauty-based checker that rejects deleted, flipped, fabricated and mass-swapped certificates, and our July engine agrees after 41½ minutes. The proof claim on the tab — Didin and Pimenov's three-page potential argument that Bob wins for every n ≥ 3^158, with a Lean 4 development — holds as read under three Opus seats (one hostile) and kernel-replays green here. K₉ followed the same day: 313,106,283 nodes, a 20,802,845-position certificate accepted by a second checker. Everything from 10 up to the certified threshold 3^158 is still open (the paper's own constants reach down to about 10^70.9).
Read the report ↗Two days after F*(13) = 6, the next rung: the all-positive case and three sign patterns fell to z3 directly, the four hardest timed out at 12 h and were split on where their outermost negatives sit among the positives — 244 covering cubes, all UNSAT, 70.5 CPU-hours — and a flat 36-hour arm then independently closed all four (14.6–24.1 h each). The exact table through n = 15 now exceeds ⌈(n+2)/3⌉ at n = 13 and 15 only; the asymptotic question is untouched.
Read the report ↗The only proof claim on erdosproblems.com/128 (Amir Sarid, August 2026) gets β ≤ 0.0262 from a new C₄ flag certificate tight at the Clebsch graph plus a one-vertex perturbation fed by Balogh–Clemen–Lidický's n²/23.5 max-cut bound. Every lemma recomputed two ways, the certificate re-established by an independent exact verifier, the Lean kernel-replayed on our box with standard axioms and a statement match. The hole is upstream: BCL Theorem 2(a) exists only as a six-page EuroComb extended abstract whose proof sketch never separately covers the part he uses, and no public certificate, so the unconditional record is still 27/1024. Two errors on the live problem page found on the way.
Read the report ↗The headline question of #477 was closed by others (Peng et al., June; Price's even K ≥ 6 in Lean, August). Our July proof covers every K ≥ 3, cubes included — the case the Lean record still calls 'probably no'. Two independent machine referees re-read the whole chain against the primary papers on 11 October and found no gap; they did find and fix write-up defects. Next stop: a human.
Read the report ↗Every oriented graph on 21 vertices contains an independent triple or a transitive 4-tournament; 20-vertex exceptions were already known, so k(3,4) is exactly 21 (the literature had 21–25). One vertex's neighbourhoods admit only 1, 7 and 1 shapes, which turns order 21 into 346 small SAT cases — 274 closed plain, 72 under lossless lex-leader symmetry breaking, every UNSAT proof replayed by drat-trim, the symmetry clauses themselves tested on 219 random orbits. One cell in a table the problem asks to understand asymptotically; nothing claimed about k(n,m) in general.
Read the report ↗Below smoothness exponent 0.284 nothing of this strength was known; the paper's parity-breaking step is a new transference theorem for weighted dilation graphs. Ten hostile seats found no mathematical gap; the decisive identity was rebuilt as an exact computation and made to fail on purpose. No Lean exists for anything but the last page. Not ours; not closed.
Read the report ↗Nobody had the exponent 2/d in any d ≥ 3; the paper claims it with a constant factor and no power saving anywhere, which is more than Erdős conjectured. Twelve hostile seats — one per section, plus a whole-paper read, a citation sweep, numerics and a Lean source audit — found no mathematical gap, no hidden rate and no cycle among the constants; a third-party Lean 4 proof exists and our own kernel replay of it printed only propext, Classical.choice and Quot.sound, and the fresh re-check of Mathlib's cache exited 0 after 7,919 s. Not ours; closed in the literature.
Read the report ↗Open for every k ≥ 4 until this release — the prior record (Leng–Sah–Sawhney 2024) was not dyadically summable. The paper claims quasipolynomial bounds for every length; the Lean it ships proves a weaker new bound, exp(−c(log log N)^(1+η)), that still settles Erdős's question — audited at source by us (4,774 files, no sorry, no axioms, statement identical to the challenge), seven hostile seats found no gap in the 198 pages, and our own kernel replay printed only propext, Classical.choice and Quot.sound. Not ours; closed in the literature.
Read the report ↗Is every ±1 polynomial a fixed fraction above √n in maximum modulus? Open since the 1950s; Odlyzko's exhaustive search pointed to a limit near 1.27. OpenAI's 23 September paper proves the limit is 1, its Lean states exactly that, and on our machine the kernel printed only the three standard axioms. Seven hostile seats read the proof and the two-sided paper: no gap. The theorem is OpenAI's; the audit and the replay are ours.
Read the report ↗Owings's 1974 two-colour sumset question was answered affirmatively eight days ago (Huang–Lian–Shao–Xiao–Xu–Zhang, arXiv:2607.17333). The live page still said OPEN. We found the preprint, audited the proof (digest-pinned v2, no gap modulo the named Stone–Čech inputs), and independently certified R_Σ(1..3)=(1,7,23). The theorem is theirs; the catch and the audit are ours.
Read the report ↗The 3/7 upper bound is NOT new to us: a public Star Fleet Math bundle (14 Jul 2026, starfleetmath.com) states it with a Lean 4 formalization of the same four-projection proof. We independently reconstructed the finite argument, audited the Lean sources (no sorries; full Mathlib rebuild not run), and tightened the rounding trivially — so no priority claim, matching the report's own stance. The genuinely new bit is the lower-bound transfer from Kominers 2607.10431 → (1/e−o(1))log n, which the live page omits.
Read the report ↗Bae's arXiv:2604.23784 (April; claims #684) rests on Lemma 18, which is false: a counterexample built in the paper's own definitions, deterministic checker green, the A_p definition and θ-condition matched verbatim against the source. The unbounded-limsup corollary falls with it. A note to the tracker / the author is the next step — Patrick's call.
Read the report ↗In 1961–62 Erdős and Prachar proved that p_n/n decreases at a positive proportion of indices n and asked whether it also increases at a positive proportion. This is Erdős problem #968. Since p_n/n < p_{n+1}/(n+1) says exactly that the gap p_{n+1} − p_n exceeds p_n/n, which is about log p_n − 1, the question asks for a positive proportion of prime gaps of at least roughly average size. The best unconditional threshold we know of was a positive proportion of gaps above 0.579·log p (Bazzanella, Languasco and Zaccagnini, 2010). On the problem's thread Terence Tao derived the answer from the Riemann hypothesis plus a pair-correlation estimate, and called the question close to the limit of current technology. OpenAI's 6 October release claims much more: for every fixed C, a positive proportion of gaps exceed C·log p. The proof averages over starting points with a weight built from smooth divisor sums over the second of two adjacent intervals of length λ·log X. Alternating signs between neighbouring dimensions make the weighted number of primes in that interval as small as wanted, while the first interval keeps its share. A bounded-multiplicity count then turns empty intervals into distinct gaps. Our main reading seat, an AI (Claude Opus 5.5), read all five sections line by line and found no gap; three further hostile AI seats, two on the mathematics and one on the sources, found none either. OpenAI's Lean proof (56 modules, 22,533 lines) replays on our machine with the standard axioms and a matching statement. It proves the Siegel–Walfisz and Bombieri–Vinogradov theorems along the way; Mathlib has neither, and the paper assumes Bombieri–Vinogradov. A kernel-checked bridge of ours carries the result to a verbatim copy of Formal Conjectures' erdos_968, which uses a different indexing and a different definition of lower density. Our own sieve to 2.3·10¹⁰ finds p_n/n increasing at between 39.7% and 42.1% of indices at all ten checkpoints from 10⁶ to 10⁹; a second implementation matches it exactly at 10⁶, 10⁷, 10⁸ and 10⁹. Nothing in the theorem is ours.
CLOSEDFULL WRITE-UPIn 1981 Ajtai, Erdős, Komlós and Szemerédi asked whether every K_r-free graph with n vertices and average degree t has an independent set of size at least c_r·n·log t/t. Ajtai, Komlós and Szemerédi had just proved this for triangle-free graphs. This is Erdős problem #802. The 1981 paper's own bound had log log t in place of log t, and Shearer's 1995 bound n log t/(t log log t) had stood since. OpenAI's 6 October release claims the conjecture for every r ≥ 4. The proof chooses vertex weights that maximize an entropy-minus-edge-mass potential, deletes closed neighbourhoods one at a time, and needs only that the weighted triangle mass is at most a constant times the edge mass. Clique exclusion enters once, through random multipliers that keep each weight in expectation. Fed into the maximizer's variational inequality, they bound the weighted edge mass between any two vertex sets of bounded weight, and a separate theorem turns that bound into the triangle estimate by splitting vertices along random walks inside their neighbourhoods. We read all six sections line by line and found no gap. Hostile AI referee seats on §2 with §6, on §§3–5, on the Lean against the paper, and on the sources found none either; the two on the mathematics logged eight exposition notes between them. OpenAI's Lean proof of the comparator's theorem (31 modules) replays on our machine with the standard axioms and a matching statement. A kernel-checked bridge of ours carries it to a verbatim copy of Formal Conjectures' erdos_802, which is still marked open and asks for more: every r, and no lower bound on the average degree. Nothing in the theorem is ours.
CLOSEDFULL WRITE-UPLet V(x) count the distinct values of Euler's φ up to x. Erdős asked whether V(2x)/V(x) → 2 and whether V(x) has an asymptotic formula; Erdős and Hall had asked whether V(cx)/V(x) → c. Ford (1998) knew V(x) only up to a bounded factor. OpenAI's preprint (dated 25 September, released 6 October) proves V(x) ~ (x/log x)·G_m·A(θ), an explicit scale times a bounded positive coefficient of a phase θ, and with it V(cx)/V(x) → c for every c > 0. Its Lean proof, 809 modules that also prove Ford's order of magnitude in the paper's form V(x) ≍ (x/log x)·G_m, replays on our machine with the standard axioms and statements that match its comparator files exactly. Our bridge derives from it verbatim copies of Formal Conjectures' statements. Two hostile AI referee seats, reading §§2–7 (the whole proof) between them, found no false or unjustified step; a third checked the introduction's citations and the other sources, and a fourth attacked our own additions. Part (i) was not first proved publicly by OpenAI: a Lean proof of exactly Formal Conjectures' statement, by the solver JenW1N on conjectures.io, was verified there on 14 September and published on 16 September. Ours, first: the bridge, and counts of V(x) to 10⁹ (by two independent methods up to 10⁸) that agree with every published value we found. Second, a check that the explicit scale is Ford's up to a bounded factor, and a consequence of the theorem the paper does not state, found with seat O: Ford's unknown bounded factor becomes a continuous periodic function of 2C₀(log₃x − log₄x), so the coefficient A is continuous but not constant. Third, a search for the seeds that decide the least-preimage question (for every k at once, that question is Erdős #51): none for k = 3 below 10⁹, where the largest ℓ(d)/d is 2.0434.
CLOSEDFULL WRITE-UPLet N(b) be the largest number of distinct unit fractions, all with denominators at least 2, that some a/b with 1 ≤ a < b needs. In 1950 Erdős proved log log b ≪ N(b) ≪ log b/log log b and asked whether N(b) ≪ log log b; Vose improved the upper bound to √(log b) in 1985, and in September 2026 van Doorn, with GPT-6 Astra Pro, reached (log log b)². This is Erdős problem #304. OpenAI's 6 October release proves the conjecture. Its route is a descent. After O(log log b) greedy steps the remainder is A/C with C in a fixed exponential range. The paper then builds one auxiliary denominator M from products of primes near (log b)¹⁰⁰ and shows that almost every fraction u/(MC) with u below a fixed height has an expansion of length O(log log b). Each step peels off one unit fraction 1/((M/t)z), with t a divisor of M chosen so that the leftover numerator is small, and a uniform divisor moment with Hölder's inequality keeps the exceptional numerators sparse at every level. A scaled copy of A·M is then the sum of two good numerators. The same paper settles the order of the double logarithm in two neighbouring problems: the number F(k) of k-term expansions of 1 (#148) and the least integer v(k) ≥ 2 that is never a denominator in one (#293) both have log log of order k. Four AI seats found no gap: three hostile referees (the upper bound in §§2–5, the corollaries in §§6–8, and the sources) and one seat reading the Lean against the paper and the problems. Bloom and van Doorn, whose exposition simplifies the proof, write that they “have not yet read” §§3–5 in detail; our upper-bound seat read them closely. OpenAI's Lean has two separate developments, 348 modules in all, which we replayed with the standard axioms and matching statements. Our kernel-checked bridges carry the results to verbatim copies of Formal Conjectures' statements for #304 and of its Konyagin-form bound for #148, and to a statement for #293, which FC does not yet have. A dependency walk of ours shows that the Lean proves the paper's §8 slope by a route the paper does not print. Nothing in the theorems is ours.
CLOSEDFULL WRITE-UPA finite point set A is Ramsey if, for every number of colours, some Euclidean space is so large that every colouring of it contains a one-coloured congruent copy of A. Erdős asked which sets these are. In 1973 Erdős, Graham, Montgomery, Rothschild, Spencer and Straus showed they lie on a sphere; Graham conjectured the converse, and Leader, Russell and Walters conjectured instead that they are exactly the subsets of finite transitive sets. On 20 September Pálvölgyi, with a proof written by ChatGPT, refuted Graham's conjecture with seven points on a circle. OpenAI's preprint of 23 September (released 6 October) gives an exact test: A is Ramsey if and only if a certain matrix exists over the ring F ⊗ F, where F is the field generated by A's coordinates. Four AI seats briefed to refute it found nothing wrong, and neither did our own line-by-line read. OpenAI's Lean (65 modules) compiles here on the three standard axioms, and its seven statements match their comparator files. Ours: a Lean refutation of Formal Conjectures' "graham" statement, which FC still tags open, a Lean proof of its "spherical" statement, and a Lean proof of its main set equality with an explicit answer built from OpenAI's test. With an independently written procedure that decides the test when the coordinates involve one transcendental number, we also found that the smallest non-Ramsey subsets of OpenAI's twelve points have eight points. One of them is a square and a rectangle inscribed in one circle. None of this has been reviewed by a human expert.
CLOSEDFULL WRITE-UPErdős asked whether the least solution of φ(n) = a can exceed a by an unbounded factor. Writing ℓ(a) for that least solution, ℓ(a)/a = ∏ p/(p−1) over the primes dividing ℓ(a), so the question is whether least preimages can carry ever more small primes. Tao expects not; Erdős, in 1979, hoped for something that would imply yes. Ours, first, is an elementary barrier theorem, extending Carmichael's 1907 observation about powers of 2 and Fermat primes. Take a finite set S of primes closed under p ↦ the prime factors of p−1. If ℓ(a)/a stayed below ∏ p/(p−1) over S, there would be infinitely many primes q with every prime factor of q−1 in S. So a negative answer to #51 would give, for some fixed y, infinitely many primes p with p−1 y-smooth, which is not known for any fixed y (for y = 3 these are the Pierpont primes). Ratios below 3 everywhere would give infinitely many Pierpont primes. And if no totient has ℓ(d) > 3d (the case OpenAI's totient preprint leaves open), there are infinitely many primes of the form 2^α3^β5^γ + 1. Second, why the theorem's family does not produce large ratios in practice. We computed the least preimage of every 3-smooth totient 2^X3^Y with X ≤ 120 and 1 ≤ Y ≤ 80 exactly, by two methods: none exceeds 2 + 10⁻²⁰, against a ceiling of 3, because the Pierpont primes the theorem asks for are there. On the theorem's own diagonals the least preimage is one to three such primes. Third, the ratio splits as T·W, with T ≤ 2 coming from powers of 2 and Fermat primes, so #51 asks whether W is unbounded; up to 10⁹ the largest W is 1.584. Fourth, our July chain re-checked by an independent program: 2.044975 at a ≈ 1.8·10¹⁶, the largest ratio we know (the published record search stops at 1.2·10¹¹ with 2.043447). The problem stays open.
PARTIALFULL WRITE-UPErdős asked whether R(s,k) ≫ k^(s−1)/(log k)^c for some c; Bradač answered yes in June with c = 2s − 4, and the problem page records it as resolved — nothing here closes it again. Two OpenAI preprints released on 6 October claim much more for s ≥ 5: the log power is s − 2 + o(1), the Ajtai–Komlós–Szemerédi upper bound's own power, so the exponent is determined. Both come with Lean proofs (858 modules). We rebuilt every module from source on our machine, printed only the three standard axioms for both main theorems, matched both statements to OpenAI's comparator challenges, and re-checked both import closures with leanchecker --fresh. The library states its construction for every dimension d ≥ 3, not Paper B's d ≥ 5 (Paper A is the single case d = 4); a verbatim copy of OpenAI's assembly with 6 ≤ s relaxed to 4 ≤ s (the hypothesis is used only for side conditions) gives r(4,t) = t³/(log t)^(2+o(1)), past Mattheus–Verstraëte's t³/(log t)⁴, on the standard axioms. Chen (11 October) and Lin–Zhang (13 October) had derived that r(4,t) statement on paper, taking OpenAI's s ≥ 5 theorem as an input. A bridge, also kernel-checked, carries the library to Formal Conjectures' own statement of #986 at every s ≥ 4. Six AI referee seats read the papers and the Lean and found no gap in what they read; three were cut off before finishing, and parts of the s = 5 paper went unread.
CLOSEDFULL WRITE-UPErdős, Faudree, Rousseau and Schelp conjectured in 1978 that R(C_m, K_n) = (m−1)(n−1)+1 for all m ≥ n; in its standard form, with n ≥ 3 and (3,3) excepted, it is Erdős problem #551. Keevash, Long and Skokan proved it in 2021 for m ≥ C log n / log log n. That settles every large n but leaves finitely many pairs, and since their C is not explicit, not even the list of open pairs was known; Terence Tao noted on the problem page in September 2025 that the problem was decidable but still open. OpenAI's 6 October release claims all of it. The proof takes a minimal counterexample, finds a clique of order at least max{3, ⌊(m−1)/2⌋}, rules out cliques of order 9 or more by hand, and reduces the rest to 3,099 finite patterns of paths between clique vertices; two Python programs and, by a different encoding, a Lean proof each exclude them all. We read §§2–9 line by line and found no gap; two hostile AI referee seats on the mathematics (the t ≥ 9 argument, and the finite stage with its code) and one on the sources agreed. Our own enumerator reproduces the 3,099 patterns, both checkers re-run clean, and the Lean proof of the comparator's theorem (182 modules) replays on our machine with the standard axioms and a matching statement. A kernel-checked bridge of ours carries OpenAI's theorem to a verbatim copy of Formal Conjectures' erdos_551, which is still marked open there, with a pull request to close it waiting on a checked formal proof. Nothing in the theorem is ours.
CLOSEDFULL WRITE-UPBorsuk asked in 1933 (Erdős #505) whether every set of diameter 1 in ℝⁿ is a union of n + 1 sets of smaller diameter. Kahn and Kalai answered no in 1993 for every n > 2014. Since then the smallest known failing dimension has come down to 64 (Jenrich–Brouwer 2014; the problem page still says 64) and then to 63 (Grinsztajn 2026, a finite set). OpenAI's 6 October release claims nine. Its set is X = {uuᵀ : u a unit vector in ℝ⁴}, which lies in the nine-dimensional space of trace-one symmetric 4×4 matrices; no ten sets of diameter below √2 cover it. The construction is Kalai's: he proposed the projector sets of ℝⁿ as candidate counterexamples in 2011 and 2015, for n large enough to reach dimensions above about 70. OpenAI's Lean proof (269 modules) replays on our machine with the standard axioms, and its statement matches OpenAI's comparator challenge. Three AI referee seats and our own reading of §§5–6 found only exposition problems in the paper. The kernel-checked proof takes a different route from the printed one in its degree theory and in most of the finite step, so the replay and the reading each check something the other does not. For covers by caps the result already follows from Walkup's 1970 bound on triangulations of ℝP³, so the new step is arbitrary sets. Ours: an exact certificate that eleven sets do cover X, which with OpenAI's theorem makes its Borsuk number exactly 11 (reported numerically, without a certificate, on 10 October); an independent SAT check of the finite step with a verified certificate, which shows the step needs less than the paper uses; and a kernel-checked bridge to the statement in Formal Conjectures, whose current link proves a differently worded theorem. The problem itself was answered no in 1993.
CLOSEDFULL WRITE-UPErdős and Gallai conjectured that every n-vertex graph is the edge-disjoint union of O(n) cycles and single edges; the record at the end of September was Bucić–Montgomery's O(n log* n). Three claimed proofs of the full conjecture then appeared: Ryan Coffey's (public 1 October with a 152-page paper and a Lean proof of Formal Conjectures' exact statement), Jaehoon Kim's (arXiv, 6 October, 22 pages in v2, no Lean) and OpenAI's (released 6 October, 32 pages, with a Lean proof of its own formulation). We compiled both Lean proofs on our machine: each depends only on the three standard axioms, leanchecker --fresh accepts each whole import closure, wrong-shape controls are rejected and planted-sorry controls show sorryAx. Formal Conjectures marks the problem solved with a link to OpenAI's proof, which proves an equivalent but different statement; we wrote the transport and kernel-checked it against a verbatim copy of Formal Conjectures' statement, while Coffey's proof is checked against Formal Conjectures' own. Hostile AI referee seats found no gap in the parts they checked: OpenAI's paper (expository fixes), Coffey's load-bearing chain (his §3–§5 device lemmas only at statement level; the Lean carries them) and Kim's v2, read line by line (nothing above exposition; the cited Bucić–Montgomery results not re-proved). No independent human check of any of the three is on record.
CLOSEDFULL WRITE-UPErdős asked for the best c such that every set of n reals in which any four points determine at least five distinct distances contains a Sidon set of size cn. The published bounds were 9/17 ≤ c ≤ 4/7 (Ma–Tang, February 2026). A reader's submission takes the 11-point set O = {0,49,75,83,98,101,117,119,121,159,269} and nests copies of it inside itself with φ(x) = 101 + 18x/269, which carries O's ends 0 and 269 onto two of its own interior points. We refereed it: for every depth K the set has 11 + 9K points, keeps the four-points-five-distances property, and its largest Sidon subset has exactly 7 + 5K points — so c ≤ 5/9. The finite facts are checked exhaustively (every 4-subset through 119 points, every additive relation through depth 12), the Sidon numbers by two independent solvers through 83 points, and a short 269-adic argument shows no relation can span more than ten levels, which turns the depth-12 census into a statement about every depth. One set suffices to beat 4/7: depth 6, 65 points, Sidon number 37. A hostile referee found four gaps in our first write-up, all fixable and fixed. The construction is the reader's; the interval is now 9/17 ≤ c ≤ 5/9.
PARTIALFULL WRITE-UPOur July census certified 4,094 of the 4,095 nonempty seeds in [12] eventually periodic under Dickson's rule and left one, E = {1,4,8,10,11,12}, with a bounded wall (no period ≤ 20,000 beginning by 479,993). This entry pushes the exact greedy extension to 10⁸ — two bitset implementations and a set-based reference agree, the July SHA-256 through 500,000 is reproduced, the recurrence is re-checked from scratch on windows of the output — and finds no gap period ≤ 3,905,308 terms beginning at or before term 7,810,617 (a = 49,993,396). The structure that stops every certificate is then measured: the power spectrum sits on the multiples of one frequency g = 0.2845919362 (the two largest peaks satisfy 4f₁ + 9f₂ ≡ 0 — a relation the hostile referee caught after a first draft had called the set two-frequency), the near-periods 130, 253, 636, 1,655 are g's convergent denominators, and under the phase x ↦ {xg} the set is a five-arc window to within a few dozen exceptions per million — the integers on the arcs' cores are in, those in the deep complement are out, and only edge zones a tenth of the circle wide are decided by the arithmetic, which is where the sumset gets completed and where a proof would have to work. No residue rail exists at any m ≤ 400; a SAT census shows Li's shield is infeasible for every doubling cycle of three or more rails (and every union containing one) at every modulus below 49, with the surviving two-rail controllers periodic in every test. One step up, a certificate census of every seed with largest element 13 and 14 (12,288 seeds; 12,282 certify, zero tool errors) finds six distinct resisting sequences in all, every one of the same kind. Whether E is a counterexample is open; we conjecture it is.
PARTIALFULL WRITE-UPErdős offered $500 for a proof or disproof that the two-colour van der Waerden number satisfies W(k)^(1/k) → ∞; the page's best lower bound was exponential — Kozik–Shabanov's c·2^k, and since August Campos–Fox–Schildkraut's k·2^(k−1), which settles the weaker W(k)/2^k question and not this one. OpenAI's 23 September 2026 paper proves W_r(k) > k^(ck⌊log₂ r⌋) with c = 10⁻⁵ for every r ≥ 2 and all k past one absolute threshold: a two-colouring of a cyclic group of size k^(ck) built from an outer local-lemma colouring of coordinate labels, a balanced-or-globally-affine dichotomy driven by a dilation that makes every short rational period vanish, and a sparse Bernoulli perturbation keyed on Behrend-type norm bands, then a digit product for every number of colours. Its catalogued Lean (115 modules) compiled on our machine in 430 s; under --trust=0 the kernel printed only propext, Classical.choice and Quot.sound on the theorem, on kthRoot_tendsto — the page's sentence at r = 2 — and on the cyclic witness; the statement and its four definitions are byte-identical to the comparator; a wrong-shape control is rejected and a planted sorry reports sorryAx. Seven tool-equipped seats, each briefed to refute, read the paper's own TeX line by line and found no gap in the proof of Theorem 1.1 — only that the Lean proves the §3 and §6 counts in weaker forms than the paper prints, that the key-multiplicity bound is really 2, and that the sizes are astronomical: the bound beats 2^k only past k ≈ 10^30103 and the threshold sits near 10^45. The question is answered yes; the improve-the-bounds half of the page stays open. The theorem is OpenAI's; the audit and the replay are ours.
CLOSEDFULL WRITE-UPErdős asked whether every finite projective plane has a blocking set meeting every line in at most C points, for one constant C. The floor is 4 for every order ≥ 5 and is met at q = 5, 7, 8, 9, 11 and all 3^r. The q = 11 optimum — returned by two solvers here and by Illés–Pisinger's 1997 annealing, whose posted set is the same configuration — is Klein's (21₄) configuration: the 21 involution centres of a PSL(2,7) inside PGL(3,11), all coordinate permutations of (1,0,0), (1,±1,0), (1,±1,±6). At q = 13 no blocking set with at most four points per line is invariant under any of the symmetric reductions we tried, plain SAT finds none, and the 1997 annealing stopped at 5; a cube campaign for an UNSAT certificate is running and reported on this page when it lands. Illés–Pisinger's posted 24-point set (and our own 34-point one) gives c(PG(2,13)) ≤ 5.
PARTIALFULL WRITE-UPErdős asked ($500) whether n points in the plane always contain one that determines n^(1−o(1)) distinct distances to the others — the pinned form of the distinct-distances problem — and the page's best bound was Katz–Tardos's n^0.864. OpenAI's 23 September 2026 paper proves that for every fixed s > 0 the fraction of ordered pairs whose distance repeats n^s times at its source tends to zero, hence all but o(n) points see at least n^(1−ε) distinct distances for every ε, with no rate. Its catalogued Lean proof (48 modules) compiled on our machine in 508 s and the kernel printed only propext, Classical.choice and Quot.sound on main, pins and exists_pin_eventually; the statement matches the comparator byte for byte and the page's question, written from scratch, closes from the Lean in four lines; cert-machine's independent comparator run agrees on two kernels. Eight tool-equipped seats (seven on the proof, one on sources), each briefed to refute, read it line by line and found no gap — only that the range s > 0.1359 already followed from Katz–Tardos, that the Lean takes a different route through §2, §6 and §7, and that the argument proves a more general Theorem G that no source the seats searched states. First question answered yes; n/√log n stays open. The theorem is OpenAI's; the audit and the replay are ours.
CLOSEDFULL WRITE-UPErdős asked for the chromatic number of the plane — the Hadwiger–Nelson problem — and the page's bounds were 5 ≤ χ ≤ 7, the five from de Grey's 2018 graph. OpenAI's 23 September 2026 paper proves that every five-colouring of the plane, with no regularity assumption on the colour classes, has two points at distance one of the same colour, so χ is 6 or 7. The proof transfers any colouring at all to a weak measurable one, for every number of colours (through a new rigidity theorem for rotation-invariant laws on the dual of the algebraic plane — false for the rational plane, which is exactly why Payne's two-colourable rational graph is no counterexample; the seats found the sentence that separates the two cases), and then excludes five weak-measurable labels by continua of common exclusion ending in a rational placement of the Moser spindle. Its catalogued Lean proof — 70 modules including the Furstenberg–Zimmer tower — compiled on our machine in 1,263 s with 0 errors; under --trust=0 #print axioms reported only propext, Classical.choice and Quot.sound for the theorem and, transitively, everything it rests on; the comparator's statement, copied verbatim, is proved by the solution's theorem; the page's lower-bound statement closes from it in three forms written from scratch; the six-colour and distance-2 controls fail. Seven tool-equipped seats, each briefed to refute, between them covered all 62 pages — each scoped seat line by line through its stretch — and found no gap — only exposition notes, an uncited 2014 precursor for the weak-measurable definition, and a theorem the paper leaves unstated: the measurable chromatic number of the plane is also at least 6, the first move past Falconer since 1981 if Theorem 1.4 holds. Five other parties record machine checks of the Lean; no human had refereed the paper. The exact value stays open. The theorem is OpenAI's; the audit, the replay and the statement probes are ours.
LIVEFULL WRITE-UPErdős–Graham's #341 extends a finite seed by the least integer that is not a sum of two earlier terms, equal terms allowed, and asks whether the gaps are eventually periodic; Zhiheng Li's August seed answered no (refereed here on 13 October). The comments to Problem 7 of Green's list pose the same question for Queneau's variant, where the two earlier terms must be distinct, and mark both open. Li's seed is periodic under that variant. We show the variant fails too: replacing 77 by 56 in his seed — A = {1, 2, 3, 5, 7, 13, 22, 27, 28, 32, 36, 40, 47, 48, 52, 56, 63, 71, 81, 89, 97} — gives a greedy extension whose gaps are not eventually periodic under Queneau's rule, and not under Dickson's either (a 21-element seed outside Li's infinite family). The proof is Li's shield mod 49 with a new controller whose three rails are switched by the blocks [8^k+1, 2·8^k], [4·8^k, 8·8^k], [2·8^k, 4·8^k], every identity checked by hand; the controller was found by letting the greedy itself run on all 27 seeds of this shape. An independent greedy on the integers matches the closed form at every integer to 10^7.
PARTIALFULL WRITE-UPIs there m coprime to 6 with 2^k 3^l m + 1 composite for all k, l ≥ 0? The only known mechanism is a two-dimensional covering system — one coset of the lattice L_p per prime, all together covering ℤ² — possibly helped by the algebraic factorisations of a perfect power. Our 12 October entry excluded every pure covering system of period up to 65,520 by a forced overlap of 5 and 7 and exact maxima over seven-prime blocks, and left the five computed pools of periods 110880–720720 (60 to 99 primes) standing. Project the covering onto the lines of a direction (a standard restriction lemma): a prime reaches one residue class of lines and covers those with intensity 1/ord_p(2^a 3^b), so every line must receive intensity ≥ 1. Along the lines of slope 1, 6 ≡ 1 mod 5 makes 5 cover a quarter of the lines completely and 7 cover half of a third of them; on the half of the lines neither touches, the rest of the pool can average at most a closed-form sum B — and B < 1 for every pool computed: ≤ 0.834 at every period ≤ 65,520 with density ≥ 1, and 0.849, 0.868, 0.854, 0.884, 0.937 at the five open pools. Exact integer programs sharpen several of these. No pure covering system has period ≤ 65,520 or dividing any of the five (the perfect-power variant stays open at 55440 and 65520, as before). Found with a hostile referee's help; the problem stays open.
PARTIALFULL WRITE-UPColour the plane with no red unit pair; how long a blue unit-spaced progression can be avoided? The page says 6 ≤ k ≤ 10⁷; the forum knows Currier–Mody–Xie–Zhang's June 2026 proof of k ≤ 6330. We recomputed every constant of that proof (hexagonal cells of diameter 1, |z(D)| = 18, p = 1/19, Janson exponent 0.015571, Milnor–Thom 2⁴·5¹⁶·m⁸): it holds, and parametrising the progression by its three real degrees of freedom instead of four gives k ≤ 4917 from the identical argument. Both known lower bounds — EGMRSS's E² → (ℓ₂, ℓ₄) and Tsaturian's E² → (ℓ₂, ℓ₅) — become exact finite certificates: 15 and 69 points of the unit triangular lattice and its Moser-angle rotations, with a red origin and (for ℓ₅) one WLOG blue point, each clause verified exactly in ℚ(√3, √11), minimal, closed by three solvers and drat-trim. The same apparatus at ℓ₆ found no certificate and refuted nothing: the instances that could decide the matched question are thousands of times harder and ran out their time caps undecided (one radius-3 instance found an ℓ₆-free patch in 5,439 s; nothing refuted the route).
LIVEFULL WRITE-UPErdős asked whether every infinite set A ⊂ ℝ is avoided by some set of positive measure — no x + sA inside it, s ≠ 0. Finite sets are never avoided (Steinhaus); slowly decaying sequences are (Falconer, Eigen); the live page says the question is open for A = {1, 1/2, 1/4, …}, Problem 94 on Ben Green's list. OpenAI's 6 October release carries two anonymous preprints: a 16-page proof for the dyadic sequence (25 September, formalized in Lean) and a 13-page proof for every geometric sequence {qⁿ}, 0 < q < 1 (5 October, paper only). We read both. The construction routes every point of the line through a finite tree of random fair-bit tables and spends its measure budget exactly once at the leaf, so the number of independent chances to hit a translated point grows without the density growing; the scale count stays local to one block of the tree. Four tool-equipped seats with disjoint scopes, each briefed to refute, verified every lemma line by line and found only cosmetic items; exact-arithmetic simulations of the paper's own construction match its exact probability formula and the negative controls fail. OpenAI's own Lean proof of the dyadic case — Green's Problem 94 exactly — was kernel-replayed on our machine today: all 75 modules compiled against Mathlib's pinned commit, the main theorem depends only on the three standard axioms, its statement is byte-identical to the challenge, the wrong-shape control fails, and leanchecker --fresh over the whole import closure exited 0. The general conjecture — every infinite set — stays open; what is settled, pending human review, is the family of geometric progressions, the special case the problem page names as open.
LIVEFULL WRITE-UPThe unit distance problem: Erdős's n^{1+o(1)} conjecture was disproved by an OpenAI construction in May; the upper bound has been n^{4/3} since 1984, and the page explains why — Valtr's metric attains it, so any improvement must use the Euclidean circle. OpenAI's 23 September preprint claims u(n) = O(n^{4/3−δ}) by complexifying the circle into the hyperbola zw = 1, so unit edges have reciprocal jumps whose heights across the places of a number field cannot stay bounded (a 3-neighbour determinant) and cannot vary either (entropy prediction, a product-formula score budget, and a Kummer-theory obstruction in an ultraproduct). Nine tool-equipped seats found no gap; two exposition defects named. A 40-file Lean proof is in the release, absent from its own catalogue; our kernel replay is green (standard axioms, statement matched to the challenge; leanchecker --fresh green over the whole closure). #90 stays disproved; the exponent now sits between 1.036 and, if this holds, 4/3 − δ.
LIVEFULL WRITE-UPEvery set of 15 nonzero integers contains a sum-free 7-subset, and {1,2,3,4,5,6,8,9,10,18,100,200,10000,20000,1000000} shows 7 is sharp, so F*(15) = 7 against Bourgain's guaranteed 6. The all-positive case and the sign patterns with 1–3 negatives fell to z3 directly (2–8.6 h each); the four hardest patterns timed out at 12 h and were closed by splitting each on where its two outermost negatives sit among the positives — 244 cubes, every one UNSAT, 70.5 CPU-hours — and a flat 36-hour run per pattern then confirmed each. The asymptotic question stays open.
PARTIALFULL WRITE-UPTwo days ago the exact table of Erdős's h(n) reached n = 27 and asked where its blocks-of-eight pattern would break. It breaks at once: a 29-element set with no admissible 6-subset, found by a pure-SAT search over [−26,26] and re-checked exhaustively, gives h(28) = h(29) = 5 where ⌊(n+20)/8⌋ predicted 6. The positive-reals lemma that was running to prove h(28) ≥ 6 is false — a 14-set of positive integers with no admissible 6-subset exists in [1,17], and a 15-set in [1,24] — so the next lower bound reachable by that route is h(32) ≥ 6, now running. A 43-set with no admissible 7-subset gives h(n) ≤ 6 for n ≤ 43.
PARTIALFULL WRITE-UPThe second game of #778: Alice colours one edge of K_n, Bob then colours two, and Bob wins only if his largest clique is strictly larger than hers; Erdős asked whether Bob wins for every n > 3. The proof-claims tab carries one claim, Didin and Pimenov's three-page potential argument (August 2026) that Bob wins for all n ≥ 3^158, with a Lean 4 development. We refereed it with three Opus seats (a hostile referee who re-derived every step and ran an exact-arithmetic instrument over 2,444 games with zero violations, a Lean seat that matched the formal statement to the literal game, and a judgment seat that quantified what the method can and cannot reach) and kernel-replayed the Lean on our box: standard axioms. Below the threshold everything was open past n = 7, where our July computation stopped. Today n = 8 falls: Bob wins on K₈, by exact backward induction over isomorphism classes (824,319 nodes), with a 210,325-position strategy certificate checked by two nauty-based checkers (Python and C++, each independent of the solver), reproduced by the same engine with reversed move ordering and with its cutoffs disabled, and by our July engine (separate code, Python, 41½ minutes). At n = 8 the triangle-avoidance route that carried 4 ≤ n ≤ 7 appears to break: our engine finds that Alice wins the (1:2) triangle game on K₈ (one engine — the July engine's run was stopped at 15 GB — not certificate-checked), so this is the first value where Bob has to win the clique game as such. Later the same day n = 9 fell too: Bob wins on K₉ — 313,106,283 nodes, 44,100,927 positions up to isomorphism, 77 minutes on one core — with a 20,802,845-position strategy certificate accepted by a second independent checker (C++ on nauty, written for the purpose because the first one would have needed about forty hours; it reproduces the first checker's n = 8 counts exactly and rejects the same deleted, fabricated and mass-swapped certificates; it reads Bob certificates only, so it refuses the flipped-winner one as out of scope). The first open value is now n = 10.
PARTIALFULL WRITE-UPErdős–Graham's version of Dickson's 1934 question: extend a finite set greedily by the least integer that is not a sum of two earlier terms (equal terms allowed) — are the gaps always eventually periodic? The proof-claims tab has carried a disproof since 9 August 2026: Zhiheng Li, using GPT-5.6 Sol, writes down the greedy extension of A = {1, 2, 3, 5, 7, 13, 22, 27, 28, 32, 36, 40, 47, 48, 52, 63, 71, 77, 81, 89, 97} in closed form — five full residue classes mod 49, three 'rail' classes 7/14/28 switched on and off at quotients taken from blocks [4·8^k, 8·8^k) and their two sumset-complements — proves it obeys the rule by a finite residue check, and reads aperiodicity off the geometric blocks. Formal Conjectures marks the problem solved; the page and the teorth database still say open. We refereed it: our own greedy from the seed agrees with his set at every integer up to 10⁷ (1,224,508 terms, 0 mismatches, mutation controls fail), the residue shield and the three controller identities recompute, the Lean (v4.33.0-rc1, tagged Mathlib) builds in 8,663 jobs with the final theorem and the p ≥ 18 family theorem on exactly propext/Classical.choice/Quot.sound, the statement is the problem's negation definition by definition and bridges to the Formal Conjectures statement by a kernel check, and a hostile seat found no gap. Also ours: under Queneau's distinct-index variant — the other convention Green lists — the same seed is eventually periodic (gap period 693, certified), so that variant stays open; and {1, 4, 9, 16, 25} is periodic within 87 terms under either rule, not 'thousands'. The counterexample is Li's; the board now says NO.
CLOSEDFULL WRITE-UPErdős asked how many colours [N] needs so that every four-term progression sees at least three of them. The page records N^{log 3/log 22+o(1)} ≈ N^{0.355} above and exp(c(log N)^{1/9}) below. The proof-claims tab now carries two preprints: Rio Itabe (14 July 2026) with N^{1/3+o(1)} and a Lean 4 development, and Shi–Dong (arXiv 2607.20752, 22 July) with N^{1/4+o(1)} — both from the same new idea, a base-p carry control plus the cubic field norm F_{p³} → F_p, which handles the one two-colour pattern (ABBA) that Behrend-style colourings are not known to. We read both proofs lemma by lemma, re-implemented Shi–Dong's colouring twice (norm as z^{1+p+p²} in Python, as a determinant in C) and enumerated every 4-AP in ℤ/p⁴ℤ for p = 5, 7, 11 (and in C for p = 13) — none symmetrically coloured, palette within 27p, three controls fire — sampled their k = 6 colouring of ℤ/7⁹ℤ (2.2·10⁸ progressions, none symmetric), brute-forced Itabe's three labels, kernel-replayed his Lean (standard axioms, statement matched to the page's h), and sent four hostile Opus seats at the papers. All four seats and the host read agree: nothing fatal, no gap that reaches a theorem; two one-line gaps in Shi–Dong's written proofs (a step-exactly-p carry case Lemma 2.1 does not cover; a false reason at x = M/2 in Lemma 5.3, true conclusion), a stale 'strongest previously known' sentence, and, on priority, that Itabe's manuscript was public eight days before Shi–Dong's v1, which did not cite it; v2 cites it as 'a concurrent result'. Itabe's cubic factor is, up to the choice of basis, their k = 4 colouring restricted to pℤ/p⁴ℤ. Ours: the referee report, the checks, and exact values we could not find written down anywhere — h(N) = 3, 4, 5, 6 on 4–12, 13–22, 23–35, 36–51. The problem stays open.
LIVEFULL WRITE-UPThe $250 sparse-halves problem asks whether every triangle-free graph has ⌊n/2⌋ vertices spanning at most n²/50 edges; Razborov's 27/1024 (2021) is the best bound in print. The proof-claims tab carries one claim: Amir Sarid (Aug 2026), β ≤ 131/5000 = 0.0262, conditional on Balogh–Clemen–Lidický's max-cut Theorem 2(a), with a Lean development taking that theorem as a hypothesis. We refereed it: every lemma recomputed by hand and by a second route (exact rationals, randomised tests with mutation controls), the C₄ flag certificate re-established by an independent exact verifier and probed on 14,651 small graphs, the Lean source audited and then kernel-replayed on our box (Mathlib v4.30.0, standard axioms only, statement match, sorry and wrong-shape negative controls). Verdict: HOLDS AS READ, label (b) — but the theorem it rests on is a six-page EuroComb 2021 extended abstract whose proof sketch does not separately cover the part he uses, with no public certificate, so the unconditional record stays 27/1024. Not ours; the problem stays open. Also: two errors on the live problem page, staged for Patrick.
LIVEFULL WRITE-UPErdős asked whether every polynomial of degree n with coefficients ±1 has maximum modulus at least (1+c)√n on the unit circle; Parseval gives √(n+1) for free and the question was whether real signs are forced a fixed fraction above it. OpenAI's 23 September 2026 paper proves the minimum over all sign choices is (1+o(1))√N at every large length N — the limit is 1, not the ≈1.27 that Odlyzko's exhaustive search had suggested — and its Lean states precisely that. On our machine the 28-module proof compiled from the pinned sources and the kernel printed only propext, Classical.choice and Quot.sound on a statement matched byte-for-byte to the challenge; seven tool-equipped referee seats, briefed to refute, found no gap in the formalized paper or in the two-sided ultraflat one. Answer: NO. The theorem is OpenAI's; the audit and the replay are ours.
CLOSEDFULL WRITE-UPIs there m coprime to 6 with 2^k 3^l m + 1 composite for all k, l ≥ 0? The only known way to build such an m is a covering system of primes, each prime killing one coset of a lattice of index e_p = |⟨2,3⟩ mod p|. Two readers of erdosproblems.com had shown the density condition Σ 1/e_p ≥ 1 and that local search plateaus near 72%. We prove the cosets of 5 and 7 overlap in density exactly 1/24 whatever m is, so a covering using both needs Σ 1/e_p ≥ 25/24 — which no prime pool of period ≤ 5040 reaches (the 5040 pool is 143/140) — and, from exact maximum-union computations on blocks of up to seven primes, that no covering system has period N for any N ≤ 65,520 (each N against its own complete pool; 30,000 when this entry first went up); any covering whose period is a multiple of 720 needs pool density ≥ 1.16625. The perfect-power factorisations do not rescue the small periods either. Open.
PARTIALFULL WRITE-UPThird entry on #151 today, second straight-reasoning pass on the k = 10 wall (n = R(3,10) ∈ {40,41}). T0: for every n, a graph with β(G) < H(n) arrows (K3,K3) in edges — the red edges plus the lone edges of a good colouring form a triangle-free graph meeting every maximal clique; the morning's notes had this only for K4-free G. So every counterexample is a (3,3)-Ramsey graph and Bikov's theorems on minimal (3,3)-Ramsey graphs apply to its core. T6 (K4-free case): at most three 'exceptional' vertices, the core's degree-9 vertices are among them, and every other core vertex has core-link one of four of Bikov's seven graphs and neighbourhood one of the three (3,4;8)-graphs (a containment table, two implementations). T7: by Seymour's 1974 theorem a minimal (3,3)-Ramsey graph has at least as many triangles as edges, which leaves the core at most 7 units of link deficit (5 by computation): it is either 8-regular and locally the Wagner graph at every vertex, or has two adjacent degree-9 vertices and is locally Wagner at all but ≤ 10 (8). Same afternoon: a classification search (five classical controls, hostile referee) finds exactly two connected locally-Wagner graphs of any order — the Paley graph P(17) and a vertex-transitive graph on 21 vertices, the Fano-plane flag graph, which refutes a 2019 thesis classification — and neither arrows, so the 8-regular case is impossible: a K4-free counterexample's core has exactly two adjacent vertices of degree 9. Not closed; the case-(b) search is running.
PARTIALFULL WRITE-UPFollow-up to this morning's #151 entry. The public n ≤ 39 proof stops at k = H(n) = 10, where n = R(3,10) ∈ {40,41}. A straight-reasoning run on a loaded box (no solver campaign) extends the claim's local bound to whole independent sets and derives what a minimum counterexample must be: β = 9 exactly, Δ, α ≤ 9, δ ≥ 4 or 5, ω ≤ 7 or 6, every neighbourhood cheap to hit (a full census of admissible links), every independent set expensive (a price table), every far vertex hanging a maximal clique off a maximum-degree neighbourhood, and — unless α ≤ 5 — lone edges dominating every maximum independent set. No contradiction yet. For K4-free graphs the question is exactly whether a K4-free graph of maximum degree ≤ 9 can arrow (K3,K3) in edges; no bounded-degree K4-free Folkman graph is known.
PARTIALFULL WRITE-UPErdős–Gallai asked whether every n-vertex graph has a clique transversal of size n − H(n), H(n) the Ramsey independence number. Thinking from the definitions, this run found the exact-bound route (a triangle-free spanning subgraph meeting every maximal clique) and its wall: for K4-free graphs that subgraph exists iff the triangle hypergraph has Property B, so edge-Folkman graphs are exactly where it fails. The same lemma turns out to be the new step of a proof claim filed on 28 September covering all n ≤ 39; we read that claim line by line and ran a blind referee on it — it holds as read. Asymptotically the problem has been settled since 2021 (JMRS); only the exact Ramsey form is open, and any K4-free counterexample must be a sparse Folkman graph.
PARTIALFULL WRITE-UPErdős's $5000 question — does a divergent reciprocal sum force arithmetic progressions of every length? — was open for every k ≥ 4; the best bound (Leng–Sah–Sawhney 2024) fell short of the dyadic-summability threshold. OpenAI's 23 September 2026 paper claims r_k(N) ≤ C_k·N·exp(−c_k(log N)^ε_k) for every k in 198 machine-written pages; the Lean it ships proves a different, weaker bound, exp(−c(log log N)^(1+η)), that is nonetheless past the threshold and so proves the reciprocal-sum statement itself — exactly the question on the problem page — in a 4,774-file, 1.1-million-line proof we audited at source (no sorry, no axioms, no escape hatches; statement identical to the challenge) and replayed on our own machine — 13,697 jobs built from the pinned sources in 14.3 hours, and under --trust=0 the kernel printed exactly propext, Classical.choice and Quot.sound for the reciprocal-sum theorem, the quantitative bound and their conjunction, with the challenge statement identical to the solution's under pp.all; nobody else had reported building it with a log (Formal Conjectures marked the problem solved on source inspection). Seven hostile seats read the paper in disjoint scopes against the sources of its two external inputs: holds as read, seven of seven — no mathematical gap, no constant cycle, the exponent iteration-independent by the paper's own argument, about forty exposition notes. Not ours — but our kernel has now said so, and #3 joins the problems closed in the literature.
CLOSEDFULL WRITE-UPErdős asked in 1946 how few distinct distances n points in ℝ^d can determine; the grid shows n^(2/d) is the most one can hope for, and eighty years of work got the exponent to 2/3−o(1) in ℝ³ (Tidor–Yu–Zakharov, August 2026) and to 2/d − 2/(d(d+2)) in general (Solymosi–Vu). OpenAI's 23 September 2026 paper claims c_d·n^(2/d) for every d ≥ 3 — the conjecture with the constant factor, stronger than the n^(2/d−o(1)) the problem page asks for — in 103 machine-written pages with no Lean in the release. We read it in twelve sectioned hostile seats briefed to refute, checked every fetchable citation at source, read the step the chain hinged on (Proposition 4.3) ourselves, and found that the same third party who formalized OpenAI's Hindman and hypercube proofs has published a 757-file Lean 4 proof of exactly this statement — taking a weaker planar route that, it turns out, the paper never needed — and our own from-source kernel replay of it printed exactly the three standard axioms, and the fresh re-check of Mathlib's cached object files exited 0 after 7,919 s; #1083 is closed in the literature. Verdict on the paper as written: holds as read, twelve seats out of twelve — no mathematical gap, no hidden rate on δ or M/A, no cycle among the constants, about ninety exposition notes; and the one Guth–Katz input the proof cannot do without is the k ≥ 3 incidence bound, not the planar n/log n it advertises.
CLOSEDFULL WRITE-UPErdős asked whether φ(m) = n can have more than n^(1−ε) solutions for infinitely many n; he proved n^c, Baker–Harman and Lichtman pushed c to 0.7156, and the conjecture C = 1 reduces to a count of primes p with p − 1 having no prime factor above p^δ, a barrier of sieve theory below δ ≈ 0.284. OpenAI's 24 September 2026 paper claims x^(1−o(1)) such primes for every δ, hence the conjecture, in 68 machine-written pages with no Lean for anything but the last page. We read it in ten sectioned hostile seats briefed to refute, checked every cited theorem against its source, had the parity-breaking step's exact identity coded independently twice and made it fail on purpose, and tried nine counterexamples to its shifted-correlation theorem. Verdict on the paper as written: holds as read, ten seats out of ten — no mathematical gap, a sketched bijection, one unwritten inequality, and a theorem that proves more than it claims. Unverified by any human or any kernel.
CONFIRMEDFULL WRITE-UPf(n) is the largest m such that every n-set of integers contains a sum-free m-subset. Bourgain gives f ≥ (n+2)/3; our August report showed every exact value through n = 14 matches that bound except n = 13, where positive sets force 6 but mixed-sign sets were unresolved. Today the six remaining sign patterns are all UNSAT over the reals (z3 on two encodings, cvc5 as a second engine): F*(13) = 6, the first n where the truth exceeds Bourgain's ⌈(n+2)/3⌉. The asymptotic question is untouched.
PARTIALFULL WRITE-UPErdős's h(n): the largest k such that every n-set of integers contains a k-set in which equal subset sums force equal subset sizes. Our August report pinned h(n) through n=19 and named one finite lemma as the wall. Two unrelated SMT solvers now prove it — every ten distinct positive reals contain an admissible five-subset, and nine do not — and a new 25-element obstruction closes the other side: h(n) = 5 for every n from 20 to 27. The asymptotics stay where Straus and Choi left them.
PARTIALFULL WRITE-UPBurr and Erdős asked in 1975 whether the Ramsey number of the n-dimensional cube is bounded by a constant times its number of vertices. Fifty years of upper bounds got the exponent from 2n+o(n) down to (2−c)n; OpenAI's 23 September 2026 paper claims the whole conjecture, R(Q_n) ≤ C·2^n, in 172 machine-written pages with no Lean. We read it in nine sectioned hostile seats briefed to refute, checked every cited theorem against its source, found that the same third party who formalized OpenAI's Hindman proof has published a 752-file Lean 4 proof of exactly the Formal Conjectures statement — and our own from-source kernel replay of it printed the three standard axioms, and the fresh re-check of Mathlib's cached object files exited 0 after 7,773 s. The problem is closed. Verdict on the paper as written: holds as read, nine seats out of nine — no mathematical gap, one exposition gap (Lemma 18.1), one step taken on trust (§9.1), and no hidden rate on N/2^n anywhere.
CLOSEDFULL WRITE-UPHindman asked whether every finite colouring of the positive integers contains arbitrarily large finite sets whose nonempty subset sums and subset products all share one colour. Alweiss proved it over the rationals; over the integers it was open until OpenAI's 23 September 2026 paper claimed it. We read all 70 pages, checked every cited theorem against its current source, ran a hostile machine referee over the whole chain, and found that a third party (Yao Xu) has since written a 6-megabyte Lean 4 proof following the paper, sorry-free, with OpenAI's own library supplying the hardest half. Four sectioned hostile referee seats read the paper as written and found no gap — every cited theorem says what the paper says it says — and our own from-source kernel replay of the Lean proof printed the three standard axioms. The problem is closed.
CLOSEDFULL WRITE-UPk(3,4) is the least order forcing, in every oriented graph, an independent triple or a transitive 4-tournament. The literature had 21 ≤ k(3,4) ≤ 25; a 20-vertex witness was known and our August run left six order-21 SAT instances unresolved. A lossless case split — a vertex's neighbourhoods have only 1, 7 and 1 isomorphism types on 8, 7 and 7 vertices — turns order 21 into 346 small cases, every one UNSAT with a drat-trim-verified proof (72 of them after lossless symmetry breaking). So k(3,4) = 21. The general k(n,m) question is untouched.
PARTIALFULL WRITE-UPExact exhaustive certificates now give f(1..7)=1,2,2,3,3,4,4 and F(1..7)=1,2,2,3,4,5,7; both asymptotic Erdős-Ulam questions remain open.
PARTIALLive-page status is OPEN with 0 formally listed claimed proofs, but VPendyala is marked “Currently working on this problem” and the live discussion contains Venkata Pendyala’s 18 June 2026 claim of a
SKIPPEDExact exhaustive computation extends A389182 with \(F(101)=\cdots=F(106)=16\), \(F(107)=\cdots=F(116)=17\), \(F(117)=\cdots=F(134)=18\), \(F(135)=\cdots=F(152)=19\), and \(F(153)=20\); the asymptotic
PARTIALexact s(k,n) for all n<=37 plus a proof that Pikhurko's 1.863949... bound is optimal within every mode-by-mode Fourier/triangle-inequality certificate; the asymptotic problem remains open.
PARTIALProved the exact ceiling–Golomb-ruler equivalence and, with dependency-free exhaustive searches and an independent C++ audit, determined f(N) exactly for every N<=120; independently audited the unrefe
PARTIALExhaustive maximum-degree CNFs and complete canonical censuses give h(18)=5 at computer-assisted solver-assertion level; the asymptotic problem remains open.
PROVEDProblem #773 asks whether the largest Sidon subset of the first N positive squares has size N^(1-o(1)); that asymptotic problem remains open. Conditional on the full published exact OEIS A390813 prefix through N=68, frozen exhaustive searches prove the next three values: a(69)=32, a(70)=33, and a(71)=33. The new upper search at 71 covers seven disjoint cubes and 114,296,406 recursive states; the size-33 lower witness is a direct integer certificate. An independent definition-level audit reconstructs every collision support and checks the witness, cube cover, and counters. This extends a finite table, not the exponent in Erdős's question.
PARTIALFULL WRITE-UP(d) Exact exhaustive certificates now give \(f_3(N)\) through \(N=125\), with \(f_3(N)=14\) for \(101\leq N\leq107\), 15 for \(108\leq N\leq124\), and 16 at \(N=125\); the asymptotic problem remains o
PARTIALproved an elementary finite-to-infinite extension and exact two-row thresholds through L_40=509, including L_11,...,L_40=101,107,127,131,149,167,173,191,197,211,241,251,257,271,281,307,313,347,361,367
PARTIALExact strict-pair values F(1),...,F(61) are exhaustively verified with standalone checkers and independent SAT controls; the asymptotic constant and higher-r bound remain open, with the missing unifor
PARTIALExact exhaustive certificates prove f(N)=14,16,18,21,23,24,26,28,32,32,34,38,39,41,44,45,48,52,52 for N=8,...,26 in Koizumi's equivalent lattice model; an all-N construction also rules out any one O(N
PARTIALExact dynamics produce arbitrarily long constant nonzero gap transients of either sign (then an absorbing zero tail), refuting uniform small-gap fixed-window strategies, while finite total negative ga
PARTIALA complete computer-assisted census proves Tuza's inequality for every simple graph on at most ten vertices; the unrestricted Erdős problem remains open.
PARTIALExact independent computations now give \(M_k(9)=(0,18,21,27,28,30,32,36)\), extending the complete frontier through nine vertices; the asymptotic problem remains open at the same triangle-removal sca
PARTIALAn exact formula counts p-subgroups of S_n by order when every nontrivial orbit has size p. One exact order already attains the known n^2/16 leading exponent, with an explicit n log n term, and the same restricted family has a discrete order limit law. This refines a known construction without solving the global problem.
PARTIALFULL WRITE-UPAn exact reconstruction gives 49,910,538,480 groups across all orders below 2,048. A published exact subclass count of 1,774,274,116,992,170 at order 2,048 already exceeds that total, certifying the stronger conjecture at m=11. The general problem remains open.
PARTIALFULL WRITE-UPBrutman and Toledano computed the four-node optimum numerically in 1997. We give an independently checkable exact global certificate: the unique nodes are {-1,-sqrt(y),sqrt(y),1}, where 21y^3+9y^2+3y-1=0, and the minimum is algebraic of degree three. This finite result does not settle the asymptotic problem, and no priority claim is made for the exact formulas.
PARTIALFULL WRITE-UPA July 2026 preprint strengthens the known affirmative limsup result to a finite-order class-B entire function. Separately, a polynomial whose nonzero exponents span d-m has at most d-m maximum-modulus points on every circle, sharply. The liminf question remains open.
PARTIALFULL WRITE-UPThe asymptotic problem remains open. A second exact computation adds ten transition indices after 1500 and proves f(N) exactly through N=2000. A custom verifier and official PMC agree on all 201 new eligible last-vertex decisions.
PARTIALFULL WRITE-UPComplete factorization gives F(115)=115 and F(116)=117. From there, one fresh proven-prime divisor of each partition number p(n) certifies F(n)>=n+1 for every 116<=n<=10,100. The 100 new steps extend the published finite frontier; the eventual inequality remains open.
PARTIALFULL WRITE-UPErdős and Surányi's 1959 paper defined a constant cₙ — how long an interval, as a multiple of max(A), guarantees n picks whose product is divisible by ∏A — proved c₂=1 and c₃=√2, and reported no bounds in general for 67 years. Rounds 1–7 pinned c₄ through c₁₀ at 2 and proved cₙ ≥ 2 for every n ≥ 4. Round 8 proves c₁₁=2. A maximum-defect Hall reduction leaves finite eleven-edge two-, three-, and four-defect kernels. The new difficulty is placing outside-edge representatives and repair multiples jointly: multi-repair obstructions collapse by short progression lemmas, while the sole singleton obstruction is removed by a gcd/lcm exchange. Rado's theorem handles K₃,₄−e, and robust support blocks survive the aligned injection's two-adic matching while avoiding the midpoint. This determines cₙ through n=11 and improves the general bound to cₙ≤2n/11+14/11. Independent hostile audits cleared the integrated proof. The famous g(n)≤2n conjecture stays open and untouched.
LIVEFULL WRITE-UPProblem #617 asks whether every r-coloring of K_(r^2+1) has an (r+1)-vertex clique missing a color. That remains open beyond the known cases r=3,4. We prove an exact auxiliary theorem for every r>=2: the fewest edges in an (r^2+1)-vertex graph with neither a clique nor an independent set of size r+1 is (r^3-r^2+4r-2)/2. Thus every color class in a hypothetical counterexample has at least 59 edges at r=5. The five bounds total 295 of 325 edges, leaving a real 30-edge compatibility gap, so this is a structural frontier rather than a solve.
PARTIALFULL WRITE-UPAn unreviewed public candidate proof gives R(C₄,K₁,₃₉)=46, closing the first bracketed entry in the finite table. Our hostile audit reconstructed the 45-vertex lower witness, the universal 46-vertex reduction, the exact spectral moments, and a rational dual certificate, and found the finite proof valid without relying on the candidate's uncertified SAT logs. This is an independently audited candidate result, not yet peer reviewed and not a solution of the asymptotic Erdős problem.
PARTIALFULL WRITE-UPProblem #295 asks whether the shortest unit-fraction expansion above a denominator cutoff eventually exceeds (e−1)N by an unbounded amount. That asymptotic problem remains open. Round 1 closed k(17)=32. Round 2 proved the rigorous computational bounds 33≤k(18)≤35; on 11 October a reader, Kyunghan Bae, cut the upper bound to 34 with an explicit 34-term certificate we verified exactly, so now 33≤k(18)≤34. The harmonic maximum excludes at most 30 terms; exact GMP and Fraction recursions independently execute the same proved exhaustive search and exclude 31 and 32. A transparent four-for-one unit-fraction surgery on the k(17) identity supplied our 35 terms beginning at 18; the reader's five-for-four surgery on it gives 34. Full reproduction, sanitizer, serial, concurrency, and hostile source audits passed. On 13 October we added his certificate upper bounds k(19) ≤ 36, k(20) ≤ 38, k(21) ≤ 39 (re-verified three ways). Whether k(18) is 33 or 34 remains open, as does Erdős's asymptotic question.
PARTIALFULL WRITE-UPAn exhaustive scan from zero finds the next record gap between sums of two squares at 133,858,454,292..133,858,454,404. Its difference is 112, so 111 consecutive interior integers are nonrepresentable. Independent scans and a direct factor certificate prove it is the first new record and remains maximal through 200 billion; the asymptotic problem remains open.
PARTIALFULL WRITE-UPThe published diameter-22,270 integral heptagon has no distinct eighth point whose seven distances to it are positive integers at most 96,000. Three exact exhaustive traversals and a big-integer metric audit certify the bounded nonextension. This concerns one fixed heptagon and gives no lower bound for arbitrary eight-point sets.
PARTIALFULL WRITE-UPThree exact enumerations give theta_4(13)=949,812,334 and theta_4(14)=9,471,574,188. The known table through n=12 is independently reproduced. This is a finite counting extension only; the singly infinite permutation problem remains open.
PARTIALFULL WRITE-UPA preprint posted on 10 August proves that adjoining any point outside the affine hull of a finite Euclidean Ramsey set preserves the Ramsey property. This resolves Ivan-Leader-Walters Conjecture 8 and extends their earlier subsoluble-base result to arbitrary Ramsey bases. An independent proof audit found no gap; the full characterization in Problem 174 remains open.
PARTIALFULL WRITE-UPA reproducible floating-MIP computation extends the finite-value table for corner-free subsets of the first 3-smooth numbers from prefix 5,000 through 5,020, adding twelve OEIS A004059 rows. Two SCIP formulations agree; no proof-carrying certificate was obtained, and the density and irrationality questions remain open.
PARTIALFULL WRITE-UPDoes a maximal Sidon subset of {1,...,N} exist with size O(N^(1/3))? The asymptotic problem remains open, and Rounds 1–2 explain why the extra log in Ruzsa's construction is structural for random lifts. Rounds 3–5 close the next exact finite frontier: a(66)=a(67)=6, a(n)=7 for every 68≤n≤101, and a(n)=8 for every 102≤n≤136. Complete enumerations cover normalized Sidon sets through seven marks, while explicit maximal sets certify every upper bound. This extends OEIS A382397 from 65 through 136 without changing the parent problem's asymptotic record.
LIVEFULL WRITE-UPA July 2026 strong-clique bound, specialized at maximum degree 4, proves the exact value 20; the C5 two-blowup attains it. This is a literature-derived partial. The strong chromatic maximum remains between 20 and 21, so Problem 149 is still open.
PARTIALFULL WRITE-UPClemen, Dumitrescu, and Liu proved that every convexly positioned planar n-point set, n>=5, has a non-diameter distance occurring at most n times. Their proof combines the Altman-Fishburn equality classification with a short pair count. This is a published partial; the arbitrary-set and growth questions remain open.
PARTIALFULL WRITE-UPAn explicit subgraph of the 9-dimensional cube has 1,531 edges and no 4-cycle, proving ex(Q9,C4)>=1,531. Exhaustive face and common-neighbour checks certify the graph. It improves our earlier 1,506-edge certificate by 25 edges and the identified external 1,505-edge certificate by 26; this remains a finite lower bound. UPDATE 19 October: superseded and corrected — a reader's explicit 1,532-edge graph is verified (submission c3u7pu), and the number 1,532 was already reported in 1994 by Marinari, Parisi and Ritort as a fully frustrated nine-dimensional ground-state energy, with no configuration published. This page's 'improves the public record' was true of published edge lists only.
PARTIALFULL WRITE-UP[a+d] Explicitly proved \(f_d(n)\ge\binom{d+1}{\binom n2-1}+1\), certified \(f_1(4)=7\), and reduced the fixed-\(n\) subexponential question equivalently to distinct-distance subsets on \((d-1)\)-sphe
PARTIALLive page status OPEN (0 claimed proofs), but “Currently working on this problem” lists dumbprime; stopped before attempting mathematics to avoid colliding with the current worker.
SKIPPEDLive page status OPEN; it lists 1 claimed proof—a partial proof claimed by Ákos Dúcz and Dániel Varga, submitted 2026-07-29, asserting a finite planar unit-distance graph with independence ratio stric
SKIPPEDThe authoritative live page is OPEN with 0 claimed proofs, but lists Hotdingus as currently working on problem #1049, so the required no-collision rule applies.
SKIPPEDLive page status OPEN (accessed 2026-07-31), with 0 claimed proofs, but “Currently working on this problem: epistemologist”; mandatory non-collision stop.
SKIPPEDThe live page is FALSIFIABLE/open with 0 claimed proofs, but lists “Currently working on this problem: ogroth” (accessed 2026-07-31), so the mandatory no-collision rule applies.
SKIPPEDReduced the live question exactly to compact capacity-one sets, proved an exact Chebyshev lemniscate-area formula with sharp constant \(C_*=1.579155688354179\ldots\), and isolated critical-value separ
PARTIALThe live page status is OPEN (0 formal claimed proofs; “Currently working” is None), but its comments contain a claimed and independently endorsed proof that \(\rho(f)\ge(\log 2)/n\) for every admissi
SKIPPEDThe live page is OPEN but lists 2 claimed proofs and names naprienko and danrobinson as “Currently working on this problem” (accessed 2026-07-31), so the mandatory no-duplication/no-collision rule for
SKIPPEDThe live page is OPEN (accessed 2026-07-31) and shows no current worker, but it lists 2 full proof claims—by Shouqiao Wang (submitted 2026-07-21) and Sangyoon Kwon (submitted 2026-07-23)—so the mandat
SKIPPEDThe live page is OPEN (0 formally logged claimed proofs; Currently working: None), but its discussion has a 27 Apr 2026 comment by Przemek Chojecki saying the problem “was claimed” in the linked prepr
SKIPPEDLIVE PAGE STATUS OPEN (0 formal claimed proofs; no current-worker or interested markers), but its 21–22 April 2026 discussion contains a claimed solution—arXiv:2604.18535 is said to give negative answ
SKIPPEDThe authoritative live page is OPEN but lists “1 claimed proof for this problem”—a full proof claimed by RayYoung, Keheng Zhu, and Yanping Luo, submitted 2026-07-15—so the mandatory no-duplication gat
SKIPPEDLive page status is OPEN, but it lists “1 claimed proof for this problem” (a full proof claimed by Eric Hou, submitted 2026-07-21); “Currently working on this problem” is None.
SKIPPEDproved a rigorous upper-constant improvement to \(1/(2\ln2)=0.7213475\ldots\) in base-2 normalization and exhaustively computed \(f(3),\ldots,f(9)=1,4,11,23,44,77,123\), but the limit and its value re
PARTIALLive page status is OPEN with 0 claimed proofs, but it lists “Currently working on this problem: SamKorsky” (accessed 2026-07-31); the mandatory collision rule therefore forbids an attempt.
SKIPPEDLive page status OPEN (last edited 11 May 2026); “Currently working on this problem” lists ligma and SamKorsky, so the no-collision rule requires stopping.
SKIPPEDLive page status is OPEN - $250, but it lists 2 full proof claims (QuietMethod and Liam Price) and names TheTorturedPoetsDepartment as currently working, so the mandatory no-duplication/no-collision r
SKIPPEDproved a strict Melchior/Bojanowski upper-bound improvement, exact grid formulas with a checker, and uniform lower bounds; the constants and limit existence for k>=4 remain open.
PARTIALThe live page status is “OPEN - $25” but it lists “2 claimed proofs for this problem” (with “Currently working on this problem: None”), so Step 0 requires no attempt.
SKIPPEDLive page status OPEN with 0 claimed proofs, but “Currently working on this problem” lists Ritvik_Nayak (accessed 2026-07-31), so the mandatory no-collision rule requires stopping.
SKIPPEDExact computer-assisted determination \(g(1),\ldots,g(9)=1,2,2,3,4,4,4,5,5\), with rational witnesses and a real nonrepresentability proof at \(n=8\); the verified asymptotic gap \(\Omega(\sqrt{n\log
PARTIALLive page status is `OPEN - $100`, but “Currently working on this problem” lists `MrLaine` (accessed 2026-07-31); per the collision rule, no attempt was made.
SKIPPEDThe live page status is OPEN, but it lists Sam_Petkov as “Currently working on this problem,” so an attempt would collide with a current worker.
SKIPPEDProved a uniform injective layer reduction, closed forms for the top three axis-support coefficients for every n, and independently certified exact n<=10 polynomials and strict two-sided bounds for di
PARTIALThe authoritative live page is OPEN with 0 claimed proofs, but it lists msawhney as “Currently working on this problem” (accessed 2026-07-31), so no mathematical attempt was made.
SKIPPEDLive page status is OPEN (0 formal claimed proofs; “Currently working” marker: None), but its April 2026 comments explicitly claim possible/complete solutions and state that Brayden Letwin is actively
SKIPPEDLive page status OPEN, but it lists 1 claimed proof (a full proof claimed by Rob Sneiderman, submitted 2026-07-21) and identifies lof310 as currently working on the problem.
SKIPPEDExplicitly constructed and verified an infinite-order, non-Fejér Fabry-gap entire function that assumes every value infinitely often; the universal problem reduces exactly to excluding zero-density Ta
PARTIALThe live page status is OPEN, but its discussion identifies current workers: on 5 June 2026 Przemek Chojecki said that he and Yuta were jointly preparing a paper collecting all arguments for Problem #
SKIPPEDAn explicit He–Tang-family entire function and independent Arb checker rigorously improve the known lower bound to B > 0.585078819674; the exact value remains open.
PARTIALProved the sharp-order bound for low 2-adic-level and quadratic-energy regimes and exactly certified all 4–6 term spectra through frequency 24; the general \(N^{1/2}\) conjecture remains open, with Be
PARTIALThe live page status is OPEN, but it lists 1 claimed proof and current workers dhyantailor, benk, and Qing_Hong (accessed 2026-07-31).
SKIPPEDProved from scratch the exact radius-one-disk values α(3)=3√3/4, α(4)=1, and α(5)=√(5(5−√5)/32), plus the sharp all-boundary formula β(n)=2 sin²(π/n) sin(2π/n); the asymptotic Erdős problem remains op
PARTIALUnder Elliott’s intended “not all collinear or concyclic” convention, \(f(7)=11\) is proved with an exact integer construction and a from-scratch lower bound; also \(12\leq f(8)\leq18\), with the exac
PARTIALLive page status is OPEN, but “Currently working on this problem” lists Lumantis (accessed 2026-07-29), so no attempt was made.
SKIPPEDLee--Pohoata--Zhu, arXiv:2607.05374v1, source-audited modulo the Hajir--Maire--Ramakrishna/Chebotarev tower input, proves \(P_2(n)<n^{1-c}\) for some \(c>0\) and all sufficiently large \(n\); the full
FOUNDThe problem remains open; dependency-free exhaustive computation and independent arithmetic audits now give the complete exact table \(g_3(N)\) for every \(1\le N\le191\), ending at \(g_3(191)=159\).
PARTIALproved the residue-vector and reflection reductions, exhaustively verified \(A(k)\), \(B(k)\), and greedy \(B\)-optimality for \(1\leq k\leq22\), and derived conditional liminf constants \(1/2\) and \
PARTIALLive page status is OPEN with 0 claimed proofs, but idrissbado is listed under “Currently working on this problem”; the mandatory collision rule therefore requires no attempt.
SKIPPEDLive page status OPEN; it lists 1 full proof claim by Jeff Pickhardt and Omniscience Research Agent (submitted 2026-07-28), so the mandatory no-duplication rule applies.
SKIPPEDThe live page status is OPEN, but it lists one claimed proof—a full proof claimed by Colin Snyder (submitted 2026-07-15)—and “Currently working on this problem” is None, so the task’s mandatory collis
SKIPPEDLive page status OPEN (accessed 2026-07-29), but “Currently working on this problem” lists DaPoWi; per the no-collision rule, no attempt was made.
SKIPPEDThe authoritative live page (accessed 2026-07-29) has status OPEN, 0 claimed proofs, and lists Shadow under “Currently working on this problem”; stopped to avoid colliding with a current worker.
SKIPPEDExplicitly proved the relation when \(\aleph_{\omega+1}\leq2^{\aleph_0}\), repaired and verified the current filter-tail lift, and reduced the remaining hard regime exactly to a ZFC free-cover/tail-fi
PARTIALLive page status OPEN (0 claimed proofs), but “Currently working on this problem” lists Sam_Petkov; stopped to avoid colliding with a current worker.
SKIPPED#1146 remains open; a counterexample must have vanishing simultaneous \(2^m3^n\)-boundary along density-minimizing prefixes, all eventually periodic competitors are excluded, and exact optimization gi
PARTIALProved the critical quadratic-window reduction and excluded every fixed-base digit complement; exhaustively computed the sharp balanced perfect-complement tail distortion for all 2<=m<=30, but the uni
PARTIALLive-page status is OPEN, but “Currently working on this problem” lists apiros3; per the collision rule, no attempt was made.
SKIPPEDproved no fixed-modulus obstruction and exactly certified the stated finite suffixes through \(10^7\) for \(r=3\) and \(10^8\) for \(4\le r\le8\); eventual coverage for every \(r\ge3\) remains open.
PARTIALProved the exact near-simplex band \(f_d(n)\) for \(n\le2d\) (including \(f_d(d+3)=\binom{d+3}{2}-3\) in every dimension), proved \(f_3(7)=15\), and corrected the live page's three-dimensional upper b
PARTIALLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists Tomodovodoo (accessed 2026-07-29); the mandatory collision-avoidance rule requires stopping.
SKIPPEDProved the canonical reduction and a uniform \(O(x/\log^2x)\) upper bound modulo the standard Selberg upper sieve; exactly enumerated 481,051 first-form and 1,021,854 second-form primes through \(10^8
PARTIALExact computational values f(n) are independently reproduced through n=200 (extending OEIS n=45..200), with f(200)=136 and an explicit checked witness; irrationality remains open and requires a unifor
PARTIALProved the exact powerful-core bijection, improved the general located exponent constant from log(3)/3 to log(2)/2 for every odd target, certified f(n)<=5 through 10^14 and f(n)<=1 for odd n through 1
PARTIAL[d] Exactly 646 Carmichael numbers occur up to \(10^9\), verified by two complete kernels and independent audits; [b] the asymptotic problem remains open, with accepted exponent \(0.3389\) and a unifo
PARTIALExact exhaustive computation finds only the five known unitary perfect numbers when every prime-power component is at most \(10^7\); any sixth has a component \(>10^7\), while full finiteness still re
PARTIALproved two uniform closed forms, an exact linear-excess regime modulo Győri's verified packing theorem, a sharp subquadratic estimate, an exact weighted-packing reduction, and the exhaustive table thr
PARTIAL\(h(n)=5\) for every \(34\le n\le40\) via an explicit five-chord family; the cases \(n=38,39,40\) extend the verified published exact table through \(n=37\), while the asymptotic problem remains open.
PROVEDproved the cited f-bounds invert to coefficients 1/2 and 2 (exposing an unsupported factor-two live-page bound), derived 33 <= h_3(6) <= 40 with an explicit fully rechecked upper witness, and reduced
PARTIAL[d] Exhaustive generation plus independently validated colouring certificates give \(f_4(11)=21\), \(f_4(12)=26\), \(f_4(13)=31\), and \(f_4(14)=36\); the general problem remains open.
PARTIALLive page status OPEN, but it lists 2 claimed proofs and current workers mchoi and Woett; per the collision/duplication gate, no attempt was made.
SKIPPEDLIVE PAGE STATUS OPEN (0 formal claimed proofs; “Currently working: None”), but its newest discussion comment (Liam Price, 30 Apr 2026) explicitly says “GPT-5.5 Pro claims a disproof to the first ques
SKIPPEDverified Tenenbaum's exact best general exponent, isolated the zero-density/Type-I–II barrier, recorded the June-2026 monic-cubic advance, and exactly certified \(F_{x^2+1}(n)\ge0.998112594359576\,n^2
PARTIALFor the irreducible cubic \(f(n)=n^3+2\), the \(d\le X\) contribution is rigorously \(2R X\log X\), the problem is reduced exactly to signed endpoint cancellation for \(X<d\le X^{3/2}\), \(R\) has an
PARTIALLive page status is OPEN, but it lists “1 claimed proof for this problem” (a partial proof claimed by KyungMin Han, submitted 2026-07-25 by Dogcake); “Currently working on this problem” is None.
SKIPPEDFGKMT plus \(x=p_k\) rigorously strengthens the cited lower bound to \(H(k)\gg k(\log k)^2\log_3k/\log_2k\); an independent exhaustive checker gives exact \(H(k)\) for \(k\leq14\), but the quadratic u
PARTIALverified and corrected the pre-jump count at the published \(10^{18}\)-range negative extremizer, certified exact decade extrema through \(10^7\), and reduced the RH-conditional \(1/4+\varepsilon\) ta
PARTIALProved, with a uniform exact bound and standalone verification, that every finite direct power \(A_5^r\) satisfies the Herzog–Schönheim conjecture; the general problem remains open.
PARTIALExact carry-factor reduction for all finite P, plus rigorous rational enclosures excluding denominators below 40–51 digits for all three-prime subsets of {2,3,5,7} (and an 18-digit bound for {2,3,5,7}
PARTIALLive page status OPEN, but it lists one full proof claim (Colin Snyder, submitted 2026-07-15, claiming the complete \(c>1\) result with a Lean 4/Mathlib formalisation); currently working and intereste
SKIPPEDproved simultaneous rationality with the sharper endpoint growth \(\liminf a_n^{1/(\sqrt{3/2})^n}>1\), exact target sums, a standalone checker, and a \(\sqrt{5/3}\) counting ceiling for the fixed-wind
PARTIALLive page status OPEN (0 claimed proofs), but “Currently working on this problem” lists daniel_e_ruiz_c and memeister27; mandatory no-collision stop.
SKIPPEDExact radical-support compression proved and a from-scratch rational verifier certifies the sharp bound \(M(n)\leq\sum_{p<n}1/p+1\) for every \(2\leq n\leq1000\); the uniform problem remains blocked b
PARTIAL[D] Every integer \(|n|\le10000\) except \(n=\pm1\) is explicitly ruled out for the always-squarefree variant by a prime-square witness with \(p\le1423\) and \(k\le250270\); within this range existenc
PARTIALExact finite compactness reduction proved; exhaustive checker certifies \(L_N\) through \(N=21\) and normalized minimax \(R_N\) through \(N=12\); the open asymptotic gap remains \(n^2/\log n\) infinit
PARTIALProved the critical-density/lower-energy hierarchy and the exact r=3 block-gluing reduction, and exhaustively certified the minimum cyclic three-basis energy for every modulus 2 through 41; the unreso
PARTIALreduced both questions to exact monotone finite Golomb-ruler profiles, proved the quadratic profile through n=21, and constructed and exactly verified a critical-log-envelope ruler through n=680; no a
PARTIALexact binomial-divisibility reduction proved and q(n,floor log n) exhaustively maximized for every 3<=n<e^21 (unique global maximum q=113), but no uniform constant saving is proved.
PARTIALreduced all uniformities to the exact \(r=3\) core, proved \(f_3(n,7,4)=3,4,6,7,9,12\) for \(7\le n\le12\) with a standalone exhaustive checker, and derived \(f_3(n,7,4)<\frac49n^2+2n\) modulo Gishbol
PARTIALProved the finite-clique hierarchy \(\chi(G)\le\beth_{q-3}(\kappa)\), obtained uniform \(>\kappa\) consequences at \(\beth_\omega(\kappa)\) and its successor-cover extension, reduced exact \(\kappa\)
PARTIALUnder GCH a uniform intersection bound below aleph_omega on any aleph_{omega+1}-sized subfamily forces the desired free set; every counterexample must have kappa full-sized rows, kappa popular points,
PARTIALUnder GCH the first arrow follows from Erdős–Rado, and relative to a huge cardinal GCH is consistent with all symmetric arrows through \(\omega_1^2+1\); the other two GCH arrows and uniformity for eve
PARTIALThe live problem remains open, but k=2 is a verified 1987 ZFC theorem; only k>=3 remains, with an exact triangle-free-cover/block-fusion reduction and a checked sharp C5 block obstruction.
PARTIALReduced #1144 exactly to a weighted squarefree positive-fluctuation lemma plus an \(L^2\)-controlled fractional error, proved the exact variance \((6/\pi^2)N\log N+O(N)\), and exhaustively verified al
PARTIALLive page status is OPEN - $500 with 0 claimed proofs, but “Currently working on this problem” lists VertRule, alansbor, old-bielefelder, and Shang_Yu_Chen (accessed 2026-07-28), so the mandatory no-c
SKIPPEDCertified sharp finite prefix bounds and an ordinary-additive extension of Mangerel's sparse-descent theorem; #1122 remains open at the average-gap and large-prime-spike barriers.
PARTIALThe Izotov candidate is re-proved Sierpiński; any finite cover is certified to require at least 686 primes, including one at least 376843822247957 with period at least 94210955561989, but unbounded le
PARTIALThe live page status is “OPEN (LEAN)”, but it lists “1 claimed proof” and JohanLand as “Currently working on this problem”; per the mandatory collision rule, no mathematical attempt was made.
SKIPPEDProved the self-contained no-pair bounds chi<=7,6,5 for odd girth 5,7,>=9, reducing any d(3,3)<=7 improvement to the C5-layer case; also verified a minimum-order 22-vertex witness for d(3,3)>=6.
PARTIALLive page status is OPEN, but it lists 1 partial claimed proof (Xiyu Hu/hxypqr, submitted 2026-07-23) and names hxypqr as currently working on the problem.
SKIPPEDLive page status OPEN, but comments dated 27–28 April 2026 link a proof and explicitly say that it claims a positive resolution of the second question (“Standard check found no issues”); stopping unde
SKIPPEDLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists lof310 (accessed 2026-07-28); stopped under the mandatory collision rule.
SKIPPEDProved exactly that $f_d(n)=\binom n2$ for $n\le d+1$, $f_d(d+2)=\binom{d+2}{2}-1$, and $f_d(d+k)=\binom{d+k}{2}-k$ for $3\le k\le d$ (with $f_d(d+3)=\binom{d+3}{2}-3$ also for $d=1,2$); the fixed-d a
PARTIALproved the conjectured exact value for all n<=15 (modulo the published g(k) classifications), proved D(A)>=ceil(n/3) modulo the planar diameter-graph theorem, and exactly ruled out the standard seven-
PARTIALExact EHS certificates give 120 members through 139 and isolate 140!+1; two independent scans give 21969 Pillai primes through 500000, but both density limits remain open.
PARTIALProved the elementary bound \(A(x)\leq(1+o(1))x/\log\log x\) and exactly certified \(A(200000000)=960\), including 241 values beyond the OEIS \(10^8\) table; the \(x^{o(1)}\) claim remains open at the
PARTIALproved an exact Wilson-reflection reduction and growing endpoint gap, derived a quantitative \((\log Y/\log\log Y)^{1/3}\) lower bound for every cutoff \(c>1/(1+9\log2)\), and independently verified e
PARTIALLIVE PAGE status OPEN with 0 claimed proofs, but “Currently working on this problem” lists jeffhino, so this run stopped before any mathematical attempt to avoid colliding with the current worker.
SKIPPEDLive page status is OPEN, but it lists jif and Vjeko_Kovac as currently working on problem #1054 (accessed 2026-07-28), so the mandatory no-collision rule requires stopping.
SKIPPEDProved that #1053 is exactly equivalent to divergence of the missing-prime sum in (11), classified all squarefree cases, and exhaustively verified the 14 multiply-perfect numbers through \(10^8\); the
PARTIALExact thresholds tau_1=1, tau_2=2, tau_3=6, the bound 9<=tau_4<=13, and a uniform O(2^n/n) deletion guarantee are verified; the fixed-positive-c problem remains open at a quantified cube-specific blow
PARTIALExhaustive computation gives h(3..10) = 6,8,9,10,12,13,14,16 with explicit certificates and an independent labeled cross-check through n=7; the asymptotic constant remains open.
PARTIALLive-page status is FALSIFIABLE; although its tracker says “0 claimed proofs” and “Currently working on this problem: None,” the discussion explicitly reports a claimed complete proof [Mi26] (with a l
SKIPPEDproved a positive-proportion \(L=10^{-10}(\log x)^2/\log\log x\) theorem modulo PPT, reduced all polylogarithmic lengths to GHP-diagonal coverage, and exactly certified \(A(10^9)=691\); the arbitrary-
PARTIALExact radical-kernel bijection proved; all solutions with odd member <= 2^64-1 and omega(odd) <= 3 are exhaustively classified (15 total), but infinitude remains equivalent to constructing infinitely
PARTIALThe live statement is literally false at \(p=2\); for the intended \(p>2\) version, \(G(p)\le211<p\) is independently certified for every prime \(p\le10^7\), two uniform subclasses are proved, and the
FOUNDLive page status on 2026-07-28 is FALSIFIABLE/open, but it lists 1 partial claimed proof (Scott Duke Kominers, submitted 2026-07-25) and current workers Sam_Petkov and skominers, so the mandatory no-d
SKIPPEDExhaustively proved for unordered k=4 representations that M_4(4)=199898912404 (four displayed prime quadruples) and M_4(5)>=5212641500689; the uniform unboundedness question remains open.
PARTIALExactly 75,670 of the first 100,000 values n^4+2 are certified squarefree, the local density is rigorously enclosed in [0.756683702608, 0.756684005282], and the open problem is reduced to the unproved
PARTIALLive page status is OPEN, but “Currently working on this problem” lists KoishiChan (accessed 2026-07-28).
SKIPPEDVia Laishram--Murty's published Grimm-function theorem, \(k(n)<n^{0.46}=n^{1/2-1/25}\) for all sufficiently large \(n\); the main \(\log k(n)\leq(\log n)^{1/2+o(1)}\) conjecture remains open, and the
PARTIALlive gate cleared; proved the quantitative binomial reduction, independently certified exact f(k) for k<=40 modulo the Carmichael-Lehmer cutoff, and constructed f(647134389)>=288; the uniform exponent
PARTIALThe authoritative live page is OPEN with no current worker, but it lists 2 claimed partial proofs (submitted 2026-07-15 and 2026-07-21), so the mandatory no-duplication gate applies.
SKIPPEDLIVE STATUS OPEN, but the 27 Apr 2026 discussion displays a claimed proof that \(h(n)=\Theta(n^{4/3})\), links its proof note, and reports that a standard check found no issues; no current worker is l
SKIPPEDproved an elementary equivalence with uniform size-biased fibre tightness, isolating the exact missing lemma, and exactly certified the sharp finite concentration function through \(x=5{,}000{,}000\);
PARTIALproved the exact regulator/drawdown reduction and certified the sharp bound \(0\le R(x)-x\le46{,}462\) for every integer \(x\le10^8\); the unresolved step is a uniform \(x^{1/4+o(1)}\) drawdown lemma.
PARTIALThe live page is OPEN with 0 claimed proofs but lists jif as “Currently working on this problem” (accessed 2026-07-28), so an attempt would collide with a current worker.
SKIPPEDexact start-anywhere computation gives maximum \(G_2\)-component size 100 and reproduces rooted moat data through \(D=10\); arbitrary bounded step remains open.
PARTIALExact rational verification proves 4.309405275 < m(3) < 4.3094055 and hence a literal finite-x counterexample below 4.3094055; the asymptotic Erdős/Shapiro question remains open.
PARTIALproved the full measurable case (with a perfect-set construction in the null case), repaired the Baire-case diagonal, and isolated the unresolved nonmeasurable/non-Baire regime; the unrestricted probl
PARTIALDual exhaustive computation proves the exact first starts through \(k=13\), the full step function \(F(x)\) for integer \(x\leq20{,}000{,}000\), and no length-14 run there; an elementary reduction iso
PARTIALLive page status OPEN (0 claimed proofs; “Currently working” marker: None), but the 18 March 2026 comment by Przemek Chojecki explicitly reports “on-going research work”; treated as a current worker,
SKIPPEDExact live-normalized computation gives a unique maximum h(n)=12 for n<=10^9 at n=472532614, with 12 factored witnesses and a reproducible verifier; the uniform polylogarithmic upper bound remains ope
PARTIALLive page status is OPEN, but “Currently working on this problem” lists Basile_Beyer_de_Ryke; stopped to avoid colliding with a current worker.
SKIPPED(d) no coprime 4-powerful solution \(a+b=c\) has \(\max(a,b)\leq10^{16}\), a 100-fold extension of the live bound; (a) the \(r\geq6\) infinite construction is independently proved, leaving global \(r=
PARTIALThe live page is OPEN with 0 claimed proofs, but it lists SkyYang as “Currently working on this problem” (accessed 2026-07-28), so the mandatory no-collision rule requires stopping without a mathemati
SKIPPEDExact certificate checks give only n={1} for 2^n-1 and n={3} for 2^n+1 through n=1000, and only n={4,5,7} for n!+1 and n={2} for n!-1 through n=139; LTE reduces each exponential branch to a uniform no
PARTIALelementary density-one bounds and exact \(n\le10^9\) tables for \(\ell=2,3\) are verified; the uniform first and third questions remain open at the explicit radical/simultaneous-powerful finiteness wa
PARTIALverified the July-2026 disproofs from explicit Odd/Witt constructions, certified h_3(4)>=71 and h_3(120)>=1,730,521, proved h_t(2)=2t+2, and isolated the remaining 253/225-versus-3/2 t=3 gap.
PARTIALLive page status OPEN; it lists current workers johnseibert19, fschumann, and aminb_el (with 0 claimed proofs, though one comment links a purported negative-answer preprint), so the mandatory no-colli
SKIPPEDLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists lof310 (accessed 2026-07-28), so the mandated collision-avoidance rule forbids an attempt.
SKIPPEDThe live page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists Svyable and satsun93 (accessed 2026-07-28); per the collision-avoidance gate, no mathematical attempt
SKIPPEDreduced #929 exactly to the primorial Jacobsthal bound \(Y(x)\le x^{1+o(1)}\), extracted the sharper proved bracket \(\sqrt{k}\ll S(k)\ll k\log_2k/(\log k\log_3k)\), and independently certified exact
PARTIALTao--Teräväinen gives the predicted ordinary density outside a zero-log-density set of scales; the supplied independently checked census is exact through 10^7, and the remaining fixed-shift all-scales
PARTIALproved an elementary O(sqrt(X)) candidate bound, classified the max-exponent-2 and two-prime slices, ruled out the standard infinite powerful recurrence beyond n=8, and independently verified exactly
PARTIALProved the uniform bound |h(n+1)-h(n)|<=1, gave an exact multiplicity/short-interval reduction and a three-way exact table through 10^9; the main asymptotic remains open at the stated harmonic-bin Poi
PARTIALVerified \(48\leq f(4)\leq67\); \(P_{67}\) is an explicit \(S_4\) tournament with a standalone exhaustive checker, while the asymptotic factor-\(n\) gap remains open.
PARTIALVerified \(m_{11}(5)=m_{12}(5)=66\), certified an edge-critical 51-edge 3-chromatic construction, and reduced the current \(32\le m(5)\le51\) gap to explicit finite set-cover windows; the asymptotic p
PARTIALproved the uniform bound f(2n)/f(n)>2 and a Bang–Zsigmondy weighted reduction, with an independent exact certificate through n=138; full divergence remains open.
PARTIALProved the necessary condition \(\sum_i1/n_i<\infty\) for the final scale question and an iff theorem for \(b_n\asymp n\log_2n\log_3n\,L(\log_2n)\), with an explicit independently checked primitive co
PARTIALExact smooth-centre reduction; all k=2 starts through 10^30 and k=3 starts through 10^12 classified, with last bad starts 4372 and 8615 respectively, but no uniform all-large-n lemma.
PARTIALexact interval reduction and exhaustive verification give \(v_0(n)\ge3\) for every \(14{,}433{,}527\le n\le50{,}000{,}000\), with exactly 2,112 smaller-prefix exceptions and last \(14{,}433{,}526\); e
PARTIALCorrected the live comment's off-by-one error, proved the exact baseline-plus-hypermatching reduction, and computationally verified \(G(n)=G_{\le2}(n)\) for every \(n\le5000\) plus exact samples throu
PARTIALLive page status OPEN; 0 claimed proofs; currently working on this problem: KStar (live page accessed 2026-07-28).
SKIPPEDThe live page is marked OPEN but lists 1 partial claimed proof (Liam Price using GPT-5.6 Sol Pro, submitted 2026-07-18) asserting that every infinite sum-free sequence satisfies \(\limsup_{n\to\infty}
SKIPPEDLive page status is OPEN (0 formal claimed proofs; no current worker), but its discussion contains DavidTurturean’s explicit 24 April 2026 claim of a total refutation for every k >= 3, updated 2 May 2
SKIPPEDproved the exact finite-union/LCM reduction, derived the rigorous lower bound \(\liminf d_t\log t\ge ce^{-\gamma}\) from Weingartner's theorem (forcing any asymptotic exponent \(c_2\le1\)), and indepe
PARTIALThe live page status is OPEN, but it lists sproutseeds as “Currently working on this problem”; the task forbids colliding with a current worker.
SKIPPEDThe live page status is DECIDABLE and states that Sawhney solved the problem for all sufficiently large \(N\); it lists 0 claimed proofs and no current worker.
SKIPPEDexact standard-library search certifies the finite extremal table \(f(N)\) for every \(1\leq N\leq70\), audits the elementary \(2/3\) bound and Freud construction, and isolates uncontrolled overlap am
PARTIALProved an exact divisor and Eisenstein-norm reduction, proved the conjectured polylog bound uniformly when the number of prime divisors p=1 (mod 3) is bounded (with a complete sharp classification whe
PARTIALclassified all possible bounded-\(\omega\) infinite families, reproduced the exact \(a=1\) list through seven prime factors, and isolated the unresolved unbounded-prime-support product-divisibility le
PARTIALexactly ten sharp-constant solutions \(n\leq10^9\), with a rigorous all-\(k\) checker and \((q,2q-1)\) prime-pair obstruction; #826 remains open at the near-critical \(\log\tau\) concentration lemma.
PARTIALLive page status is OPEN, but “Currently working on this problem” lists SamKorsky (accessed 2026-07-28); stopping to avoid colliding with a current worker.
SKIPPEDexact computer-assisted table \(l(1..10)=1,2,2,3,3,3,4,4,4,4\) and \(4\leq l(n)\leq5\) for \(11\leq n\leq14\); both asymptotic questions remain open.
PARTIALThe live page status is OPEN, but it lists “1 claimed proof for this problem” (and “Currently working on this problem: None”), triggering the mandatory no-duplication stop rule.
SKIPPEDLive page status is OPEN, but it lists 2 claimed proofs and a current worker (mthiim).
SKIPPEDexact 15-point obstruction/table and base-family classification verified; #774 remains equivalent to the unresolved uniform finite bound \(C(\delta)<\infty\).
PARTIALLive page status OPEN (0 claimed proofs), but “Currently working on this problem” lists Aron and ogroth; stopped to avoid colliding with current workers.
SKIPPEDLive page status is FALSIFIABLE/open (0 site-registered claimed proofs), but it lists jif as “Currently working on this problem” and its 28 Feb 2026 discussion also records arXiv:2410.13840 as a claim
SKIPPEDExact reproducible checks find no counterexample through n=14 and reduce the first open order n=25 to five SAT instances (maximum degree 13 through 17); the uniform conjecture remains open.
PARTIALLive page status OPEN with 0 claimed proofs, but “Currently working on this problem” lists ryin and boolean_matrix (accessed 2026-07-28); stopped before mathematics to avoid colliding with current wor
SKIPPEDRigorous modulo MRSTT Proposition 1.13, \(1/6\leq\liminf S(n)/\log\log n\leq\limsup S(n)/\log\log n\leq5/6\); exhaustive rational enclosures verified every \(100\leq n\leq10^7\), but the uniform recip
PARTIALverified Godsil--McKay through \(k=o(n^{6/7})\), proved a uniform permanent reduction/logarithmic bound, and independently computed exact reduced counts through \(n=6\) plus \(R(4,7)=1{,}293{,}216\);
PARTIALProved exactly that ex(n;K_{r,r}) equals C(n,2) for n<2r, C(2r,2)-r at n=2r, and C(2r+1,2)-(r+2) at n=2r+1, with exhaustive independent checks through r=4; the asymptotic question remains open.
PARTIALThe authoritative live statement is literally false for \(G=K_2\) since \(\operatorname{ex}(n,K_2)=0\); for the intended nondegenerate problem, the report proves an explicit infinite \(K_{2,t}\)-core
FOUNDProved the exact covering-design reduction, closed three near-diagonal finite regimes (including all ex_3(n,K_{n-2}^3)), and independently certified ex_3(n,K_4^3)=3,7,14,23,36,54 for n=4,...,9; no com
PARTIALThe live page (accessed 2026-07-28) has status FALSIFIABLE/open, lists 2 claimed partial proofs (one accepted by the site), and names conglu, Woett, and ster as currently working; the mandatory no-dup
SKIPPEDExact multiplier-cost reduction and independently verified sharp terminal-prime bounds for every prime-chain length 1 through 14; the uniform exceptional-path lemma needed for either asymptotic questi
PARTIALFor the strict live-page problem, \(G_2(n)\ll n^{2/3}\) follows from standard Erdős–Turán/van der Corput bounds, the exact remaining one-sided discrepancy condition is isolated, and exhaustive indepen
PARTIALIndependently certified \(Y(x)=h(\pi(x))-1\) and the exact values through \(x<43\) (in particular \(Y=73\) on \(41\le x<43\)); a fixed positive interval-sieve survivor bound (5.3) would prove \(Y=o(x^
PARTIALFor epsilon=1/10 and cutoff K=16, exactly 94 admissible n occur through Q_101+15 and all are at most 225, while the infinite problem reduces to an every-interval multiscale gap lemma not supplied by k
PARTIALLive page status OPEN, but it lists “1 claimed proof for this problem” (with “Currently working on this problem: None”), so the mandatory claimed-proof stop rule applies.
SKIPPEDElementary proof gives continuum many incongruent maximizers at n=6; modulo AMP25's exact u(n) theorem the same holds at n=8,9,12,21, while no uniform extremality-propagation lemma is known.
PARTIALExact \(f(n)\) for every \(3\le n\le21\), plus a verified \(C=2\) construction for every \(q^2\le n\le q^2+q+1\) with prime-power \(q\); the uniform problem remains blocked by gaps between projective-
PARTIALexact CRT reduction plus a complete k=2 enumeration proves the sharp cutoff q(n,2)<=199 for every 1<=n<68979941211663467981891685180356798343731381481900118460455756739438, with q(N,2)=211 at equality
PARTIALLive page status is OPEN, but it lists 1 claimed full proof (submitted by Colin Snyder on 2026-07-15); per the mandatory collision rule, no mathematical attempt was made.
SKIPPEDThe disjoint diagonal half-shift has an exact odd-square-sum distance set and is the unique finite-family minimizer in 848 arithmetic candidates for every \(4\le m\le64\), but Landau–Ramanujan rigorou
PARTIALPublished few-distance classifications plus exact witnesses determine \(f_{\rm cvx}(n)\) for every \(4\le n\le20\) (with a jump from 3 to 5), and an elementary regular-pyramid family attains \(\lfloor
PARTIALExact elementary/algebraic certificates prove \(\phi(n,3,3)=3,3,5,6\) for \(n=3,4,5,6\); the planar asymptotic question remains open.
PARTIALThe literal live-page formulation is false and its exact sharp minimum is \(D(X)=\lfloor n/2\rfloor\), attained for every \(n\) by the regular \(n\)-gon; historically intended no-four-concyclic pinned
PROVEDProved \(f(2)=1,\ f(3)=1,\ f(4)=2,\ f(5)=f(6)=3\), established \(3\leq f(7)\leq4\) and \(4\leq f(8)\leq5\), and supplied exact no-four-concyclic constructions and checks; the asymptotic \((1/3+c)n\) q
PARTIALProved \(g(n)\le n-2\) for every \(n\ge7\) and, by exact nested \(\mathbb Q(\sqrt3)\) constructions, \(g(7)=5\), \(g(8)=6\), and \(g(9)=7\); the asymptotic question remains open.
PARTIALMandatory non-collision stop: the live page status is open (“VERIFIABLE - $44”) with 0 claimed proofs, but “Currently working on this problem” lists Ritvik_Nayak, pommeret, ScottHughes, and will0708 (
SKIPPEDThe explicit 12-uniform parity family on 22 vertices has computationally certified property (7,2) and elementary transversal number 10, proving 10 <= f(12,7) <= 11; both asymptotic questions remain op
PARTIALproved the exact boundary formula for every t at n<=2t and independently certified g_3(7)=17, g_3(8)=23 (live thresholds f(7;3)=18, f(8;3)=24); the asymptotic problem remains open.
PARTIALRigorous modulo the published DMMS lemmas, the final parameter argument improves the known upper bound to f(n)=O(n(log n)^7); the independent checker passes the construction, f(n) through 7, all const
PARTIALexact M_2(N)=ceil(N/2)+ceil(floor(log_2 N)/2) is certified for every N<=256, M_t(N) is proved exactly when 3t>N, and a precise Hall-expansion lemma isolates the unproved uniform t=2 step.
PARTIALFor the unrestricted live statement, proved the threshold reduction \(p(h)/2^h\to0\), supplied directly checked witnesses, and computationally established \(H(n)=0,1,2,3,3,3,4,4,4,4,4\) for \(1\le n\l
PARTIAL(b) Morris--Sahasrabudhe--Verstraëte, arXiv:2607.16118v1, gives the uniform answer \(f(n)=\Theta(\sqrt{n\log n})\); independently (d), exhaustive checks give \(f(1),\ldots,f(10)=1,2,2,3,4,4,4,5,5,6\).
PROVEDproved the exact table t(3..7)=(1,1,1,2,2) and gave a checked explicit family with tau=s+1 for every r>=5s+1+floor((s-1)/3); the general problem remains open.
PARTIALproved the sharp \(K_5\)-free odd-clique bound for \(d=5,10,15,20\), with uniform-in-diameter finite certificates and a standalone verifier; the general problem remains open.
PARTIALLIVE PAGE status OPEN (accessed 2026-07-28); it lists “1 claimed proof for this problem”—a partial proof claimed by Lezhe Gao, submitted 2026-07-22 with external proof at Zenodo record 21475089—so Ste
SKIPPEDEvery rayless instance reduces rigorously to a full-type finite-kernel column graph with a ccc finite-independent-set poset; the remaining CH-frontier obstruction is the full-order kernel avoidance pl
PARTIALexact e(n,r) is verified through n=10 and closed forms are proved for r=n-2 and r=n-3, but both fixed-r asymptotic questions remain open.
PARTIALRelative independence is verified modulo Garti--Hayut and Jech; additionally, any first bad cardinal is proved regular and \(\aleph_0\)-closed, sharpening the linked threshold note, while the exact co
PARTIALThe live page is OPEN - $250 with 0 claimed proofs, but lists Sam_Petkov as “Currently working on this problem.”
SKIPPEDReduced every unresolved positive instance to uniform three-way amalgamation of Schipperus game strategies, and proved that every endpoint-compatible alternating block pattern triangle-amalgamates (wi
PARTIALExact computational values F(1..10)=0,1,3,6,9,12,16,19,23,27 are certified with explicit lower graphs and 918,981 exhaustive upper checks; the asymptotic gap remains open.
PARTIALThe literal live H2 assertion is false, rigorously modulo LUW Proposition 2.1: explicit D(5,q) graphs have girth at least 10 but require Omega(q^2) H2 edges; this does not settle the sparsity-qualifie
PROVEDExact exhaustive path-number distributions and the stronger odd-semi-clique classification are verified for every connected simple graph on at most 8 vertices; no uniform proof or counterexample is ob
PARTIALThe live page is still open (display badge “DECIDABLE”) and lists no current worker, but it lists 1 partial claimed proof—Rafik Zeraoulia’s claimed verification through \(n\le 19\), with a visible com
SKIPPEDLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists SkyYang (accessed 2026-07-28), so the mandatory no-collision rule requires stopping.
SKIPPEDLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists Dharun; stopped to avoid colliding with a current worker.
SKIPPEDThe live #575 statement is uniformly false for \(\mathcal F=\{K_{1,2},2K_2\}\): \(\operatorname{ex}(n;\mathcal F)=1\) for \(n\ge2\), while both member extremal numbers grow linearly.
FOUNDindependently proved and reverified the exact table \(f(n)=0,1,2,3,5,6,8,10,12,15,16,18,21,23,26\) for \(1\leq n\leq15\); the asymptotic factor-\(\sqrt2\) upper-bound gap remains.
PARTIALWoodall gives the exact all-\(k\) range \(n<2k\) and \(2k\le n\le4k-3\), and an independent exhaustive check verifies the first three \(C_8\) cases, but the required asymptotic construction remains op
PARTIALcombining the 2026 JLY theorem with KKL densification proves the family (5), including \(29/18\), and certifies all 46 reduced rationals of denominator at most 12; the first gap in the audited suite i
PARTIALExact same-order extremal numbers are proved for every tree (and independently checked for all 106 ten-vertex trees); page \(k=9\) is reduced to 41 tree types and critical hosts with \(n\ge15\), \(e=4
PARTIALproved h(1)=1, h(2)=2, h(3)=3, h(4)=4; gave and independently checked an exact family with h((m+1)^d-2) <= (m+1)^d-(d+1), including h(7)<=6, plus the exact 3x3-grid table; the unrestricted asymptotic
PARTIALmodulo Bertrand's postulate and Mertens' prime-reciprocal theorem, \(M_r(N)\asymp\log N\min\{1,r/\log\log N\}\) uniformly for \(r\ge2\); exact finite bounds, a cap-two construction, a cold Lean audit,
PROVEDStatus OPEN (“This is open, and cannot be resolved with a finite computation”); the mandatory page check found current workers SharkyKesa and SamKorsky in the latest retrievable indexed problem-page r
SKIPPEDThe live page is OPEN with 0 formal claimed proofs and no current worker, but its 2026-07-28 discussion comment explicitly reports that GPT-5.6 Pro claims a negative resolution (with a linked manuscri
SKIPPEDVerified \(f(22)=276\), an explicit \(278\)-point construction in \(\mathbb R^{23}\), the exact \(d\leq8\) table, and the revised reduction \(f(d)=\max\{g(d),s(d)+1,s(d-1)+3\}\); the first remaining c
PARTIALA null-initial well-order gives an explicit counterexample, so the first question is negative under add(N)=cov(N) or non(N)=c; the live joint problem remains OPEN.
PARTIALindependently proved and checked the exact table through n=9 and the sharp 5/9 bound for every three-colour-multiset blow-up; the unrestricted density gap remains, and the live page's 0.5611666 decima
PARTIALproved the rational-dependence subcase constructively, reduced the hard pair \((\sqrt2,\sqrt3)\) to exact Pell residuals, certified its complete record table through \(10^7\), and constructed a checke
PARTIALProved an exact classification for all solutions with at most one odd prime divisor, verified explicit extension certificates, and exhaustively enumerated \(n\leq20{,}000{,}000\) for \(|k|\leq20\); th
PARTIALLive page status OPEN; it lists a partial proof claimed by Xiyu Hu (submitted by hxypqr on 2026-07-23) and names hxypqr as currently working on the problem, so the mandatory no-duplication rule applie
SKIPPEDThe seed \(3,5\) is exactly certified through \(10{,}000{,}000\) terms with \(q_{10^7}=437{,}662{,}243\) and sharp gap bound \(3270\) on that range; infinitude remains open because the required adapti
PARTIALLive page status is OPEN - $10 with 0 claimed proofs, but “Currently working on this problem” lists Tomodovodoo; stopping to avoid colliding with the current worker.
SKIPPEDproved the elementary uniform mean bound \(\sum_{n\le x}|D'_n|\le(2\pi/\sqrt3)x\) and independently certified all values through \(10^6\), finding new records 25, 29, and 32 at \(240240,277200,942480\
PARTIALExact anchor/knapsack certificates rule out every x<=7012 under 1<=n<x; 7013 is only the first relaxation admission, and the asymptotic two-colour problem remains open.
PARTIALThe authoritative live page is OPEN with 0 claimed proofs, but lists Svyable as “Currently working on this problem”; per the collision rule, no mathematical attempt was made.
SKIPPEDLive page status is OPEN (0 formally listed claimed proofs; currently working: None), but the live discussion has a 4 May 2026 comment by DavidTurturean explicitly claiming an unconditional solution o
SKIPPED\(\liminf q_n/n^2\ge1/(S-1)>0.543448148339064\), and exactly \(M(100000)=250\); the required limit remains open and reduces to linked-block sparsity (7).
PROVEDexact CRT reduction and density verified; n_k certified for 1<=k<=110; n_184>10^14 certified; the unresolved step is a uniform initial-interval hit bound such as n_k<=D_k^{-C}.
PARTIALLive page status is OPEN, but it lists 1 claimed proof—a full proof claimed by Colin Snyder (submitted 2026-07-15 01:30:36)—so the mandatory collision rule forbids an attempt.
SKIPPEDThe Mills-realizable coloring \(c(n)=\sum_{q\notin\{2,5,7\}}v_q(n)\bmod5\) has first zero triple \(37,329,226\), proving \(\Lambda(5,3)\ge37,329,226\) (and the same for odd \(5\mid k\)); finiteness re
PARTIALexactly 100 exceptions are certified for 5 <= n <= 10^10 (last 267680), with an elementary reduction and standalone checker; the uniform semiprime-gap step remains open.
PARTIALLive page status is OPEN, but it lists 2 claimed proofs (a full proof claimed by Samuel Korsky on 2026-07-20 and a partial proof claimed by him on 2026-07-18); “Currently working on this problem” and
SKIPPEDProved an elementary canonical descent forest and density-neutral recurrence for all holes; independently verified exactly 4,302 holes and all gap runs through \(2^{25}\), but the uniform multiplicity
PARTIALLive-page status is OPEN with 0 claimed proofs, but Rafikzeraoulia2025 is listed as “Currently working on this problem”; stopped before mathematical work to avoid colliding with a current worker.
SKIPPEDProved an elementary uniform prime-cofactor product formula and exact necessary-and-sufficient reductions (11)–(12), and exhaustively verified all 999,998 values of F(log n,n) through 10^6; the missin
PARTIALRigorous modulo Ford (1998/2013), the ratio has limsup strictly above 1, so any existing limit is >1; existence remains open, with exact certified data through \(x=10^7\).
PARTIALLive page status is OPEN, but its 13 July 2026 discussion comment explicitly says “Here’s the full solution” and links erdos415-sol.pdf; stopping under the no-duplication rule despite the page’s forma
SKIPPEDExact frontier computation proves coalescence for every pair of starts at most 10^10; the open uniform step is to force single-component square frontiers for arbitrarily large k.
PARTIALLive page status OPEN (last edited 17 April 2026; accessed 2026-07-28), with 0 claimed proofs, but “Currently working on this problem” lists conglu and RaziqStark; stopped to avoid colliding with curr
SKIPPEDIndependently proved computationally that the sigma-orbits of 2 and 5 have no common value at most 10^342, extending their published 10^200 separation; no uniform invariant was found, and the next fre
PARTIALThe literal live statement has explicit infinite transient families outside the page's conjectured odd-part list, including every \(2^a3^b\) with \(a,b\geq1\); the exact basin/cycle reduction and a \(
FOUNDLive page status OPEN (accessed 2026-07-28), with 0 claimed proofs and RomanLeLan listed under “Currently working on this problem”; stopped to avoid colliding with the current worker.
SKIPPEDLive page status OPEN with 0 claimed proofs, but “Currently working on this problem” lists Svyable; stopped to avoid colliding with the current worker.
SKIPPEDThe live Erdős Problems #406 page (accessed 2026-07-28) has status OPEN, 0 claimed proofs, and lists `chamb` as “Currently working on this problem” (also “Interested in collaborating”), so the mandato
SKIPPEDLive page status is OPEN, but Sky-Yang is listed as currently working on Erdős problem #404 (accessed 2026-07-28), so the mandatory no-collision rule applies.
SKIPPEDLive page status OPEN; it lists SamKorsky and arkyang as currently working on the problem, so the required no-collision rule applies.
SKIPPEDThe live page displays the problem as FALSIFIABLE/open, with 0 site-filed claimed proofs and no current worker, but its comments list Ahmad Sabihi's paper “A short solution for Brocard-Ramanujans’ pro
SKIPPEDLive page status is OPEN, but “Currently working on this problem” lists jdehorty and SharkyKesa (checked 2026-07-28 via the required Bright Data browser path).
SKIPPEDExact exhaustive computation extends A388302 from n=79 through n=100 (in particular f(80)=76), with a complete geometric-mean reduction and standalone verifier; the uniform asymptotic problem remains
PARTIALLive page status is OPEN, but it lists one full claimed proof (Shouqiao Wang, submitted 2026-07-19), so the mandated no-duplication rule applies.
SKIPPEDProved an elementary prime-gap reduction and, modulo Granville–Ramaré plus PNT, isolated all sufficiently large solutions to a thin prime-free edge regime; exact certified searches found only the nine
PARTIALExactly 100 values n<=10^9 have F(n)<=n, all equalities and the last n=267680; also F(n)-n>=16384 for 521111630<=n<=10^9, while the uniform rough-semiprime lemma needed for either asymptotic question
PARTIALLive page status is OPEN with 1 claimed proof—a partial proof claimed by Rafik Zeraoulia and submitted 2026-07-25—while “Currently working on this problem” is None (accessed 2026-07-28); the mandatory
SKIPPEDExplicit bad intervals are rigorously certified through width 13; exact first starts are computed for widths 0–8, and an audited exhaustive search gives \(999999992\leq U_9\leq4928180396\), but neithe
PARTIALExactly certified max_{n<=10^8} f(n)=f(3250)=1.1792429057944813969965..., found the omitted Sander log-weighted theorem, and reduced the unresolved issue precisely to a uniform small-prime/digit-depth
PARTIALexact exhaustive enumeration gives 14,273 positive solutions through \(10^{100}\), extending the public \(10^{70}\) table by 12,900 verified values, but supplies no uniform infinitude argument.
PARTIALRigorous modulo Laishram--Shorey (2006) plus a twice-reproduced exact computation, Grimm's conjecture holds uniformly for every block length k <= 59; the full problem remains open.
PROVEDLive page status is OPEN with “1 claimed proof for this problem” (a partial proof claimed by Rafik Zeraoulia, submitted 2026-07-27 03:24:16); “Currently working on this problem” is None, but the manda
SKIPPEDThe problem remains open; primary literature gives the omitted unconditional Hickerson classification through \(n\le e^{80}\), while an exact valuation recursion independently finds only the four know
PARTIALProved an exact monotone-triple reduction, exhaustively verified all \(n\leq10^8\) with sharp tail discrepancy bounds, and isolated all-scales fixed-shift exchangeability as the missing lemma; the den
PARTIALModulo Luca–Najman’s corrected completeness theorem, the exact maxima and counts for every prime smoothness bound through 97 are verified, with last \(F(n)<100\) at \(n=9,591,468,737,351,909,375\); th
PARTIALThe live page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists sproutseeds (accessed 2026-07-28), so the mandatory non-collision rule requires stopping.
SKIPPEDLive page status is VERIFIABLE and lists “1 claimed proof for this problem” (currently working: None), so the mandatory no-duplication rule applies.
SKIPPED\(S(10^{16})=26\) is exhaustively certified (five pairs have neither endpoint square), the best located theorem is \(S(x)\ll_\epsilon x^{29/100+\epsilon}\), and the unresolved step is a uniform polylo
PARTIALExact from-scratch enumeration proves there is no square-centered powerful triple \(x^2-1,x^2,x^2+1\) for \(x\le10^{17}\) (center \(\le10^{34}\)); the unrestricted problem remains open because no unif
PARTIALThe live page is OPEN but lists 1 claimed full proof (Principia Math, submitted 2026-07-23) and current workers ruiliangli and Basile_Beyer_de_Ryke, so no attempt was made.
SKIPPEDLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists AnimishSharma; stopped to avoid colliding with a current worker.
SKIPPEDexact computer-assisted thresholds are proved for a 16-cell rectangle, including greatest exception 558 for the irrational pair (10√2,10√3), and the remaining uniform finite-interval lemma is isolated
PARTIALLive page status OPEN; SSD117 and Sprite144 are listed as currently working on problem #348, so no attempt was made.
SKIPPEDLive page status OPEN; it lists 1 claimed proof (a full proof/counterexample claimed by Liam Price, submitted 2026-07-15) and a current worker (SkyYang), so the mandatory no-duplication/no-collision r
SKIPPEDauthoritative live-page status is OPEN, but “Currently working on this problem” lists old-bielefelder (0 claimed proofs); stopped to avoid colliding with a current worker.
SKIPPEDproved a deletion-robust order-3 basis of restricted order 6, completely resolved both finite-deletion questions for eventually periodic bases, and isolated the nonuniform deletion-threshold lemma sti
PARTIALLive-page status OPEN (accessed 2026-07-28), with no current worker, but the page lists 1 claimed proof—a full proof claimed by Colin Snyder (coffeewithcolin), submitted 2026-07-15, asserting \(\lim_{
SKIPPEDExact computation proves G(73)=G(79)=131,486,759 and F(131,486,759)=83; a congruence construction gives F(p)≫log p infinitely often modulo Linnik, while the uniform n^{o(1)} question remains blocked b
PARTIALProved an explicit zero-upper-Banach-density realization \(D(A)=S\) for every \(S\subseteq\mathbb N\), independently verified positive-upper-Banach sufficiency and the packing reduction, and ran the s
PARTIALLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists AnimishSharma (accessed 2026-07-28); per the no-collision rule, no attempt was made.
SKIPPEDLive Erdős Problems page status is OPEN with 0 claimed proofs, but it lists “Currently working on this problem: Aron” (accessed 2026-07-28), so the mandatory collision rule requires no attempt.
SKIPPEDPublished literature plus a checked deduction proves the full asymptotic for every k>=26, improves the lower exponents for k=23,24,25, and gives an exact N=200 table; the verifiable open range is k=3,
PARTIALVerified \(f_{3,3}(10^9)=100735175\) by two independent exact algorithms, derived \(f_{k,3}(x)\sim \Gamma(1+1/k)^3x^{3/k}/(6\Gamma(1+3/k))\) for every \(k\ge26\) from Salberger, and isolated the suffi
PARTIALLive page status is OPEN, but “Currently working on this problem” lists boolean_matrix; the mandatory collision rule therefore forbids an attempt.
SKIPPEDProved an NP-complete upper-bound-attainment subproblem, derived exact common-core and divisibility-chain formulas, and exhaustively certified all 511 nontrivial sets with maximum modulus at most 10;
PARTIALthe Ismailescu--Son candidate is re-certified, and any covering integer must contain at least 59 distinct primes above 10^7 (and outside its 30 covering primes), but ruling out every finite cover rema
PARTIALLive page status OPEN (accessed 2026-07-28); it lists “1 claimed proof for this problem,” specifically a partial proof claimed by Rafik Zeraoulia using OpenAI GPT-5.6 Thinking and submitted 2026-07-27
SKIPPEDLive page status OPEN with 0 claimed proofs, but “Currently working on this problem” lists arkyang (accessed 2026-07-28); stopped to avoid colliding with the current worker.
SKIPPEDproved a sharp explicit formula for every fixed index in the large-seed regime and an O(log n) exact first-obstruction reduction; independently certified A(4) through a_20000, corrected two indexing/p
PARTIALProved fixed-bound factorial-tail separation and Hausdorff dimension zero, reduced a positive factorial answer to open problem #68, and exactly certified that every rational sum for all admissible $\{
PARTIALLive page status is OPEN with 0 formal proof claims and no current worker, but its 9 May 2026 comments explicitly report a checked, Lean-formalized disproof of the second question; the claimed/falsifi
SKIPPEDexact greedy constructions now verify every 1<=n<=100000, correct TUZ20's n=5588 table row, and reduce the uniform problem to a specific modular orbit; the all-n and rational-continuum questions remai
PARTIALLive page status OPEN; it lists 1 claimed proof and Hanziwww as “Currently working on this problem” (accessed 2026-07-28), so the mandatory non-duplication stop applies.
SKIPPEDLive page status OPEN; it lists 2 claimed proofs and Steve_Fan as currently working, so the mandatory no-duplication/no-collision rule applies.
SKIPPEDFor the smallest open case k=5, an exact six-term reduction and independently certified 51-digit computation prove that any rational value has reduced denominator greater than 100000000000000000000000
PARTIALThe main irrationality question remains open; exact reduction (4) isolates eventual periodicity of weighted prime-gap tails, and a reproducible Farey/continued-fraction certificate proves that any rat
PARTIALThe live page status is OPEN, but “Currently working on this problem” lists Terrez1000 and VPendyala (checked 2026-07-28), so the mandatory no-collision gate applies.
SKIPPEDLive page status OPEN; “Currently working on this problem” lists ekalvi (checked 2026-07-28), so the mandatory no-collision rule forbids an attempt.
SKIPPEDLive page status is OPEN with 0 claimed proofs, but “Currently working on this problem” lists Svyable; stopped to avoid colliding with a current worker.
SKIPPEDLive page status “FALSIFIABLE - $250”; “Currently working on this problem” lists KMendoza, dahlkebj, and Sam_Petkov (page accessed 2026-07-28 UTC), so the mandatory no-collision rule applies and no ma
SKIPPEDExplicitly verified a 32-point integer \(n=7\) lower-bound witness, certified the sharp \((7,4,7)\) constrained regime in a stronger signotope relaxation with two SAT engines, and reduced the open 33-
PARTIALThe live page is open with 0 claimed proofs, but its “Currently working on this problem” marker lists JineonBaek and Vugar_Guliyev; per the mandatory no-collision rule, no mathematical attempt was mad
SKIPPEDLive page status is “OPEN - $100”, with 0 claimed proofs, but “Currently working on this problem” lists rubicon (accessed 2026-07-28); the mandatory collision rule therefore forbids an attempt.
SKIPPEDproved an elementary primorial-strengthened bounded-strip theorem and logarithmic record-drift bound, derived long finite monotone staircases from a named almost-prime theorem, and supplied an exact s
PARTIALLive-page status is OPEN with 0 formal proof claims and no current worker, but the 30 April 2026 discussion explicitly claims a Matomäki–Radziwiłł proof, links a solution note, and includes a later “s
SKIPPEDExact standard-library certification of the direct invariant \(\mu(N)\) for every \(1\le N\le40\) (maximum \(1.422032936328\ldots\)); the uniform arbitrary-shift large-prime lemma needed for Erdős #12
PARTIALarXiv:2607.17333v2 gives an exact affirmative solution to #1199; the current proof audit found no gap modulo its named Stone–Čech facts and Hindman's 1979 Corollary 2.10, and an independent exhaustive
FOUNDYounis's 2024 all-interval theorem plus the classical Dickman theorem proves #1184 for every fixed \(1<\alpha<30/17\) unconditionally (and for \(1<\alpha<2\) under RH); the endpoints and larger \(\alp
PARTIALVerified F(7)=11 and f(7)=16 by a fresh exhaustive checker, recovered the published table through n=12, and sharpened the live-page existential bound to n^(3/2)sqrt(log n) << f(n) << n^(3/2)log n via
PARTIALExact labelled distributions through n=7 (plus the n=8 chi<=3 prefix), two all-n tail formulas, an eventual-unimodality reduction for question 1, and an exact fixed-window reformulation for question 2
PARTIALReconstructed the known sharp worst-prime-tuple value \(\lceil2\sqrt u\rceil\) for \(2<\alpha<3\), certified explicit \(\alpha=5/2\) examples for \(u\leq16\), proved current arithmetic-Kakeya lower tr
PARTIALExact modular covering proves there is no solution for \(2^{128}\le n\le340282371933923199876807076826562457784\); the uniform Erdős problem remains open.
PARTIALproved the exact equivalence \(R_N\to0\iff\mathcal G_2(p_{N+1})/\mathcal G_1(p_{N+1})\to0\), derived a rigorous chain-theorem lower bound for the numerator, and exactly verified \(2/9\le R_N\le5510/12
PARTIALIndependently verified \(h_3(4)=11\), \(h_3(5)\ge19\), and exact \(f(n)\) through \(n=18\); proved the Davies--Illingworth threshold/peeling template cannot beat constant \(2\), but did not improve th
PARTIALExact exhaustive rational enumeration proves the signed maxima \(0,0,2,4,6,8,12\) for \(1\leq n\leq7\), with a standalone checker; the asymptotic exponent remains in the verified interval \(1.77898\ld
PARTIALThe two page-cited ZFC constructions are verified to contain \(K_{\aleph_0}\); an ordered lower-clique theorem and exact truncation formulas are proved, while the general problem remains open at the c
PARTIALproved the sharp bound \(p-k!\geq\operatorname{nextprime}(k)^2\), certified equality solutions \(769\) and \(6\,227\,021\,089\), and exactly corrected/enumerated the strict sequence through \(10^9\) (
PARTIALmodulo Dirichlet every class is nonempty and infinitely many primes lie at or above each class; an independent exact certificate gives \(p_1,\ldots,p_{18}\), while exact-class infinitude and the behav
PARTIALverified g(4..14)=(3,0,3,3,3,3,3,3,4,4,4), extended Simonovits's Omega(n^(1/3)) bound to every sufficiently large order by Hajós joins, and constructed delta>=4 examples for every n>=56; the linear-gr
PARTIALverified the omitted stronger linear bound \(R(k+1,k)-R(k,k)\geq2k-2\) for \(k\geq5\), proved its optimality within the Xu--Shao--Radziszowski adjacent construction family, and reduced a proportional
PARTIALLive page status “OPEN - $100” (accessed 2026-07-27); “Currently working on this problem” lists CrashoverrideX and Sam_Petkov, so the mandatory no-collision rule requires no attempt.
SKIPPEDmodulo Guth–Maynard, \(13/30\le\liminf f\le1\) and \(\limsup f\ge13/30+\log2\); all three questions reduce exactly to \(f(p)\), and exact integer computation certifies the unique extrema through \(2{,
PARTIALExhaustively cross-checked all 171,551 connected 6-regular circulant parameter triples through order 80; every one of the 5,806 four-vertex-critical cases has a critical edge orbit, so no circulant ta
PARTIALUnder CH the explicit shift graph on \([\omega_2]^2\) has chromatic number \(\aleph_1\) and every lesser-order-type subgraph is countably chromatic; the first variant is blocked in the Foreman--Laver
PARTIALThe first question is relatively independent (even with GCH); the second has an exact positive solution under square+CH, hence in L, and reduces uniformly to the unresolved countable-chromatic-compact
PARTIALExhaustively verified \(f_6(6),\ldots,f_6(11)=15,15,23,27,35,39\), exhibited the unique 11-vertex 39-edge core, and reduced \(f_6(n)\sim n^2/4\) exactly to the two missing upper bounds (L5) and (I6);
PARTIALErdős #911 is exactly reduced, up to explicit constants, to proving \(\beta(d)=\omega(d)\) for bipartite minimum-degree-\(d\) targets; projective-plane incidence graphs certify that biclique extractio
PARTIALExact identities reduce #890 to a parity-level almost-prime tuple problem and a coefficient-1 maximal-order bound for \(\omega(\prod_{i<k}(n+i))\); an independently rechecked exhaustive scan on \(5{,}
PARTIALAn elementary Pell-orbit construction gives infinitely many n with five divisors in the required window for every C>24 (explicitly, the whole stated orbit works for C=25), improving the live comment's
PARTIALLive page status is OPEN, but “Currently working on this problem” lists MaskoMys and zitterbewegung (accessed 2026-07-27); mandatory no-collision stop.
SKIPPEDErdős–Rosenfeld, open at k=5: do five integers exist sharing at least five common factor-differences D(N)={|a−b| : N=ab}? The cases k=2,3,4 are solved. We ran GPT-5.6 Sol on it and found no witness — but a strong partial: a clean reformulation (a k=5 witness is exactly a 5×6 square-additive rectangle, equivalently a K₅,₅ biclique), an independent re-verification of the known k=3 (Guiduli) and k=4 (Bremner) examples, and three separate proofs that three different near-miss families are exactly saturated — Bremner's k=4 rectangle, Choudhry's brand-new June-2026 5×3 family, and a community list of 71 4×6 rectangles each admit no further row or column, all re-run on our side. Honest gap: no global obstruction proved; a witness could lie past every region searched.
PARTIALFULL WRITE-UPExact exhaustive verification proves the sharp threshold for every nonvacuous n<=36 and every required odd cycle length through C13; the uniform endpoint remains open and requires an arithmetic Hall-e
PARTIALThe live page status is OPEN with 0 claimed proofs, but it lists Svyable as “Currently working on this problem” (and its discussion contains Svyable’s unverified 3 May 2026 complete-answer post), so t
SKIPPEDProved that \(3+2\sqrt2\) is the sharp exponent for every block-size schedule certified by the posted \(C_k\) carry-closure lemma; the original range \(1\le c<3+2\sqrt2\) remains open.
PARTIALProved the elementary uniform bound \(F(A,X,k)\ll_k X^{\Delta_k}\log X\) with explicit \(\Delta_k\downarrow1/4\), upgraded it to the literal live-page inequality for every \(\epsilon>1/4\), and exactl
PARTIALThe authoritative live page (accessed 2026-07-27; status OPEN; 0 claimed proofs) lists current workers old-bielefelder, pommeret, and joshoakley, so the mandatory non-collision rule requires no attemp
SKIPPEDThe live page status is OPEN with 0 claimed proofs, but Woett is listed under “Currently working on this problem”; no attempt was made.
SKIPPEDLIVE PAGE status OPEN; mandatory gate triggered because it lists 1 claimed proof—a partial proof claimed by Samuel Korsky (using GPT 5.6-Pro), submitted 2026-07-26—and lists “Currently working on this
SKIPPEDThe authoritative live page is OPEN and shows “Currently working on this problem: None”, but it lists 1 claimed proof—a full proof claimed by RayYoung, Keheng Zhu, and Yanping Luo, submitted 2026-07-1
SKIPPEDexplicit 447-in-3159 admissible/CRT certificate and exact fixed-width scan through x=10^8 verified; the live large-x,large-y question remains open because the missing step is simultaneous primality of
PARTIALProved (modulo PNT and Mertens) liminf F(k)/(k log log k) >= e^gamma and Q(k) >= (e^gamma/2-o(1))k log log k; independently verified exact F(k) through k=13, full gap sets through k=8, and F(100)>=482
PARTIALCertified every even consecutive-prime gap through 1572, proved \(r(92,489,057,256,472,962,493)\ge1574\), exactly computed \(r(50,847,533)=254\) with all prefix breakpoints, and reduced the two open l
PARTIALVerified the repaired \(h(x)\gg(\log x)^{1/3}\) and \(h(x)\ll_\varepsilon x^{0.41+\varepsilon}\) reductions, computed the exact frontier through 105,000,000 starts, and found \(R(14)=R(15)=19,205\); t
PARTIALelementary reduction and an independent exact scan exclude y<=10^9; modulo Hercher's published exhaustive Theorem 1, all y<1.4e12 are excluded, but the unbounded problem remains open.
PARTIALExact modulo the published fixed-pair theorem, every \(\binom n2\) with \(4\leq n\leq10^{32}\) has half-triangle multiplicity at most 4 (only \(n=78\) attains 4); a 4.319-billion-candidate exact sieve
PARTIALProved \(A_3\cap[0,2/9)=\{0\}\), certified the exact five-vertex Lagrangian gap at \((189+15\sqrt5)/961\), and isolated the unproved endpoint-jump lemma hidden by the published \(0.2316\) rounding.
PARTIALLive page status is OPEN with 0 formal proof claims and no current worker, but its discussion page (accessed 2026-07-27) says “GPT-5.5 Pro claims a solution to the 2nd question here,” so the mandatory
SKIPPEDProved an elementary complement/extension equivalence and a hereditary LS(4,5,k+5) obstruction, independently verified the k=4,6 exceptional cases, and isolated k=16 at the open LS(4,5,21) barrier; pr
PARTIALexact equation-only A(10^8)=236 (231 distinct pairs plus 5 perfect diagonals), with a dual-engine checker through 10^7, endpoint re-factorization through 10^8, an exact aliquot-cycle reduction, and a
PARTIALVerified \(h(10^6)=6{,}437{,}809\), an explicit 46-member coprime sigma-fiber, and the sharper named-theorem bound \(h(x)>x^\alpha\) for every \(\alpha<1.4313775065\ldots\); exponent \(2\) still requi
PARTIALThe authoritative live page is OPEN but lists “1 claimed proof for this problem”; per the mandatory collision rule, no mathematical attempt was made.
SKIPPEDProved the fixed-window transfer \(R(n+h)-R(n)\geq r(h+1,n+h)-1\); with the published \(r(4,t)\) bound, superquadratic gaps occur in every three consecutive positions (lower density at least \(1/3\)),
PARTIALProved an exact rainbow-triangle identity and sharp t=2 minimum, proved problem 811 positive for forests and graphs with 2-core K3, proved lexicographic amplification always fails for C6, and reduced
PARTIALExhaustive certificates prove computationally that \(M(n)=0,1,3,5,7,11,14,17,23,30\) for \(1\le n\le10\), but the uniform dense construction/colored-completion lemma needed for Erdős #810 remains open
PARTIALThe live problem remains open only for C7; exact computation and an explicit certified witness give chi_S(10,26,C7)=13, while the uniform high-density path-length lemma needed for the n→∞ asymptotic i
PARTIALindependently verified the exact table g(n) for every 0<=n<=65; #791 remains open between the Yu and Kohonen asymptotic constants.
PARTIALExact, from-scratch computer-certified values are \(g(n)=1,2,3,4\) on \(n=1\!-\!3,4\!-\!7,8\!-\!13,14\!-\!19\), respectively; the asymptotic problem remains open.
PARTIALFor the distinct-elements problem, proved computationally that \(M(20)=13\), recomputed the exact table \(M(N)\) for \(2\le N\le25\), and isolated the one-rank signed-relation defect that blocks the p
PARTIALVerified a 5-QP(4) of positive squares, correcting the 2003 “no 5-QP(5) found” observation; exhaustively proved diameter at least 4 for five terms with least gap at most \(10^8\), while both arbitrary
PARTIALproved the exact Cramér-window/tail decomposition, APRCL-reverified witnesses for 2<=n<=100, and BPSW-checked (not proved) the n=3001 candidate; the uniform prime-gap/prime-pair step remains open.
PARTIALLive page status OPEN; it lists 1 claimed proof (a partial proof claimed by Jeffrey Zeng, submitted 2026-07-24 17:13:29) and no current worker, so the mandatory no-duplication rule applies.
SKIPPEDLive page status is OPEN (accessed 2026-07-27), but it lists “1 claimed proof for this problem”—a partial proof claimed by Jeffrey Zeng and submitted 2026-07-24—while “Currently working on this proble
SKIPPEDThe general problem remains open, but the two live questions are rigorously equivalent, and an independently checked exhaustive computation classifies every graph through seven vertices: exactly \(K_7
PARTIALThe open problem is not solved; an independently rerun exhaustive census proves the exact values of \(M_{13}(T)\) for every 6- and 7-vertex tree, with explicit 4-chromatic graph6 witnesses and a preci
PARTIALexact f(n)=(3,3,4,4,6,6,6,6,6) for 3<=n<=11 with a from-scratch exhaustive verifier; proved an Omega(n^(3/4)) projective-truncation obstruction and isolated a quantifier gap in the current conditional
PARTIALThe live page is OPEN but lists 1 claimed proof—a full proof claimed by Eric Li (using GPT-5.5 Pro), submitted 2026-07-17—and lists “Currently working on this problem: None”; the claimed-proof stop co
SKIPPEDThe live page is OPEN but lists 1 claimed proof—a full proof claimed by Liam Price (using GPT Pro), submitted 2026-07-15—and lists “Currently working on this problem: None”; the claimed-proof stop con
SKIPPEDcorroborated Lu's stronger \(f(n)\geq n^{10/143}-2\) literature bound, independently verified nine MOLS(108), and exhaustively ruled out an eleventh row in the published matrix's natural equivariant f
PARTIALThe unrestricted problem remains open; verified here are an explicit Hall-multiplier proof excluding cyclic order 12 and a from-scratch exact exclusion of every non-prime-power cyclic order through 10
PARTIALFor the intended range r>=2, proved the conjecture uniformly for n<=r+3 and exactly for (r,n)=(3,7), with a standalone exhaustive checker; the general covering-design inequality (7) remains open.
PARTIALLive page status is OPEN with 0 claimed proofs, but it lists “Currently working on this problem: skominers” (accessed 2026-07-27); the mandated collision rule therefore forbids an attempt.
SKIPPEDLive page status is “OPEN - $78”, with SkyYang listed under “Currently working on this problem”; stopped to avoid colliding with a current worker.
SKIPPED\((1/e-o(1))\log n\le f_{709}(n)\le7\lceil n^{3/7}\rceil\), with a direct checked Hall certificate \(f_{709}(999999)>4.151303\); the asymptotic order remains open.
PROVEDThe polynomial upper bound remains open; this run gives explicit checked clique certificates including \(L(5)\ge12,L(7)\ge16,L(8)\ge19\), and proves by a standalone exhaustive checker that the triangu
PARTIALLive page status is OPEN, with 0 claimed proofs, but pollodumas is listed under “Currently working on this problem” (checked 2026-07-27), so the mandatory no-collision gate requires stopping.
SKIPPEDClassical finite-lcm reduction verified; a density-preserving blow-up gives a primitive gcd-1 reciprocal-divergent example of exact density 2/3, and all 1024 five-prime semiprime families were exhaust
PARTIALLive page status OPEN; it lists “1 claimed proof for this problem,” triggering the mandatory no-duplication stop.
SKIPPEDProved the exact Jacobsthal-quotient reduction, the unconditional bound \(\limsup\epsilon_n\le e^{-1}\), and a from-scratch exact table \(L(n)\) for every \(11\le n\le70\); the missing uniform linear
PARTIALThe live page status is OPEN, but it lists 1 partial claimed proof (Jake Weatherhead, submitted 2026-07-14) and “Currently working on this problem: None”; stopped under the mandatory claimed-proof col
SKIPPEDproved an exact LCM-seed valuation reduction, certified f(lcm(1..150)-1)=924 and the n<=100000 record table, and found a rigorous counterexample to the Fourier-tail lemma underlying arXiv:2604.23784's
PARTIALReduced #683 exactly to a fixed-power saving for the gap function f(y), proved c=1/10 for every k<=2,845,920 modulo Nagura and Nair--Shorey with all finite exceptions checked, and exhaustively verifie
PARTIALLive Erdős Problems #681 page status is OPEN, but it lists “Currently working on this problem: stellachenyl” (accessed 2026-07-27), so the mandatory no-collision rule applies.
SKIPPEDExact reduction obtained; the first assertion holds for every \(116\le n\le10^9\) (next-prime witness), with exactly seven smaller exceptions, while the uniform square-root gap step and the exponentia
PARTIALLive page status OPEN; mandatory collision guard triggered because it lists 1 claimed proof (a partial proof claimed by Liam Price using GPT 5.6 Sol Pro, submitted 2026-07-27 13:14:00); “Currently wor
SKIPPEDModulo verified square/cube/fifth-power theorems, any counterexample at the first unresolved lengths k=35..38 has prime exponent at least 7 and largest term at least 13,357,343; 13,750,206; 47,045,881
PARTIALExact finite progress—proved by a standalone exact certificate that for every d>=3 the minimum five-point diameter is 10+t_*=10.097819085934546..., with an explicit R^3 Gram construction; the fixed-d
PARTIALProved the uniform bound c(p,q) <= (p-2)/(C(p,2)-q), the neighborhood recurrence, and two infinite families of strict adjacent jumps; reduced the remaining p=4 jump exactly to the independence exponen
PARTIALExact catalogue-backed verification proves the \(k=4\) assertion for every graph on at most 12 vertices, with sharp threshold \(\chi=5\), and determines the unique smallest path-version witness at ord
PARTIALThe live page status is OPEN with a “Partial Solution” notice stating “A claimed solution has been posted in the comments”; the discussion page shows an April 2026 claimed counterexample/proof thread,
SKIPPEDProved that any total-\(\le39\) obstruction reduces to one on a palette \(11\le q\le22\), and computationally certified with two independent solvers that every 11-color obstruction whose unoriented un
PARTIALIndependently reproduced the known double-critical census through 12 vertices and certified that any order-13 noncomplete double-critical graph must be 6- or 7-chromatic; the general Erdős–Lovász Tiha
PARTIALExact, reproducibly checked values are \(f(n)=1\) for \(1\le n\le4\), \(f(n)=3/2\) for \(5\le n\le10\), and \(f(n)=2\) for \(11\le n\le16\); the asymptotic limit remains open.
PARTIALreduced both limits exactly to growth rates of N_k(m), proved the m=3 exponent 1/2 modulo Kim, improved liminf g_4(n)/log n to 1/(6 log 2) modulo Morgenstern, and independently verified a 66-vertex gi
PARTIALStatus OPEN ($1000), but the live-site search index lists “Currently working on this problem | zitterbewegung” for #625 (cross-checked on the indexed zitterbewegung profile); direct Bright Data access
SKIPPEDf(n,k) is the fewest edges forcing every (k+2)-set of vertices to induce a subgraph with a vertex of degree ≥k. Round 1 reduced it to a finite-family Turán problem and flagged the general formula as unproven. Round 2 pushed on that gap — and mostly settled it, except for one claim we caught overreaching: it silently treated the 50-year-open Erdős–Simonovits even-cycle conjecture as solved. Corrected, and the corrected version is the more interesting finding: for most k, a clean formula is provably at least as hard as that named open problem — that's WHY it doesn't exist, not just that nobody's found it yet. Round 3 maps the regime Round 2 left untouched — the near-diagonal one (n−k small): the actual 1996 Erdős–Reid–Schelp–Staton theorem and Pikhurko–Thomason's 2002 follow-up, which disproves the ERSS conjecture, gives the k→∞ asymptotic, and proves the naive split-graph fails off-diagonal — plus an unconditional f(n,k)=C(n,2)−o(n²) for every fixed k. The fixed-k orders Round 2 already proved (k=2,3,…) re-derive here; they're confirmation, not new ground.
LIVEFULL WRITE-UPLive status is OPEN with no worker or claimed proof; primary sources leave \(2^{\Omega(\sqrt{\log n})}\le f(n)\le O(n^{3/2}2^{n/2})\), while a proof-carrying exhaustive computation establishes the exa
PARTIALproved \(\omega_1^2\to(\omega_1\omega,G)^2\) for every finite \(K_4\)-free block graph and reduced the full finite question exactly to 2-connected \(K_4\)-free blocks; the first unresolved-by-this-met
PARTIALClassified every finite target in the full \(G_1=C_4\) row—exactly the triangle-free, \(C_4\)-free graphs containing \(P_4\)—and found/verified the minimum 9-vertex, 11-edge \(C_4\)-free red-blue Rams
PARTIALThe live page status is OPEN, but it lists 1 claimed proof—a full proof by Cambie Stijn and Freschi Andrea (arXiv:2606.11174, submitted 2026-07-25)—and its newest comment says the solution is availabl
SKIPPEDProved the explicit 2-core reduction \(R(G,H)\le R(G,C_2(H))+(v(G)-1)(v(H)-1)\), reduced #568 to connected minimum-degree-two targets, and exhaustively isolated \(K_4^*\) as the unique order-at-most-f
PARTIALProved exact all-n formulas for R(H5,nK2), R(K3,3,nK2), and R(Q3,nK2), with an exhaustive standalone verifier; the full arbitrary-target problem remains open.
PARTIALProved \(R(K_4^*,nK_2)=2n+2\) for every \(n\ge2\) and computationally determined \(R(K_4^*,H)\) for every no-isolate \(H\) with at most four edges; the uniform \((2,3)\)-sparse problem remains open.
PARTIALproved a uniform barrier excluding every fixed pointwise two-colour merge of the standard four-colour stepping-up construction, and independently verified the known explicit 87-vertex colouring \(R_3(
PARTIALProved the exact piecewise formula R_alpha(4)=18,10,6, computed the complete n<=7 extremal table, and reduced the asymptotic question to existence of lim_k log R_alpha(k)/k, whose alpha=0 case is the
PARTIALverified a compact explicit 87-vertex coloring proving the known bound \(R_3(5)\geq88\), proved a uniform no-go theorem for the naive tournament stepping-up lift, and isolated the still-missing \(R_3(
PARTIALLive page status OPEN; it lists old-bielefelder under “Currently working on this problem” (and 0 claimed proofs), so the required collision rule forbids an attempt.
SKIPPEDindependently certified \(\hat R(K_{2,2})=15\) and uniquely \(K_6\) as the 15-edge host (up to isolates), proved \(45\le\hat R(K_{3,3})\le153\), but the conjectured diagonal factor \(n\) remains block
PARTIALAn explicit cubic-residue colouring and an elementary spectral count prove \(20\le R_3(K_{2,3})\le22\); unrestricted \(K_{20}\)/\(K_{21}\) feasibility is the exact remaining finite question, while cyc
PARTIALverified \(R_q(T)\leq q(n-2)+2\) for all sufficiently large fixed-bounded-degree trees (modulo Pokrovskiy Theorem 1.16), certified every \(R_3(T)\) for \(|T|\leq5\), and isolated the unresolved all-tr
PARTIALThe live statement is false at n=3 (R_3(C_3)=17>9); for the intended n>=4 problem, R_3(C_4)=11 and the sharp Toeplitz K32/K33 C_9 transition are verified, while unrestricted R_3(C_9)<=33 remains open.
FOUNDThe live page status is OPEN and lists RobSneiderman under “Currently working on this problem” (with 0 claimed proofs), so the mandatory no-collision rule requires stopping.
SKIPPEDThe live problem is open with no claimant or worker; current bounds miss by a \(k^{k/\ell}\) factor, and the report proves a precise colour-index-gap reduction plus fully checked finite certificates,
WALLCan two disjoint blocks of consecutive integers, both length >3, ever have equal products? 8·9·⋯·14 = 63·64·65·66 = 17,297,280 is the only known example. Round 1 established fixed-pair finiteness. Round 2: a real corollary narrows it further (fixed length RATIO is also finite, so any infinite family needs infinitely many distinct ratios), a 2024 paper's computer search conjectures this IS the complete classification, and a search reaching 10 million found nothing else across 1.4 billion comparisons. Round 3: a follow-up wrote out the actual proof of the fixed-unequal-length finiteness Round 2 had only cited — a clean Kulkarni–Sury case-elimination we verified by exact computation — and caught a subtle error in the naive root-comparison argument. It proves no uniform bound, so the full problem stays open; everything below the uniformity step is now settled.
LIVEFULL WRITE-UP#126 asks whether f(n)/log n → ∞, where f(n) is the fewest distinct primes that can support all pairwise sums of an n-element set — equivalently N(s)=exp(o(s)), N(s) being the largest set whose pair sums use ≤s primes. The window (½+o(1))s·log s ≤ N(s) ≤ 2^s has been open since Erdős–Turán. We didn't prove it and found no counterexample — but a strong partial: the conjecture reduces cleanly to ONE missing theorem (a uniform subexponential bound for binary S-unit equations over ℚ), the key extra structure is identified (the problem needs a clique of mutually compatible S-unit solutions, not the star a single binary equation gives), and the old local prime-by-prime route is provably dead. N(2)=4 exactly, plus explicit f(14)≤8 and f(21)≤12 — all verified on our side.
PARTIALFULL WRITE-UPcertified 247 distinct cycle sets on 11 vertices, so f(11)>=247; reproduced exact f(1..10), but the required unbounded-factor lower bound remains open.
PARTIALLive page status OPEN; collision rule triggered because “Currently working on this problem” lists Svyable (checked 2026-07-27).
SKIPPEDLive Erdős Problems #81 status is OPEN with 0 claimed proofs and “Currently working on this problem: None,” but it lists jtraverso under “I am working on formalising the results on this problem”; this
SKIPPEDLive page status OPEN; it lists “Currently working on this problem: memeister27,” so no attempt was made under the required collision rule.
SKIPPEDThe live page status is “OPEN - $500” with 0 claimed proofs, but it lists Mahmudsudo and quintessen as “Currently working on this problem”; stopped before any mathematical attempt to avoid colliding w
SKIPPEDExhaustively verified the exact complete-bipartite minimum and uniqueness for every \(4\le n\le10\) and \(2\le d\le\lfloor n/2\rfloor\); the unresolved step is a uniform fixed-small-\(d\), all-\(n\) s
PARTIALProved the common-4-chromatic conclusion for every pair of canonical finite-order shift-graph ages and computed exact first thresholds 4, 9, 21, 85, 8574 through order five; the arbitrary good-family
PARTIALExplicit induced-C6-free lexicographic powers have 17^k vertices and homogeneous number 3^k, giving c_EH(C6) <= log_17(3), with T_C6(4)=18 and an exact 104-type six-vertex threshold table; the uniform
PARTIALExhaustively verified the new exact cases \(h_{C_4}(n,1)=2\) for every \(14\le n\le18\), with explicit two-cycle witnesses and a 55-second standalone checker; the uniform \(\Omega(\sqrt n)\) problem r
PARTIALProved, modulo Schoenberg/Mertens/Bertrand, a dense continuum-sized family of irrational points generated by an explicit recursion with infinite upper-right Dini derivative; the possibility of a finit
PARTIAL#41 asks whether every infinite B₃-set (all triple sums distinct) must have its normalized counting function dip to zero: liminf A(x)/x^(1/3)=0. It's known for every even order and open for odd. GPT-5.6 Sol found no resolution — but a strong partial: (1) the exact reason the classical B₂ method breaks at B₃, a parity wall (a B_h condition controls an h-variable signed form, which can balance + and − only when h is even); (2) a real conditional theorem — any B₃-set with positive critical density must have logarithmic gap spikes, so #41 holds for every smooth-gap B₃-set; (3) the sharp finite bounds 1 ≤ liminf R₃(N)/N^(1/3) ≤ limsup ≤ 1.51546…; (4) an explicit construction hitting the critical exponent 1/3 at checkpoints (but with liminf zero). Constants and citations re-verified on our side.
PARTIALFULL WRITE-UPPliego's theorem rules out every g with a positive polynomial lower bound, an exact compactness reduction isolates the remaining subpolynomial frontier, and a verified 25-term cap-3 witness gives psi(
PARTIALexact finite square-completion numbers are verified through target 101, with a rigorous block reduction isolating the missing uniform \(q(N)<(2-o(1))\sqrt N\) lemma; the live limsup constant remains o
PARTIALExact fresh-shell minima were certified at 13 values through N=128, and two natural independent-scale approaches were rigorously shown to retain the log-squared barrier; the missing step is a correlat
PARTIALProved that bounded pairwise gcds force an explicit natural density, so every counterexample must have unbounded common factors; verified 27,567 finite systems and an exact nonsummable gcd-2 example.
PARTIALThe authoritative live page is OPEN - $1000 but lists sproutseeds, Rynaldos, and Lumantis under “Currently working on this problem” (accessed 2026-07-27), so the mandatory no-collision rule applies.
SKIPPEDThe live page is OPEN - $250 but lists 1 claimed proof (a partial proof claimed by Liam Price, submitted 2026-07-24, asserting the first question) and Sam_Petkov as currently working on the problem; m
SKIPPEDProved an elementary cylinder-budget theorem forcing convergence for the regular oriented-CRT block template used in the live comments, and exactly computed the finite harmonic optima M(N)=3/2 through
PARTIALLive page status OPEN with 0 claimed proofs, but “Currently working on this problem” lists lof310 (checked 2026-07-27), so the required no-collision rule applies.
SKIPPEDLive page status “VERIFIABLE - $25”; current workers are listed as duckmerc and Aurelien_Col, so the mandatory no-collision rule forbids an attempt.
SKIPPEDCounterexamples to eventual strictness found and checked. Unresolved.
PARTIALLiterature map plus several open cases — no resolution.
NO PROGRESSOpen — a related variant was solved by others (Joret–Micek–Reed–Smid) while we worked it.
NO PROGRESSPage status: OPEN; nevertheless, erdosproblems.com lists #550 under “Solution Claims” (Eric Li claims a full proof in arXiv:2606.23659), so the mandatory claimed-proof stop condition applies.
SKIPPEDBright Data reached Erdős Problems #547 but the origin returned HTTP 522; the latest accessible indexed page and discussion-thread representations (crawled three weeks to one month ago) report status
SKIPPEDproved from scratch that the eight-edge colex graph has Ramsey number 18 (so its exact matching counterexample gap is 5), and located the missed 1989 theorem \(R(\widehat K_{n,2})=R(K_n)\) for every \
PARTIALAn exact checker exhibits nested critical graphs through k=8, proves that the unique (3,9;35) graph has independent-8-set transversal number 9 so the nesting cannot continue at k=9, and proves a sharp
PARTIALVerified \(F(1)=1\), \(F(2)=9\), and certificate-backed \(F(3)=54\); an explicit checked colouring proves \(F(4)\geq201\), while the asymptotic tower-versus-double-exponential gap remains open.
PARTIALThe order is already Θ(√N) — the refinement is the question. Open.
NO PROGRESSSieve machinery explored; the full problem appears untouched. Open.
NO PROGRESSExplicitly reverified an 8-coloring of [1,5362], derived a checked infinite lower-bound subsequence, repaired the printed width-111 template, and proved the width-380 tail constant 148 locally maximal
PARTIALproved the sharp identity A(p^2-p+1)=p-1 for every prime p and independently verified A(n)>=227 on 10^6<=n<=10^7; the uniform limit remains blocked by a worst-case rough-semiprime gap lemma.
PARTIALThe stronger composite-only inequality with C=1 is certified (>0.961) for every real x in [10^6,10^9], and the remaining all-x asymptotic step is the stated uniform balanced-semiprime Type-II lower bo
PARTIALExplicit CRT arithmetic gives f(n,500)=218 (hence any uniform constant is at most 0.436), and exhaustive periodic enumeration gives the exact minima for every t<=13; Erdős #461 remains open.
PARTIALReduced the conjecture to a precise growing paired-gap window and certified every prefix record through \(n=10,000,000\), with maximum \(148\) first at \(n=2,886,673\); unboundedness remains open at t
PARTIALHow long a run of consecutive integers can stay above the normal prime-factor count ω(n) > log log n? Round 1 gave the explicit CRT lower-bound construction and reported the honest bad news: no non-trivial upper bound existed anywhere. Round 2, same day: a second model built a real one — a genuine sieve-theoretic upper bound miles below the trivial prime-gap bound, with a fully checkable 5-integer example. Half its six background literature citations didn't survive verification and are dropped below; the actual proof — checked independently, not just accepted — doesn't depend on any of them.
LIVEFULL WRITE-UPThe problem remains open; verified current progress is Croot--Yip's July-2026 quadratic-intersection theorem, and this report adds an exhaustive sharp computation of the balanced all-prime-sum paramet
PARTIALAny hypothetical witness sequence is rigorously forced by a uniform Selberg prime-pair bound to have gaps at least $\exp(m^{c_A})$, an exact synchronized-chain reduction and two-witness maxima through
PARTIALRound 5 — the capstone. The 0-indexed entirely-complete boundary has a closed form, t0(α) = min over k≥0 of (2^k+1)/α^k, now triply confirmed (our exact-rational compute, a same-family skeptic, and a cross-family GPT-5 Pro proof whose key move is Graham's 1964 Lemma 4 in disguise). The honest payoff is provenance: under the reindex u=t/α the 0-indexed sequence IS the literature's sequence, so for t<α we sit inside Graham's 1964 unit square (Acta Arithmetica 10, primary-verified — Lemma 1 the greedy criterion, Theorem 5 the powers-of-two obstruction, Theorem 6 the regions whose pullback is exactly our fragmented complete set, Theorem 3 complete iff entirely complete there) and for t≥α inside van Doorn 2026. So the set, its ≈85% area, and its region structure are Graham's; the 1-indexed closed thresholds are van Doorn's. What is genuinely new is the independent cold re-derivation plus the one-line min-formula boundary of Graham's set in 0-indexed coordinates (explicit shelf + least-minimizer) — a unification not previously written — not a new theorem. We think that is the better, truer story.
LIVEFULL WRITE-UPSubset-sum checker built; the asymptotic threshold is unresolved.
NO PROGRESSProved the exact forward-obstruction characterisation and \(a_n\leq\binom n3+n\), independently recomputed 3,000 terms and the collision/tail split, but the required uniform \(m^{2+o(1)}\) bound remai
PARTIALproved the complete finite-prefix-shadow criterion for all ultimately periodic pairs, exhibited \(A_q=q\mathbb N\cup\{1\}, B_q=q\mathbb N\), and exhaustively verified the stated small-period tables; t
PARTIALLive page status OPEN, but it lists 1 claimed full proof—Will Sawin's submitted 2026-07-18 construction giving a positive-density counterexample to the second question (now arXiv:2607.15419)—so the ma
SKIPPEDLive page status is OPEN, but it lists 1 claimed proof (and no current worker); the mandatory collision rule therefore forbids an attempt.
SKIPPEDExact modular certificates prove the second inequality for every \(5\leq n\leq200000\) (and equality defeats it exactly at \(n=1,2,3,4\) in this range); the uniform prime-residue lemma and the first q
PARTIALNew computational contribution landed; infinitude still open unconditionally.
PARTIALLive page status is OPEN with 0 claimed proofs, but SamKorsky is listed under “Currently working on this problem” (accessed 2026-07-26), so the mandatory no-collision rule requires stopping without an
SKIPPEDUniform elementary equivalence proof, corrected rigorous 5/6 subsequence argument, and an exact independently checked table extended from N=25 to N=50; the asymptotic question remains open at the expl
PARTIALLive page status on 2026-07-26 is open/VERIFIABLE with 0 claimed proofs, but “Currently working on this problem” lists aditya, will0708, and Ary300; stopping to avoid colliding with current workers.
SKIPPEDLive-page status is OPEN (0 site-counted claimed proofs; “Currently working on this problem: None”), but the live discussion contains Yuren Tang’s explicit 19 June 2026 claim of an affirmative, sorry-
SKIPPEDLive page status OPEN; it lists 1 claimed proof (partial, attributed to Robert Schuh using GPT 5.6 and Kimi 2.6, submitted 2026-07-20 by 15Redstones) and CURRENTLY WORKING markers for Woett and Quanyu
SKIPPEDThe live Erdős Problems page marks #301 OPEN with 0 claimed proofs, but lists Woett and Quanyu_Tang under “Currently working on this problem”; per the collision rule, no attempt was made.
SKIPPEDexact v(1..7) = 2,2,4,11,17,103,733 and the independently verified bracket 2307 <= v(8) <= 27539; the asymptotic problem remains open.
PARTIALThe open half is reduced exactly to a growing-prime leading-digit avoidance problem, and two independent exhaustive sieves certify 10,323,214 gcd-\(1\) values through \(10^8\); infinitude remains unpr
PARTIALLive page status is OPEN with 0 claimed proofs, but jgold is marked “Currently working on this problem”; stopped under the mandatory collision rule (accessed 2026-07-26).
SKIPPEDThe live page status is OPEN, but it lists Rafikzeraoulia2025 and Ritvik_Nayak as currently working on Erdős problem #288, so the mandatory no-collision rule applies.
SKIPPEDLive page status on 2026-07-26 is FALSIFIABLE/open with 0 claimed proofs, but it lists stffp under “Currently working on this problem” (and “Interested in collaborating”); mandatory collision-avoidanc
SKIPPEDExact distinct-odd greedy termination verified for all 202,660 reduced fractions a/b with odd b<=999 (at most 27 terms), plus a rigorous reduction to the below-2/3 convention; uniform termination rema
PARTIALRigorous reduction to boundedness of H_k, FGKMT-based sublinear bound, repaired density-one proof, and independently verified exact frontier H_3(172)=76; the required uniform O(1) bound remains open.
PARTIALPositive lower density is proved for every Pisot or Salem base C (rigorous modulo Ballot–Luca), while arbitrary real C still requires the pointwise Romanoff correlation bound (6.1).
PARTIALLive page status is FALSIFIABLE/open with 0 claimed proofs, but it lists current workers jgold, alansbor, Bradford, and auro (accessed 2026-07-26), so the mandatory no-collision rule applies.
SKIPPEDExhaustive dual-algorithm computation gives exact R_D(10^j) tables through 10^9 and sharp finite-range constants, while the open asymptotic is reduced to logarithmically long holes in the short-gap in
PARTIALExact exhaustive computation proves max_{n<=10^9} f(n)=19 with four maximizers and a reproducible checker; the open asymptotic reduces to a growing-dimension uniform prime-tuple sieve bound whose fact
PARTIALLive page status is OPEN, but it lists aaryanium under “Currently working on this problem” (checked 2026-07-26), so the mandatory no-collision rule requires stopping.
SKIPPEDExact dual-sieve verification proves \(C_N\le2.23N(\log N)^2\) for every \(10\le N\le10^7\) (and \(2.15\) for \(100\le N\le10^7\)); asymptotically the unresolved input is the large-gap tail (8), while
PARTIALproved the quantitative tie bound \(E_N\ll N/\sqrt{\log N}\) modulo the standard Selberg sieve, reduced both density claims exactly to \(S_N=o(N)\), isolated a fixed admissible triple sufficient for i
PARTIALThe requested limiting ratio was never proved. Open.
NO PROGRESSThe sharp scale-local constants are \(\Delta_2,\ldots,\Delta_6=2,4,11,44,226\), with explicit checked periodic witnesses; a logarithmic lower bound for #187 would follow from the still-missing uniform
PARTIALverified a five-class near-colouring of PG(7,2) with exactly one monochromatic Fano plane and proved by a standalone exhaustive checker that every proper five-colouring is at fixed-label Hamming dista
PARTIALExhaustively verified the exact inverse-Ramsey and maximum/average independent-set tables for every triangle-free graph through 13 vertices (unique minimum ratio \(244/169>4/3\)), isolated the equival
PARTIALThe live #162 definition is ill-posed—every integer k>n is vacuously admissible, while restricting k≤n gives F(n,α)=n eventually for every α<1/2 and no admissible k at α=1/2.
FOUNDproved the exact closed form for all n=t+2 (including literal two-jump examples t=4,n=6 and t=5,n=7), verified it exhaustively, and isolated hypergraph Nikiforov as the current asymptotic wall.
PARTIALexact exhaustive recomputation gives F(1..7) = 1,0,1,6,72,2320,245765 with a no-duplicate k=7 certificate; the corrected Konyagin identity is proved, but the asymptotic log-factor gap remains open.
PARTIALErdős's largest bounty ($10,000): an actual asymptotic formula for r_k(N), the size of the largest subset of {1,...,N} with no non-trivial k-term arithmetic progression. "Probably unattackable," Erdős said — and it still is. We sent two frontier models after it independently, expecting no proof, and got no proof — but both surfaced and verified two genuine 2024–2026 breakthroughs most casual summaries (including our own brief) had gotten stale, plus a precise account of exactly why "formula" is a different kind of hard than "bounds."
NO PROOF TODAYFULL WRITE-UPVerified the published CPAP-10 from embedded ECPP certificates, computationally verified that no CPAP-7 ends by 10^9, and reduced the general case conditionally to explicit admissible linear forms; no
PARTIALLive page status OPEN, but it lists 1 claimed proof and Lherdos as currently working on the problem; mandatory no-duplication/no-collision stop.
SKIPPEDUnder the live page's literal definition, \(R(n;3,2)>\lfloor1.022^n\rfloor\) for every \(n\ge500\), and EKR strengthens this to \(R(n;3,2)\ge2^{(1/4-o(1))n}\); hence the requested \(C^{\sqrt n}\) uppe
PROVEDThe universal limit is equivalent to Erdős's finite-density formulation, and the EHS ordered 2-shift is proved to have sharp \(\Theta(n^{3/2})\) defect; exact DP gives \(\beta(S_{12})=40\).
PARTIALIndependently proved and exhaustively checked the exact thresholds \(F(2,r)=2\) and \(F(3,r)=r\) for odd \(r\), \(r+1\) for even \(r\), and isolated the density-free short-cycle-transversal versus col
PARTIALproved the first inequality for every epsilon > 0.627760438360797, reduced the k=5 lower bound 43 to 4,195 checked critical candidates, and certified R(K_2 join C_5) >= 26; both full asymptotic questi
PARTIALExact post-1601 Paley values (including \(\omega(P_{1669})=\alpha(P_{1669})=13\)) and the entropy-\(\log m+O(1)\) reduction are verified, but the required uniform strongly explicit family remains open
PARTIALLive page status “OPEN - $250”; the “Currently working on this problem” marker names Sam_Petkov (fetched via Bright Data on 2026-07-26), so the mandatory non-collision rule applies.
SKIPPEDLive page status “OPEN” with “0 claimed proofs” and no current worker, but its live discussion contains Przemek Chojecki’s explicit 12 Apr 2026 claim of a proof of the first statement; the mandatory c
SKIPPEDlive page is OPEN with no worker/claim; verified \(n\leq3\) for all countable \(\beta\) and, modulo Jones 2018, every finite \(n\) for \(\beta\leq\omega\cdot2+1\), leaving \(n\geq4,\ \beta\geq\omega\c
PARTIALLive page status OPEN; it lists one claimed partial proof (Liam Price using GPT Pro, submitted 2026-07-20, claiming the lower bound 0.38055470) and names JJ_ as currently working, so the mandatory non
SKIPPEDThe live page status is OPEN - $1000, but “Currently working on this problem” lists Emmanuel_Audigé_Y., Rynaldos, TerenceTao, and KMendoza (accessed 2026-07-26), so the mandatory no-collision rule app
SKIPPEDreduced the documented \(n=13\) frontier exactly to \(m=33,\ldots,54\) and supplied independently verified reduced witnesses with exact chromatic index in all 22 nonvacuous buckets; the universal colo
PARTIALproved an exact transition/frontier reduction and independently verified all cluster primes through 10^8 (202,208 total), but infinitude remains blocked already by the unproved H_1<=6/Maillet-level lo
PARTIALexact \(F(x)\) extrema through \(10^8\), exact short-interval parity tables, a rigorous Abel/correlation reduction, and a counterexample to anti-concentration as a sufficient intermediate target; the
PARTIALexact finite exception minima E(N) are exhaustively verified for every 1<=N<=80, with explicit witnesses and a 43,083,585-node from-scratch checker; the asymptotic problem remains open.
PARTIALexact exhaustive table through 1,117,175,146; proved computationally that 1,117,175,146 is the first integer requiring four powers, while the uniform boundedness question remains open.
PARTIALverified an explicit 420-digit member and infinite CRT family in \(A\), proved computationally that \(A\cap[1,10^9]=\{1,3\}\) with sharp exponent cap 28, and ruled out fixed local covering obstruction
PARTIALLive page status OPEN; “Currently working on this problem” lists alansbor, so no attempt was made to avoid colliding with a current worker.
SKIPPEDLive page status `OPEN - $500`; it lists `Currently working on this problem: lbattu` (and `0 claimed proofs for this problem`), so the no-collision rule requires stopping before any mathematical attem
SKIPPEDFor closed A ⊆ [−1,1], does some continuous f have A as the cluster set of the Chebyshev–Lagrange interpolation sequence L_n f(x₀)? We first shipped this as an unflagged find; it wasn't. Przemek Chojecki posted the resolution to the erdosproblems.com comment thread on 30 April, Nat Sothanaphan confirmed it the same day, and Allen Hart announced a Lean formalization in early May, also confirmed. The top-level tracker badge (OPEN, 0 claimed proofs) just hadn't caught up — we mistook a stale badge for an unflagged result because our first pass never loaded the actual comment thread. Our contribution is a genuine one, just smaller than we first framed it: an independent from-scratch Lean rebuild, on our own compute, as a second confirmation.
CLOSEDFULL WRITE-UPerdosproblems.com's own statement of #1063 is just 'estimate n_k' — open-ended, and it stays open here. What we actually proved: n_k = exp(o(k)), a genuine improvement on Cambie's exp((1+o(1))k) bound, which fills one specific formalized open target (a Google DeepMind Lean placeholder). A reader correctly called out an earlier version of this entry for reading like a full solve with no checkable proof behind it — full corrected writeup and proof now public.
LIVEFULL WRITE-UPOpen — a recent Eric Li preprint claims more; we treat it as an external candidate, not ours.
NO PROGRESSStrong partial — the universal statement remains open.
PARTIALg₃(n): the largest A⊆[n] where every integer has at most two representations as a product of two elements of A. We first shipped Rishikesh Gajjala's construction as unflagged; it wasn't — his own proof-claims submission was already on the tracker since 15 July, and so was a separate, independent, earlier claim by Colin Snyder (Star Fleet Math) giving a sharper exact constant. Our from-scratch rebuild of Gajjala's proof still stands (with a real sorry found, traced, and confirmed harmless) — Snyder's competing claim is not yet independently checked by us.
CLOSEDFULL WRITE-UPDensity of integers where every prime factor has a divisor ≡1 mod itself — Eric Li's paper pins the exact constant c=1/(2√log2). Already independently formalized twice by different people (Li himself, and separately JohanLand). We're a third, from-scratch check, not the first.
CLOSEDFULL WRITE-UPNo counterexample, no general proof. Open.
WALLA $500-prize problem (#593, characterize the finite triple systems every uncountably-chromatic triple system must contain) plus a companion (#1177, three exact-cardinal questions about avoidance classes) — both already claimed by Eric Li, already flagged by the community as warranting extra scrutiny given his pace of claims. We gave it that scrutiny: cloned the repo, built from source, ran #print axioms on all 8 component theorems plus the unconditional master theorem. Clean.
CLOSEDFULL WRITE-UPStar Fleet Math (Colin Snyder, GPT-5.6 with a custom Lean harness) has quietly submitted full proof claims for four open Erdős problems on the tracker — ten days before we noticed. We almost shipped these as our own unflagged finds, on a triage brief whose search access was blocked from seeing the tracker's proof-claims pages. We caught it before posting anything: all four (#489, #394, #336, #1188) are already on record, zero comments, zero scrutiny. So instead of "we found this," here's the honest version — an independent from-scratch rebuild of two of the four, on our own compute, as a second opinion nobody had given yet.
CLOSEDFULL WRITE-UPRound 2: proofs for 3 and 4 primitive generators. General case open.
PARTIALDecidable up to the computed range, no counterexample — general case open.
PARTIALErdős and Graham call this 'almost certainly' true but 'beyond our ability' to prove. New reciprocal-exponent budget sharpens exactly what a counterexample would need to contain, and (conditional on a real distributed prime-gap computation) the conjecture holds for every gap through 10²⁰. First problem this session came from a fresh, self-directed scout rather than a shared transcript.
LIVEFULL WRITE-UPRemote-witness obstruction unresolved; a blind reattempt corroborated the architecture, no summable bound.
WALLF(n) counts iterations of n ↦ φ(n)+1 until a prime is hit. New elementary potential-function theorem pins the leading constant to 1 (down from 5/4) and resolves the prime-square case cleanly; with Rosser–Schoenfeld, F(n) ≤ √n + (7/4)loglog n + O(1). Exponent below 1/2, and the general fixed-prime-basin question, stay open.
LIVEFULL WRITE-UPFor which f does n+f(n) hit some output range far more often than chance, for every F growing slower than f? Confirmed: Maynard's 2016 clustering theorem really does build exact, verifiable collisions of n+τ(n); the real 1985/1997 Erdős–Pomerance–Sárközy mechanism is reconstructed correctly; and the naive τ generalization of it fails for a precise, provable algebraic reason. Round 5: a genuinely new result EPS never published — for every fixed m, infinitely many y have at least m representations y=n+τ(n), rigorous modulo a real 1985 theorem, independently reverified.
LIVEFULL WRITE-UPA reduction plus a conditional construction — no resolution. Open.
NO PROGRESSGiven any finite Sidon set A, can you always extend it to a bigger one of near-(1−ε)√M density? A quantifier-correct construction reaches 1/√2, full density-1 for |A|≤2 (and |A|=3 via a named unpublished proof), and a proof that the obvious repair strategy (patch a perfect difference set) is structurally dead for seeds like Alexeev–Mixon's {1,2,4,8,13}. Round 2: the two |A|=4 patterns that provably embed in no Singer difference set turn out to embed cleanly in a different classical family instead — Singer failure wasn't the wall it looked like. Round 4: the round-3 obstruction sets do embed in Sidon spaces (rebuilt and independently verified, including a real density-value error caught along the way), but a cited nonexistence theorem shows the standard construction family is empty exactly where density-one completions would need to live. Round 5: cubic Bose–Chowla doesn't restore coverage either — a clean, verified structural negative. Round 6: two reasoners working independently converge exactly, and a fact Round 4 left unverified — zero binary critical Sidon spaces at dimension 5 — is now genuinely triple-checked.
LIVEFULL WRITE-UPNo counterexample found — search exhausted its budget. Problem open.
WALLDo sums of distinct factorials contain only finitely many perfect powers? The two-term case collapses exactly onto Brocard's equation — open since 1876. No proof, but a real quantitative bound, a fully reproduced computational sweep, and a concrete new angle on Brocard itself.
LIVEFULL WRITE-UPDo two disjoint blocks of consecutive integers with identical prime support only collide finitely often? A real structural transfer from our #677/#389 work, a sharper (partly-verified) counting bound, and a computational sweep we reproduced exactly — 16 for 16.
LIVEFULL WRITE-UPA real theorem for close prime triples, plus Maynard's sieve theorem, appears to unconditionally answer 'yes, infinitely many' to one of the page's three sub-questions. We verified everything we could — 650 sampled cases, zero disagreements — but this needs outside eyes before we call it settled.
LIVEFULL WRITE-UPk=2, k=3, and k=4 are fully closed, each independently verified — k=4 cross-checked against a real 1975 paper. k=6's overlapping case is now fully classified too (verified by independent brute force), reduced to four explicit curves for the hard disjoint case — honestly not yet closed, but the exact remaining computation is now specified.
LIVEFULL WRITE-UPErdős #389 itself stays open. Our shift conjecture got refuted by an exact counterexample — then a same-day follow-up proved an exact obstruction formula and certified a 14th minimal witness (n=28), piggybacking on a public exhaustive computation for a different Erdős problem.
LIVEFULL WRITE-UPf(n) counts the biggest strictly-increasing sequence up to n where every contiguous run sums to something different. New result: f(n) ≤ n/2 + √n + O(1) — and we didn't just check the final number, we replayed the entire proof by hand and it never once broke.
LIVEFULL WRITE-UPFour rounds in. Every leading coefficient u is reachable for SOME v, but round 4 found a genuine mod-7 wall: (7,1) specifically is unreachable by this whole construction family — real information, not just a failed search, and we caught and dropped an overreaching claim in the same return.
LIVEFULL WRITE-UPThe problem's headline question (is there ANY polynomial of degree ≥ 2 with a tiling complement?) was answered yes by Peng et al. in June 2026 for K=13, and the Lean record now cites Price's even K ≥ 6. Our July proof covers every K ≥ 3 — including cubes, which the Formal Conjectures file still lists as open and 'probably no'. Re-refereed 11 Oct 2026 by two independent passes: no gap. No human mathematician has reviewed it yet.
CLOSEDFULL WRITE-UPFound non-log-concave trees, but still unimodal — the target was never met across 11 search runs.
WALLComputational upper bounds for f(4), f(5) verified. General problem open.
PARTIALThe one that beat every model at every budget in our cross-model bench. Best outcome: an honest decline.
WALLVerifier built and checked; no verdict write-up was ever produced.
WALLEarly batch run — no verdict recovered (run JSON only).
WALLStrong partial, verified — not closed by us (Price's claimed proof is unauditable).
PARTIALComplete N=4, k=4 certificate — no integers m, n exist. Full problem stays open.
PARTIAL