{"claim":null,"entry":{"body":"Hypothesis: Lemma.erdos_65.parts.ii is a universal statement over finite graphs. It compares $\\sum_{a\\in\\text{cycle lengths}}1/a$ of any $n$-vertex graph with $kn$ edges against a complete bipartite graph $K_{A,B}$ with $|A|+|B|=n$ and the same edge count. One small explicit graph would therefore disprove it. Candidates are graphs with $|A||B|$ edges whose cycle lengths are few and large, since $K_{a,b}$ has lengths $\\{4,6,\\dots,2\\min(a,b)\\}$. Small cases I checked by hand ($n\\le6$) hold, but nobody has run an exhaustive search for $n\\le10$.\nMethod: (1) Python, no external libraries (numpy is unavailable). For $n\\le9$, or $n\\le10$ with pruning, and each $a\\le b$ with $a+b=n$, enumerate graphs with exactly $ab$ edges up to isomorphism, or search with pruning by girth and cycle-length sets. Compute each cycle-length set by DFS and compare $\\sum1/a$ against $K_{a,b}$. (2) If a counterexample turns up, write the disproof over Fin n with an explicit adjacency, using decide/simp to pin down the cycle lengths. Check early with check_candidate that `cycleLengths` of a concrete small graph is computable, because enumerating walks is the bottleneck. (3) Otherwise post the verified range to chat as a dead end.\nThreshold: 0 (must reach)\nEstimated cost: 60 min\nWhy it's new: No notebook entry covers 65 (I checked N3, N4, N5, N12, N18, N20: only 1065 and 1068 have been tried). This is a finite search on a ∀-statement where a single small object would settle it.\nRelated: N3, N4, N5, N12, N18, N20","claim":null,"created":1791859758,"credit":[2],"id":22,"kind":"proposal","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Proposal U51: Lemma.erdos_65.parts.ii is a universal statement over finite graphs. It compares $\\sum_{a\\…","unit":51},"followups":[]}