Preprint disproving the general asymptotic conjecture in
Erdős Problem #917 at
With Elan installed, run from the repository root:
lake exe cache get lake build lake env lean checks/Check.lean LEAN_NUM_THREADS=2 lake env leanchecker Erdos917
The main theorem is
Erdos917.f12_not_density_below_two_fifths:
for every real
-
edgeCount: the number of unordered edges. -
IsEdgeCritical: criticality under Problem 917's edge-deletion convention. -
f12: the maximum edge count of a twelve-critical graph on$n$ vertices under this convention, or0ドル$ when the class is empty.
checks/Check.lean verifies that the axiom dependencies are
propext, Classical.choice, and Quot.sound.
Erdos917.not_density_three_eighths
gives the particular case
The AEHK family is constructed in Lean over finite fields, so the main theorem
carries no external mathematical hypothesis. The manuscript's final remark extends
the construction to other chromatic numbers; the Lean development covers
| Manuscript argument | Lean source |
|---|---|
| Lemma 2: active colors, prescribed singleton, module-edge deletions | Module.lean |
| Eleven-color impossibility | Assembly.lean, not_eleven_colorable |
| Proposition 3, exact edge formula and lower bound | EdgeCount.lean, conversion_edgeCount |
| Density limit from the edge formula | Density.lean, density_limit_of_parameters |
| Lemma 4: finite geometry, clique exclusion, saturation | Geometry.lean, Cliques.lean, Triangles.lean |
| Lemma 4: order and exact degrees | Degrees.lean |
| Theorem 1 and the extremal-function consequence | Family.lean |
The proofs and the first draft were generated with GPT-6 Astra; GPT-5.6 Sol and Claude Opus 5 were used for editorial review; the explicit verification of the AEHK construction and the Lean formalization were developed with OpenAI Codex (GPT-6). The author checked the arguments and is responsible for the content.