∑ Math Proof Playground › Research › Erdős problems

Erdős problem campaign

A comprehensive record of exact Formal Conjectures variants, independently verified external results, and still-open arithmetic and combinatorial campaigns.

Status at a glance

ProblemWhat is establishedWhat remains
602Exact countable-index variant proved in LeanUpstream review/merge
865Exact theorem bridged to an external complete proof and kernel checkedAttribution-preserving upstream acceptance
1150Parseval lower-bound variant proved in LeanMain (1+c)√n conjecture remains open
885Large proof-oriented arithmetic-geometry campaignComplete determination of rational points / missing column
366Large negative computation over 3-full candidatesNo proof or witness; problem remains open

Erdős 602 — countable-index Bernstein coloring variant

Exact Lean theoremGreen CI

For each infinite set A i, recursively choose two fresh points outside all previously selected points. Color the second point blue and every other point red. Global freshness forces every A i to contain both colors.

The proof is stronger than the repository assumptions: it needs only infinitude of each set; the extra countability and intersection hypotheses are unused.

The exact HasPropertyB ℕ A statement was rechecked after an earlier witness-shape mismatch was caught. The corrected source compiles without sorryAx.

CRL PR #4

Erdős 865 — exact-statement bridge

External resultIndependent kernel verification

The pinned external formalization proves the explicit finite implication

5·N + 53 < 8·|A| ⇒ A contains the required pairwise-sum triple.

The CRL wrapper derives the exact eventual real-valued Formal Conjectures theorem with the explicit constant C=7.

The underlying solution is not original to CRL. It is attributed to Jay Yang and the Cipollini / GPT-5.5 Pro solution. This project contributes the exact-statement bridge, pinned dependency, and independent audit harness.

CRL PR #3

Erdős 1150 — Parseval lower-bound variant

Exact Lean variant provedMain conjecture open

For a degree-n complex polynomial with coefficients in {−1,1}, the formal development proves

sup_{|z|=1} |P(z)| ≥ √(n+1).

The proof establishes character orthogonality and discrete Parseval on ZMod (n+1), extracts a large Fourier coefficient, identifies it with evaluation at a root of unity, and transfers the bound to the unit-circle supremum.

Boundary: this closes only the textbook Parseval variant. The research conjecture asking for a uniform factor (1+c)√n remains open.

CRL PR #2

Erdős 885 — square-addition arrays

Advanced computational progressNot solved

The campaign moved beyond bounded brute force to proof-capable arithmetic geometry. Work products include:

  • 18 normalized 5×4 square-addition packets;
  • exact genus-5 models and five elliptic quotient factors per packet;
  • minimal models, torsion, root numbers, conductors, generators, and proof-aware rank screens;
  • good-prime and bad-prime local tests;
  • mod-4, mod-8, mod-16, and isolated mod-32 Mordell–Weil sieve stages;
  • exact classification of stationary ghost vectors;
  • a unified fixed-basis recomputation correcting basis-dependent class labels and affine sign counts;
  • a current attempt to certify the known image subgroup through the product 2-Selmer localization kernel over Q₂.

The mod-8 and mod-32 stages each tested 7,340,032 lifted candidates in sparse five-factor compatibility computations. These are proof-oriented filters, not a proof that no missing column exists.

Current PR #16 · all Erdős 885 PRs

No PR in this campaign is labeled as a solution. Heuristic ranks, bounded searches, and local sieves are kept separate from certified global rational-point arguments.

Erdős 366 — computational exclusion

Negative computationStill open

An exact search checked 9,718,456 relevant 3-full candidates without finding a witness. This is substantial evidence and a reusable computational result, but it is not an exhaustive proof over the infinite search space.

Publication priority

  1. Submit the exact, green Lean variants 602 and 1150 through minimal upstream patches.
  2. Keep 865 attribution explicit and present it as independent exact-statement verification.
  3. Publish Erdős 885 only as a reproducible research computation until the global rational-point criterion is complete.
← Research dashboard · Erdős Problems database