FormalConjectures/Arxiv/2507.17780/1.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

1 declarations, 1 contain sorry, 0 declared as axioms

TxGraffiti Conjecture 1: independence, annihilation, and residue

Reference: arxiv/2507.17780 In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator by Randy Davila, Boris Brimkov, Ryan Pepper

Conjecture 1, the oldest of the four TxGraffiti conjectures in the cited collection (open since 2016), asserts that every nontrivial connected graph $G$ with maximum degree $\Delta \ge 2$ satisfies $$\alpha(G) \ge \frac{a(G) + R(G)}{\Delta(G)},$$ where $\alpha$ is the independence number, $a$ the annihilation number, $R$ the Havel–Hakimi residue, and $\Delta$ the maximum degree.

This conjecture is true, proved in arXiv:2606.29553 (C. Gupta).

Imports (1)
  1. theorem Arxiv.«2507.17780».tx_graffiti_conjecture_1 TxGraffiti Conjecture 1: for every nontrivial connected graph $G$ with $\Delta(G) \ge 2$, $$\alpha(G) \ge \frac{a(G) + R(G)}{\Delta(G)}.$$ This conjecture is true sorry line 60 source

    Source documentation

    TxGraffiti Conjecture 1: for every nontrivial connected graph $G$ with $\Delta(G) \ge 2$, $$\alpha(G) \ge \frac{a(G) + R(G)}{\Delta(G)}.$$

    This conjecture is true.

    Proof sketch. Substitute the Caro–Wei lower bound $\alpha \ge W$ for $\alpha$ and reduce to $a \le (\Delta - 1) \alpha$. The case $\Delta = 2$ is trivial ($a = \alpha$). For $\Delta \ge 4$ an AM–HM argument with $m \le (n - a)\Delta$ yields a quadratic whose discriminant is negative. For $\Delta = 3$ the annihilation number has a closed form in the degree counts $(n_1, n_2, n_3)$ and $a \le 2W$ is verified in three regimes. See arXiv:2606.29553.

    L4DEL explanation

    TxGraffiti Conjecture 1: for every nontrivial connected graph $G$ with $\Delta(G) \ge 2$, $$\alpha(G) \ge \frac{a(G) + R(G)}{\Delta(G)}.$$ This conjecture is true. Proof sketch. Substitute the Caro–Wei lower bound $\alpha \ge W$ for $\alpha$ and reduce to $a \le (\Delta - 1) \alpha$. The case $\Delta = 2$ is trivial ($a = \alpha$). For $\Delta \ge 4$ an AM–HM argument with $m \le (n - a)\Delta$ yields a quadratic whose discriminant is negative. For $\Delta = 3$ the annihilation number has a closed form in the degree counts $(n_1, n_2, n_3)$ and $a \le 2W$ is verified in three regimes. See arXiv:2606.29553.

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Nat, OfNat.ofNat, SimpleGraph.maxDegree, Real, HDiv.hDiv, HAdd.hAdd, SimpleGraph.annihilationNumber, SimpleGraph.residue, SimpleGraph.indepNum

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem tx_graffiti_conjecture_1 (V : Type) [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (_hConn : G.Connected)
    (_hDeg : 2 ≤ G.maxDegree) :
    (G.annihilationNumber + residue G : ℝ) / G.maxDegree ≤ G.indepNum := by
…