CLI toolkit for Erdős problem research: literature ingestion, RAG search, and Lean 4 formalization
Plectis: Lean research on Erdős problems. Read it at wcook04.github.io/plectis. This repository holds the website source and the earlier Python toolkit; the Lean proofs are in wcook04/plectis-erdos.
The official repository of the Nexus Resonance Codex (NRC)
Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.
Computational evidence isolating the log(n) spreadness artifact in the Erdős k=3 Sunflower Conjecture via bitmask-accelerated Simulated Annealing.
The official repository of the Nexus Resonance Codex (NRC) Protein Folding Enhancements.
Results mined from a 30,438-object ore ledger and re-checked from scratch, including one PROVED claim shown false
Open, fully rigorous re-certification of White's lower bound for Erdős's minimum-overlap problem (#36), with an independent verifier
Certified global lower-bound improvement for the Erdos minimum-overlap problem: c_E > 0.38055925 via independent Arb and MPFI checks; the exact value remains open.
An AI agent's verification-first campaign on open Erdős problems: which conjectures LLMs can actually crack, and why.
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
Erdos problem #1086: how many triangles of one area can n points in the plane span? Open. An explicit constant 6e^gamma/pi^2 = 1.0828 in the square-grid lower bound n^2 log log n (informal proof), g(5)=7, g(6)=12 (computer-assisted), and exact grid counts to 800x800.
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.
CC0 unrefereed candidate all-N determination for Erdős Problem 848, with replayable exact certificates and AI-readable evidence maps
Erdos problem #1162: the number of subgroups of S_n, and a statistical theorem on their order. Open. Exact elementary abelian counts to n=512, and a conjecture.
Explicit C4-free subgraph certificates for hypercubes Q9 through Q15 with reproducible verification.
Sidon f(7)>=24 with a running verifier, 677 covering numbers, circulant Ramsey exhaustion, and a twin-primes barrier audit
Erdos 273: covering systems with prime-minus-one moduli, parity reduction, SAT ladder, controls and correction history.
To associate your repository with the erdos-problems topic, visit your repo's landing page and select "manage topics."