erdos-problems

Results mined from a 30,438-object ore ledger and re-checked from scratch, including one PROVED claim shown false

Erdős–Graham #411 (r=2): the Steinerberger–Hercher bridge, the base-6 cascade (axiom-free Lean), and the omega-ladder; no exceptional prime below 1.33e14. Residual gap open; retraction preserved.

Open, fully rigorous re-certification of White's lower bound for Erdős's minimum-overlap problem (#36), with an independent verifier

An observed prime-descent law for Erdos 710 with five primes held out as a live test, five sealed Hall theorems, and a closed form for the Erdos 1044 extremal family

An AI agent's verification-first campaign on open Erdős problems: which conjectures LLMs can actually crack, and why.

Lean 4 formalization of the k = 1 case of JSP-000467 / Erdős problem 577

Computational attacks on Erdos 850 and 273: a 4.6e11 exhaustion frontier, an exact parity-split reduction, full receipts, and the negative prior-art result that retired one lane

Automated frontier-model attempts at every open Erdős problem — verdicts, completeness scores, full transcripts.

Paper and partial Lean 4 formalization for a p^(8/15) lower bound on factorial residues modulo a prime

Lean 4.34 formalization of a shrinking-window theorem for 5-smooth subset sums

Erdos 850: radical-coincidence search, exact difference lemma, finite frontier receipts and independently replayed controls.

Complete if-and-only-if classifications of Erdos-Straus solutions with arithmetic or geometric progression denominators. Verifiers exit 0.

Erdos 273: covering systems with prime-minus-one moduli, parity reduction, SAT ladder, controls and correction history.

Papers (v1.0) with data and code (data release 1) on consecutive powerful numbers, Pell equations, and Erdős problems #364 and #365

Machine-verified Lean 4 proofs from the UNICO/NOUS autonomous certification pipeline, including the geometric formalization of Morley's trisector theorem (Wiedijk #84)

Lean 4 proof of the higher-dimensional Erdős distinct-distances bound (Erdos distinct distances): n points in R^d, d ≥ 3, determine at least c_d n^(2/d) distinct distances, and this order is sharp; formalization with Mathlib

Citation-audited proof note on the Rademacher formulation of Erdős Problem #521

CC0 unrefereed candidate all-N determination for Erdős Problem 848, with replayable exact certificates and AI-readable evidence maps

Kernel-certified verification of Erdős problem 364 (three consecutive powerful numbers) to 10^14, with axioms limited to propext, Classical.choice and Quot.sound.

AI trying to tackle erdos problems