Erdős problem 65 - part ii

Is the sum

\sum\frac{1}{a_i}

minimised when

G

is a complete bipartite graph? This problem is #65 in Extremal Graph Theory in the graphs problem collection.

$1,026 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-parts-ii-169fc11042da5eb778782dc0-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«65»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos65.erdos_65.parts.ii" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

∀ (k : ℝ),
  0 < k →
    ∀ (n : ℕ) (V : Type) [inst : Fintype V] (G : SimpleGraph V),
      0 < n →
        Fintype.card V = n →
          ↑G.edgeSet.ncard = k * ↑n →
            ∀ (A B : Type) [inst : Fintype A] [inst_1 : Fintype B],
              Fintype.card (A ⊕ B) = n →
                ↑(completeBipartiteGraph A B).edgeSet.ncard = k * ↑n →
                  ∑ᶠ (a : ℕ) (_ : a ∈ (completeBipartiteGraph A B).cycleLengths), 1 / ↑a ≤
                    ∑ᶠ (a : ℕ) (_ : a ∈ G.cycleLengths), 1 / ↑a

Original conjecture source: FormalConjectures/ErdosProblems/65.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:fc453ffa060cb914f7109b59f6354da3842cbad2e6ac352c3861b16155b70546
Task id: fc-v2-parts-ii-169fc11042da5eb778782dc0-formalized
Task commitment: sha256:054d1a5e7aad1cbec49a0544df7402c3795adbf4f9b94679158ec720cdc84e1a

References

erdosproblems.com/65

[GKS84] Gyárfás, A., Komlós, J. and Szemerédi, E., On the distribution of cycle lengths in graphs. J. Graph Theory (1984), 441-462.
[GPSV85] Gyárfás, A., Prömel, H. J., Szemerédi, E. and Voigt, B., On the sum of the reciprocals of cycle lengths in sparse graphs. Combinatorica (1985), 41-52.
[LiMo20] Liu, H. and Montgomery, R., A solution to Erdős and Hajnal's odd cycle problem. arXiv:2010.15802 (2020).

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord

∀ (k : ℝ), 0 < k → ∀ (n : ℕ) (V : Type) [inst : Fintype V] (G : SimpleGraph V), 0 < n → Fintype.card V = n → ↑G.edgeSet.ncard = k * ↑n → ∀ (A B : Type) [inst : Fintype A] [inst_1 : Fintype B], Fintype.card (A ⊕ B) = n → ↑(completeBipartiteGraph A B).edgeSet.ncard = k * ↑n → ∑ᶠ (a : ℕ) (_ : a ∈ (completeBipartiteGraph A B).cycleLengths), 1 / ↑a ≤ ∑ᶠ (a : ℕ) (_ : a ∈ G.cycleLengths), 1 / ↑a