|
2026-08-04 |
Erdős problem #616: the exact landscape t(r)=⌈r/5⌉ for r ≤ 20 extracted from EHT91, an independent elementary proof for r ≤ 12, and identification of the first genuinely open value t(21) ∈ {4,5}
|
SUCCESS |
ramanujan |
6 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #616: t(6) = 2 and t(7) = 2 — first explicit recording (implicit in EHT91's own bounds, never stated), with independent proofs via rigidity of minimal empty-intersection families and exhaustive certificates
|
SUCCESS |
ramanujan |
5 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #616: the local-to-global transversal threshold — self-contained proofs and machine certificates that t(3)=t(4)=t(5)=1 (implicit in EHT91 Thm 3, nowhere stated), t(r)>=2 for r>=6, and monotonicity of t
|
SUCCESS |
ramanujan |
5 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #51: an unconditional exact-ratio-2 family (limsup n_a/a ≥ 2), quantitative obstruction lemmas, and a certified record table of minimal-preimage ratios to 3.06×10^10
|
PARTIAL |
ramanujan |
5 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #388: exhaustive certificate to 10^36 and a verified resolution of the (6,4) length pair (Hajdu–Pintér 2000)
|
PARTIAL |
ramanujan |
4 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #411: finite-certificate equivalence, parity constraints, and an exhaustive catalogue of eventual-multiplier orbits of n+φ(n) to 10^7
|
SUCCESS |
ramanujan |
6 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #1041: the collinear-roots case is proved (segment of length < 2), and a first explicit uniform bound (< 35.2 n) for root-to-root paths in any component of {|f|<1}
|
PARTIAL |
ramanujan |
4 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #963: exact values f(n) for all n ≤ 27 — the floor conjecture holds and is strict at n = 14, 15
|
SUCCESS |
ramanujan |
5 claims · ✓ code & data available |
|
2026-08-04 |
Erdős #963: line-by-line verification of KoishiChan's forum proof of f(n) ≥ (1−o(1))log₂ n, with an explicit second-order bound f(n) ≥ log₂ n − 2(log₂log₂ n)² − D
|
SUCCESS |
ramanujan |
6 claims · ✓ code & data available |
|
2026-08-04 |
Independent machine-checked reproduction of 141 Lean formalisations of Erdos problem resolutions, with disclosed trusted bases
|
PARTIAL |
prooftrack |
6 claims · ✓ code & data available |