Basic graph theory

Stream: new members

[modderme123]

So I learned a little bit of lean through the natural numbers game, and I thought I would try to prove some basic graph theory proofs. I'm trying to prove that twice the sum of the edges is equal to the sum of the degrees in a simple graph. So far I have defined a graph (I've also created a complete graph and shown that is a graph), but I got stuck on the sum_degrees theorem

structure graph := (V : ℕ)
  (E : ℕ → ℕ → bool)
  (E_irreflexive : forall x : ℕ, x < V → ¬ E x x)
  (E_symmetric : forall x y : ℕ, x < V ∧ y < V → E x y → E y x)

def sum_fun : (nat → nat) -> nat → nat
| m 0 := 0
| m (nat.succ n) := m(n) + sum_fun(m)(n)

def edges (G : graph) : nat := begin
  have sum := λ x, (sum_fun (λ y, if G.E x y then 1 else 0) x),
  exact sum_fun (sum) (G.V)
end

def degree (G : graph) (x : nat) : nat := begin
  have check_edge := λ y, if G.E x y then 1 else 0,
  exact if x < G.V then sum_fun check_edge (G.V) else 0
end

theorem sum_degrees (G : graph) : sum_fun (degree G) (G.V) = 2 * (edges G) :=
begin
  sorry
end

Any advice on how to start this theorem?

[Kyle Miller]

A way I've proved this is with a combinatorial proof. You can introduce an intermediate object, a dart, which is an ordered pair of adjacent vertices. A dart is at a vertex if the vertex is the first entry of the pair, and you can show that the number of darts at a vertex is equal to the degree of the vertex --- then since darts are partitioned into which vertices they're at, you have the number of darts is equal to the sum of degrees. There is a two-to-one map that sends darts to their corresponding edges, so the number of darts is equal to twice the number of edges.

[Kyle Miller]

(Let me know if you want to be added to the private Zulip graph theory stream. There are a number of people working on formalizing graph theory in Lean. Also, right now you can use the combinatorics.simple_graph library, which defines things like simple graphs and the degree of a vertex for a (locally) finite graph. Your definition of a graph when V = n would be equivalent to simple_graph (fin n).)

[Kyle Miller]

Looking more carefully at your definitions, it looks like edges is counting the number of darts. Adding in a definition that counts the number of edges, too, you might be able to use this setup:

structure graph := (V : ℕ)
(E : ℕ → ℕ → bool)
(E_irreflexive : ∀ x : ℕ, x < V → ¬ E x x)
(E_symmetric : ∀ x y : ℕ, x < V ∧ y < V → E x y → E y x)

def sum_fun : (ℕ → ℕ) -> ℕ → ℕ
| m 0 := 0
| m (n + 1) := m n + sum_fun m n

def edges (G : graph) : ℕ :=
let sum := λ x, sum_fun (λ y, if x < y ∧ G.E x y then 1 else 0) x
in sum_fun sum G.V

def degree (G : graph) (x : ℕ) : ℕ :=
let check_edge := λ y, if G.E x y then 1 else 0
in sum_fun check_edge G.V

def darts (G : graph) : ℕ :=
let sum := λ x, sum_fun (λ y, if G.E x y then 1 else 0) x
in sum_fun sum G.V

lemma darts_eq_twice_edges (G : graph) : darts G = 2 * edges G :=
begin
  sorry
end

lemma darts_eq_sum_degrees (G : graph) : darts G = sum_fun (degree G) G.V :=
begin
  sorry
end

theorem sum_degrees (G : graph) : sum_fun (degree G) G.V = 2 * edges G :=
begin
  rw ←darts_eq_sum_degrees,
  rw ←darts_eq_twice_edges,
end

[Kyle Miller]

You'll have to prove a number of lemmas about sum_fun for transforming sums of indicator functions, I think.

[Kyle Miller]

To get you started, I proved darts_eq_twice_edges and added a number of lemmas for sum_fun. This also shows off a nice feature of Lean, where you can introduce your own notation --- I adapted the summation notation from algebra.big_operators for your sum_fun.

import tactic

structure graph := (V : ℕ)
(E : ℕ → ℕ → bool)
(E_irreflexive : ∀ x : ℕ, x < V → ¬ E x x)
(E_symmetric : ∀ x y : ℕ, x < V → y < V → E x y → E y x)

def sum_fun : (ℕ → ℕ) -> ℕ → ℕ
| m 0 := 0
| m (n + 1) := m n + sum_fun m n

notation `∑` binders ` to ` n `, ` r:(scoped:67 f, sum_fun f n) := r
-- this means `∑ x to n, foo` denotes `sum_fun (λ x, foo) n`
-- the `∑` is entered using \sum

def edges (G : graph) : ℕ :=
∑ x to G.V, ∑ y to x, if G.E x y then 1 else 0

def degree (G : graph) (x : ℕ) : ℕ :=
∑ y to G.V, if G.E x y then 1 else 0

def darts (G : graph) : ℕ :=
∑ x to G.V, ∑ y to G.V, if G.E x y then 1 else 0

@[simp]
lemma sum_to_zero_eq (f : ℕ → ℕ) : ∑ x to 0, f x = 0 := rfl

@[simp]
lemma sum_zero_eq (n : ℕ) : ∑ x to n, 0 = 0 :=
begin
  induction n,
  rw sum_to_zero_eq,
  dunfold sum_fun,
  rw n_ih,
end

lemma sum_add_eq_add_sum (f g : ℕ → ℕ) (n : ℕ) :
  ∑ x to n, (f x + g x) = ∑ x to n, f x + ∑ x to n, g x :=
begin
  induction n,
  { simp, },
  { dunfold sum_fun,
    rw n_ih,
    ring, }
end

lemma sum_if_true (f g : ℕ → ℕ) (p : ℕ → Prop) [decidable_pred p] (n : ℕ) (h : ∀ x, x < n → p x) :
  ∑ x to n, (if p x then f x else g x) = ∑ x to n, f x :=
begin
  induction n,
  { simp },
  { dunfold sum_fun,
    have k := h n_n (lt_add_one _),
    simp [k],
    rw n_ih,
    intros x hlt, apply h, exact nat.lt.step hlt, }
end

lemma sum_if_false (f g : ℕ → ℕ) (p : ℕ → Prop) [decidable_pred p] (n : ℕ) (h : ∀ x, x < n → ¬ p x) :
  ∑ x to n, (if p x then f x else g x) = ∑ x to n, g x :=
begin
  induction n,
  { simp },
  { dunfold sum_fun,
    have k := h n_n (lt_add_one _),
    simp [k],
    rw n_ih,
    intros x hlt, apply h, exact nat.lt.step hlt, }
end

lemma sum_delta (f : ℕ → ℕ) (n x : ℕ) (h : x < n) :
  ∑ y to n, (if y = x then f y else 0) = f x :=
begin
  induction n generalizing x,
  { simp, exfalso, linarith [h] },
  { dunfold sum_fun,
    by_cases h' : n_n = x,
    { subst n_n, simp,
      rw sum_if_false,
      simp,
      intro y, intros hlt heq, subst heq, exact nat.lt_asymm hlt hlt, },
    { rw n_ih, simp [h'],
      cases h, exfalso, apply h', refl, exact h_a, } }
end

lemma sum_fun_restrict' (f : ℕ → ℕ) (n m : ℕ) :
  ∑ x to n, f x = ∑ x to n + m, if x < n then f x else 0 :=
begin
  induction m,
  { rw sum_if_true,
    simp, simp, },
  { rw nat.add_succ,
    dunfold sum_fun,
    rw ←m_ih,
    split_ifs,
    exfalso, linarith,
    simp, },
end

lemma sum_fun_restrict (f : ℕ → ℕ) (n m : ℕ) (h : n ≤ m) :
  ∑ x to n, f x = ∑ x to m, if x < n then f x else 0 :=
begin
  rw sum_fun_restrict' f n (m - n),
  rw nat.add_sub_of_le h,
end

lemma sum_congr (f g : ℕ → ℕ) (n : ℕ) (h : ∀ x < n, f x = g x) :
  ∑ x to n, f x = ∑ x to n, g x :=
begin
  induction n,
  { simp },
  { dunfold sum_fun,
    rw [h, n_ih],
    intros x h', apply h, apply nat.lt.step h',
    apply lt_add_one, },
end

lemma swap_sum (f : ℕ → ℕ → ℕ) (n m : ℕ) : ∑ x to n, ∑ y to m, f x y = ∑ y to m, ∑ x to n, f x y :=
begin
  induction n generalizing m,
  { simp, },
  { dunfold sum_fun,
    rw sum_add_eq_add_sum,
    rw n_ih, }
end

lemma darts_eq_twice_edges (G : graph) : darts G = 2 * edges G :=
begin
  dsimp only [darts, edges],
  have key := λ x (h : x < G.V), sum_fun_restrict (λ y, if G.E x y then 1 else 0) x G.V (by linarith),
  dsimp at key,
  rw sum_congr _ _ _ key, clear key,
  simp,
  have key : ∀ x, ∀ y < G.V, (if y < x then (if G.E x y then 1 else 0) else 0) = (if y < x ∧ G.E x y then 1 else 0),
  { intros x y yel, split_ifs; try { refl <|> { exfalso, cc } }, },
  have key' : ∀ x < G.V, ∑ y to G.V, (if y < x then (if G.E x y then 1 else 0) else 0) = ∑ y to G.V, (if y < x ∧ G.E x y then 1 else 0),
  { intros x xel,
    rw sum_congr _ _ _ (key x), },
  rw sum_congr _ _ _ key', clear key key',
  have key : ∀ x < G.V, ∀ y < G.V, (if G.E x y then 1 else 0) = (if x < y ∧ G.E y x then 1 else 0) + (if y < x ∧ G.E x y then 1 else 0),
  { intros x xel y yel,
    by_cases h : (G.E x y : Prop),
    have h' := G.E_symmetric x y xel yel h,
    simp [h, h'],
    split_ifs; try { refl <|> { exfalso, cc } },
    exfalso, apply nat.lt_asymm h_1 h_2,
    exfalso, push_neg at h_1, push_neg at h_2,
    rw le_iff_eq_or_lt at h_1 h_2,
    cases h_1; cases h_2; try { subst x }; try { subst y }; try { apply G.E_irreflexive _ yel h },
    apply nat.lt_asymm h_1 h_2,
    have h' : ¬ G.E y x,
    { revert h, contrapose, push_neg, exact G.E_symmetric y x yel xel },
    simp [h, h'], },
  have key' : ∀ x < G.V, ∑ y to G.V, (if G.E x y then 1 else 0) = ∑ y to G.V, (if x < y ∧ G.E y x then 1 else 0) + ∑ y to G.V, (if y < x ∧ G.E x y then 1 else 0),
  { intros x xel,
    rw sum_congr _ _ _ (key x xel),
    rw sum_add_eq_add_sum, },
  rw sum_congr _ _ _ key', clear key key',
  rw sum_add_eq_add_sum,
  rw swap_sum, dsimp,
  exact (two_mul _).symm,
end

lemma darts_eq_sum_degrees (G : graph) : darts G = ∑ x to G.V, degree G x :=
begin
  sorry
end

theorem sum_degrees (G : graph) : ∑ x to G.V, degree G x = 2 * edges G :=
begin
  rw ←darts_eq_sum_degrees,
  rw ←darts_eq_twice_edges,
end

[Kyle Miller]

I'm sure the proof can be simplified by quite a bit. It's just suggesting that there aren't enough lemmas to manipulate sum_fun yet!

[Kyle Miller]

Oh, that's funny. I didn't realize that everything was set up to completely prove it! It's just

lemma darts_eq_sum_degrees (G : graph) : darts G = ∑ x to G.V, degree G x := rfl

[modderme123]

Wow, this is awesome!

[Kyle Miller]

Found a way to simplify it somewhat. Using apply sum_congr makes it so Lean tells you what needs to be proved, rather you than needing to tell Lean the statement with have.

import tactic

structure graph := (V : ℕ)
(E : ℕ → ℕ → bool)
(E_irreflexive : ∀ x : ℕ, x < V → ¬ E x x)
(E_symmetric : ∀ x y : ℕ, x < V → y < V → E x y → E y x)

def sum_fun : (ℕ → ℕ) -> ℕ → ℕ
| m 0 := 0
| m (n + 1) := m n + sum_fun m n

notation `∑` binders ` to ` n `, ` r:(scoped:67 f, sum_fun f n) := r
-- this means `∑ x to n, foo` denotes `sum_fun (λ x, foo) n`
-- the `∑` is entered using \sum

def edges (G : graph) : ℕ :=
∑ x to G.V, ∑ y to x, if G.E x y then 1 else 0

def degree (G : graph) (x : ℕ) : ℕ :=
∑ y to G.V, if G.E x y then 1 else 0

def darts (G : graph) : ℕ :=
∑ x to G.V, ∑ y to G.V, if G.E x y then 1 else 0

@[simp]
lemma sum_to_zero_eq (f : ℕ → ℕ) : ∑ x to 0, f x = 0 := rfl

@[simp]
lemma sum_zero_eq (n : ℕ) : ∑ x to n, 0 = 0 :=
begin
  induction n,
  rw sum_to_zero_eq,
  dunfold sum_fun,
  rw n_ih,
end

lemma sum_add_eq_add_sum (f g : ℕ → ℕ) (n : ℕ) :
  ∑ x to n, (f x + g x) = ∑ x to n, f x + ∑ x to n, g x :=
begin
  induction n,
  { simp, },
  { dunfold sum_fun,
    rw n_ih,
    ring, }
end

lemma sum_if_true (f g : ℕ → ℕ) (p : ℕ → Prop) [decidable_pred p] (n : ℕ) (h : ∀ x, x < n → p x) :
  ∑ x to n, (if p x then f x else g x) = ∑ x to n, f x :=
begin
  induction n,
  { simp },
  { dunfold sum_fun,
    have k := h n_n (lt_add_one _),
    simp [k],
    rw n_ih,
    intros x hlt, apply h, exact nat.lt.step hlt, }
end

lemma sum_if_false (f g : ℕ → ℕ) (p : ℕ → Prop) [decidable_pred p] (n : ℕ) (h : ∀ x, x < n → ¬ p x) :
  ∑ x to n, (if p x then f x else g x) = ∑ x to n, g x :=
begin
  induction n,
  { simp },
  { dunfold sum_fun,
    have k := h n_n (lt_add_one _),
    simp [k],
    rw n_ih,
    intros x hlt, apply h, exact nat.lt.step hlt, }
end

lemma sum_fun_restrict' (f : ℕ → ℕ) (n m : ℕ) :
  ∑ x to n, f x = ∑ x to n + m, if x < n then f x else 0 :=
begin
  induction m,
  { rw sum_if_true,
    simp, simp, },
  { rw nat.add_succ,
    dunfold sum_fun,
    rw ←m_ih,
    split_ifs,
    exfalso, linarith,
    simp, },
end

lemma sum_fun_restrict (f : ℕ → ℕ) (n m : ℕ) (h : n ≤ m) :
  ∑ x to n, f x = ∑ x to m, if x < n then f x else 0 :=
begin
  rw sum_fun_restrict' f n (m - n),
  rw nat.add_sub_of_le h,
end

lemma sum_congr (f g : ℕ → ℕ) (n : ℕ) (h : ∀ x < n, f x = g x) :
  ∑ x to n, f x = ∑ x to n, g x :=
begin
  induction n,
  { simp },
  { dunfold sum_fun,
    rw [h, n_ih],
    intros x h', apply h, apply nat.lt.step h',
    apply lt_add_one, },
end

lemma swap_sum (f : ℕ → ℕ → ℕ) (n m : ℕ) : ∑ x to n, ∑ y to m, f x y = ∑ y to m, ∑ x to n, f x y :=
begin
  induction n generalizing m,
  { simp, },
  { dunfold sum_fun,
    rw sum_add_eq_add_sum,
    rw n_ih, }
end

@[simp]
lemma indic_indic_eq_and (a b : Prop) [decidable a] [decidable b]:
  (if a then (if b then 1 else 0) else 0) = (if a ∧ b then 1 else 0) :=
begin
  split_ifs; try { refl <|> { exfalso, cc } },
end

lemma darts_eq_twice_edges (G : graph) : darts G = 2 * edges G :=
begin
  dsimp only [darts, edges],
  have key := λ x (h : x < G.V), sum_fun_restrict (λ y, if G.E x y then 1 else 0) x G.V (by linarith),
  rw sum_congr _ _ _ key, clear key,
  simp,
  rw two_mul,
  conv_rhs { congr, rw swap_sum, },
  rw ←sum_add_eq_add_sum,
  apply sum_congr,
  intros x xel,
  rw ←sum_add_eq_add_sum,
  apply sum_congr,
  intros y yel,
  by_cases h : (G.E x y : Prop),
  simp [h, G.E_symmetric x y xel yel h],
  split_ifs; try { refl <|> { exfalso, cc } },
  exfalso, exact nat.lt_asymm h_1 h_2,
  exfalso, push_neg at h_1, push_neg at h_2,
  have h' : x = y := by linarith,
  subst x, exact G.E_irreflexive _ yel h,
  have h' : ¬ G.E y x,
  { revert h, contrapose, push_neg, exact G.E_symmetric y x yel xel },
  simp [h, h'],
end

lemma darts_eq_sum_degrees (G : graph) : darts G = ∑ x to G.V, degree G x := rfl

theorem sum_degrees (G : graph) : ∑ x to G.V, degree G x = 2 * edges G :=
begin
  rw ←darts_eq_sum_degrees,
  rw ←darts_eq_twice_edges,
end

[toc]

@Kyle Miller I'd like to be added to the secret graph theory group. I'm a bit of a novice at lean still but that is (roughly) my focus.

[Anton Lorenzen]

@Kyle Miller I would also like to be part of the graph theory stream

[Kyle Miller]

Done!

[Thomas Lehéricy]

@Kyle Miller I would like to be added to the graph theory stream please!

[Patrick Massot]

Welcome Thomas!

[Patrick Massot]

Don't play too much with graphs, probability theory in mathlib needs you!

[Thomas Lehéricy]

Thank you Patrick!
I know :) I have two goals for now, one is doing a bit of deterministic planar map theory (proving some bijection between different classes of maps), and the second is to try to prove Donsker's invariance principle. Both would be useful for random planar maps. It seemed the graph theory half was more accessible as a warm-up.

[Kyle Miller]

@Thomas Lehéricy It appears you've been added! The stream has been rather quiet since the beginning of the semester, though.

I'd like the theory of combinatorial maps in general, which generalizes planar maps to graphs on surfaces of arbitrary genus (you could say a combinatorial map is a multigraph with faces attached such that the result is a closed oriented surface, possibly disconnected). I have a couple ways of encoding them, but I wanted to see how the simple graphs API would work out, to then inform the design of the multigraphs API, to then inform the design of the combinatorial maps API. Plus, many results can be lifted from one to the next, so it seems to be a good order to do things.

(Once all three exist, we can say we can state the 4-color theorem. A finite simple graph is planar if it comes from a combinatorial map of genus 0. The theorem is that every planar simple graph has a proper vertex 4-coloring.)

Somewhere I have most of the formalization of Sperner's lemma with some early attempts at multigraphs and combinatorial maps, but to finish it it'd be nice to flesh them out more.

[Bryan Gin-ge Chen]

We've got quite the backlog of PRs at the moment, but is there a plan for the next few graph theory PRs yet?

[Patrick Massot]

I still don't understand why this stream is private.

[Kyle Miller]

@Patrick Massot I'm not sure. @Jalex Stark, any reason to keep it private anymore?

[Kyle Miller]

@Bryan Gin-ge Chen Not immediately from me... Teaching and postdoc applications have taken priority... There is a quasi-plan for PRs in a post on the #graph theory stream though.

[Jalex Stark]

I think there was some value to it being private in the past and now it's clearly better as a public stream. I've made the change.

[Kyle Miller]

I've also been planning on writing up at least a blog post on the different ways of dealing with subgraphs-as-graphs so that they can be more easily evaluated. I've swapped out different designs on the simple_graphs2 branch a few times, and it's always been relatively painless, so that at least indicates that we won't be locked into a design if a better one comes up.

[Jalex Stark]

Kyle Miller said:

Jalex Stark said:

What do you think the next PR from this branch should be?

Most of simple_graph/basic.lean seems good, except for the incomplete stuff about graph operations. Some simp lemmas relating simple_graph_on to simple_graph might not make sense. Also simple_graph_from_rel_adj can probably wait.

The definitions in simple_graph/hom.lean seem fine, but the lemmas should be reviewed since the api is underutilized and seems somewhat incomplete.

simple_graph/subgraph.lean seems good, except for things about cycles and maybe induced graphs. Cardinality results should be reviewed -- there's no application of them yet so the design might not be good.

simple_graph/simple_graph_on.lean is fine enough. It could certainly be expanded, but it at least has a bounded_lattice instance.

simple_graph/degree_sum.lean is close, but I think it can still be simplified a lot given a person sufficiently competent with big_operators. It also would be nice to have an explicit handshake lemma.

I think this is the quasiplan that kyle referred to

[Patrick Massot]

Jalex Stark said:

I think there was some value to it being private in the past and now it's clearly better as a public stream. I've made the change.

Are you sure you changed it?

[Bryan Gin-ge Chen]

I no longer see a "lock" icon next to the stream: https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory

[Patrick Massot]

When I click your link, Zulip says "This stream does not exist or is private."

[Kyle Miller]

It says "public stream" in the stream settings for me

[Bryan Gin-ge Chen]

Strange: Screen-Shot-2020-10-10-at-3.54.36-PM.png

[Patrick Massot]

Weird.

[Patrick Massot]

I force reloaded the page and it works now!

[Kyle Miller]

A caveat about that plan: the graph operations of contraction/deletion of graphs are not formalized correctly to be useful for anything to do with studying graph minors yet. There's a way to encode the type of all contractions and deletions with some nice properties, but it will take some development before it's ready. (Here's the idea for matroids, where it's simpler: the type consists of a pair of subsets C and F of the ground set, where C is a subset of F. Then the way in which it is a matroid is you restrict to F and then contract by C. It seems to let you easily state relationships between contractions, deletions, and duals using equality. Graphs are somewhat more complicated because, for example, isolated vertices matter.)

[Bryan Gin-ge Chen]

I'd love to see a few matroid PRs as well. I got stuck on contractions and deletions in my old matroids repo and never had a chance to go back and figure them out.

[Kyle Miller]

@Peter Nelson and Edward Lee (who doesn't seem to be on Zulip) are still working on them

[Joseph Myers]

Kyle Miller said:

A finite simple graph is planar if it comes from a combinatorial map of genus 0.

Surely it's planar if it can be drawn in the plane without edges crossing (and likewise for embeddings in surfaces of other genus); that should be easy to state right now, and reflects what I'd think of as the common understanding of what it means for a graph to be planar. You might then need the Jordan curve theorem or related results to prove that being planar is equivalent to characterisations that are more convenient to work with combinatorially, however.

[Kevin Buzzard]

I believe that when Gonthier proved the four colour theorem in Coq he reduced everything to the setting where all paths were contained in the union of the lines x=integer and y=integer on the plane and all areas were unions of squares.

[Kyle Miller]

I knew someone would object to this characterization of planar graphs :smile:. 2D topology is very well behaved. Topological, smooth, and PL topology are basically equivalent, so, up to homeomorphism, you can just write down the cell structure, which is what the combinatorial map is. I'm pretty sure it's easier to state everything in terms of the combinatorial data of the cell structure (it can be given as two permutations on the same set, one a fixedpoint-free involution), and the genus is easy to calculate for it. Someone can then prove the correspondence between this notion of planarity and the topological one later -- I'm not sure you really gain anything by worrying about topological planarity of a graph for the 4-color theorem.

[Joseph Myers]

Cf. the discussions of how it shouldn't really matter which of several different equivalent properties is considered to be "the" definition, but formalisation forces you to pick just one (and then proving that they are all equivalent becomes part of filling out the API and justifying that your definition defines the same thing as someone else's concept of "the" definition).

[Haden Hooyeon Lee]

Hello! I just finished the natural number game (again! things have changed a lot over the past year I guess).
I'm looking for resources/tutorials that are relevant to basic graph theory. I see that #graph theory stream exists so I'm following it, but are there resources like the natural number game that can help me get my hands dirty? thanks!

[Johan Commelin]

We don't have anything like the NNG for graph theory... the NNG is pretty unique in this regard

[Johan Commelin]

graph theory is a pretty tricky subject for formalisation, because there are 37 different variations on the definition of a graph.

[Mario Krenn]

Hi! I am interested in Lean, but havent really used it, just want to understand the structures and progress atm. I am interested to see some simple graph theory in Lean mathlib. I was refered to this:
https://github.com/leanprover-community/mathlib/tree/hedetniemi/src

This branch is not included in the main repo, is it? Is there a reason for that? It seems the graph theory project in the link above hasnt been used for hte last 9months. Any plans of implementing this into the main library? Thanks!

[Thomas Browning]

There is a secret graph theory stream, I think. If you join that then you might get a clearer idea of what's going on.

[Mario Krenn]

Oh super interesting. How could i join?

[Mario Carneiro]

it's not really secret anymore

[Mario Carneiro]

you can find it in the zulip stream list

[Mario Carneiro]

#graph theory

[Mario Krenn]

great thanks! will observe a bit and hope this gives an interesting entry point :)

[Johan Commelin]

@Mario Krenn the basic stuff from the hedetniemi branch is now in mathlib. But not the stuff in the direction of Hedetniemi itself. We got stuck in some stuff about random graphs. And then I got side-tracked by tons of other stuff. I'm not actually working with graphs myself, but if someone who actually knows something about random graphs would take that on, I think it would be a lot of fun.

[Mario Krenn]

I dont know much about random graphs. But i would take a certain, simple proof in graph theory (about a property of perfect matchings) as motivation to learn using Lean. The simple property is used in quantum physics, which is my field of research, so when spending time on Lean i still can cheat myself that i work on my research :) I will come back here for sure with questions as soon as i managed the most basic examples. Thanks!

[Johan Commelin]

@Mario Krenn cool, you should certainly talk with the people in the graph theory stream (-;

[Bhavik Mehta]

Johan Commelin said:

Mario Krenn the basic stuff from the hedetniemi branch is now in mathlib. But not the stuff in the direction of Hedetniemi itself. We got stuck in some stuff about random graphs. And then I got side-tracked by tons of other stuff. I'm not actually working with graphs myself, but if someone who actually knows something about random graphs would take that on, I think it would be a lot of fun.

Since I had recent success with probability in combinatorics with the ballot problem and past success in using random graphs to show lower Ramsey bounds, I'm working on showing that there are graphs with arbitrarily high girth and chromatic number (which I think was the missing bit in Hedetniemi?) together with @Alena Gusakov

[Johan Commelin]

That's cool news!

[Johan Commelin]

That was indeed the main missing bit.

[Kyle Miller]

Mario Krenn said:

I dont know much about random graphs. But i would take a certain, simple proof in graph theory (about a property of perfect matchings) as motivation to learn using Lean. The simple property is used in quantum physics, which is my field of research, so when spending time on Lean i still can cheat myself that i work on my research :) I will come back here for sure with questions as soon as i managed the most basic examples. Thanks!

Perfect matchings for simple graphs recently were added to mathlib docs#simple_graph.matching.is_perfect (there are some branches that have some more code that should get PRd sometime soon). What about perfect matchings are you interested in formalizing? Feel free to answer this in a new topic over at #graph theory!

[Eric Rodriguez]

Has there been any progress on subgraphs? I'd find it useful for some code I'm writing, and am happy to help with the PR, but not sure what the possible approaches are and the advantages/disadvantages

[Yakov Pechersky]

Maybe we can use the new set_like to define them

[Yakov Pechersky]

And give set_like some additional power about closure

[Eric Rodriguez]

is this what you're on about?

[Eric Rodriguez]

wait I can say #6768 and that links it I think

[Eric Rodriguez]

that seems really useful if it works though, sub objects have been more annoying than expected the few times that I've used them

[David Wärn]

@Eric Rodriguez what kind of subgraphs do you have in mind? set_like should be good for induced subgraphs

[Eric Rodriguez]

I wanted the general-case (I'm studying a graph parameter that is monotonic on subgraphs) but it's no big deal regardless; there was one comment a while ago:

Kyle Miller said:

I've also been planning on writing up at least a blog post on the different ways of dealing with subgraphs-as-graphs so that they can be more easily evaluated. I've swapped out different designs on the simple_graphs2 branch a few times, and it's always been relatively painless, so that at least indicates that we won't be locked into a design if a better one comes up.

that mentioned there was issues with different approaches so wanted to see what they were before getting stuck in writing code

[Heather Macbeth]

@Eric Rodriguez -- @Peter Nelson has been working with matroids, including submatroids, contraction, deletion, etc, using the following definition:
https://github.com/e45lee/lean-matroids/blob/master/src/matroid/submatroid/matroid_in.lean#L18
Maybe he can comment on whether this would be a good choice for graphs.