Zulip Chat Archive

Stream: new members

Topic: Basic graph theory


view this post on Zulip modderme123 (Sep 16 2020 at 19:40):

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?

view this post on Zulip Kyle Miller (Sep 16 2020 at 19:54):

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.

view this post on Zulip Kyle Miller (Sep 16 2020 at 19:57):

(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).)

view this post on Zulip Kyle Miller (Sep 16 2020 at 20:09):

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

view this post on Zulip Kyle Miller (Sep 16 2020 at 20:11):

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

view this post on Zulip Kyle Miller (Sep 16 2020 at 22:40):

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

view this post on Zulip Kyle Miller (Sep 16 2020 at 22:41):

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!

view this post on Zulip Kyle Miller (Sep 16 2020 at 22:43):

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

view this post on Zulip modderme123 (Sep 16 2020 at 22:46):

Wow, this is awesome!

view this post on Zulip Kyle Miller (Sep 16 2020 at 23:10):

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

view this post on Zulip toc (Sep 17 2020 at 05:54):

@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.

view this post on Zulip Anton Lorenzen (Sep 22 2020 at 13:23):

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

view this post on Zulip Kyle Miller (Sep 22 2020 at 17:15):

Done!

view this post on Zulip Thomas Lehéricy (Oct 10 2020 at 12:42):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 13:02):

Welcome Thomas!

view this post on Zulip Patrick Massot (Oct 10 2020 at 13:03):

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

view this post on Zulip Thomas Lehéricy (Oct 10 2020 at 13:13):

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.

view this post on Zulip Kyle Miller (Oct 10 2020 at 19:25):

@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.

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 19:27):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 19:27):

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

view this post on Zulip Kyle Miller (Oct 10 2020 at 19:34):

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

view this post on Zulip Kyle Miller (Oct 10 2020 at 19:36):

@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.

view this post on Zulip Jalex Stark (Oct 10 2020 at 19:43):

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.

view this post on Zulip Kyle Miller (Oct 10 2020 at 19:44):

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.

view this post on Zulip Jalex Stark (Oct 10 2020 at 19:45):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 19:48):

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?

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 19:53):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 19:54):

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

view this post on Zulip Kyle Miller (Oct 10 2020 at 19:54):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 19:54):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 19:55):

Weird.

view this post on Zulip Patrick Massot (Oct 10 2020 at 19:55):

I force reloaded the page and it works now!

view this post on Zulip Kyle Miller (Oct 10 2020 at 19:57):

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.)

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 20:01):

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.

view this post on Zulip Kyle Miller (Oct 10 2020 at 20:04):

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

view this post on Zulip Joseph Myers (Oct 10 2020 at 23:00):

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.

view this post on Zulip Kevin Buzzard (Oct 10 2020 at 23:10):

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.

view this post on Zulip Kyle Miller (Oct 10 2020 at 23:16):

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.

view this post on Zulip Joseph Myers (Oct 10 2020 at 23:27):

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).

view this post on Zulip Haden Hooyeon Lee (Nov 16 2020 at 01:27):

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!

view this post on Zulip Johan Commelin (Nov 16 2020 at 06:58):

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

view this post on Zulip Johan Commelin (Nov 16 2020 at 06:59):

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

view this post on Zulip Mario Krenn (Jan 04 2021 at 02:57):

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!

view this post on Zulip Thomas Browning (Jan 04 2021 at 03:16):

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.

view this post on Zulip Mario Krenn (Jan 04 2021 at 03:29):

Oh super interesting. How could i join?

view this post on Zulip Mario Carneiro (Jan 04 2021 at 03:30):

it's not really secret anymore

view this post on Zulip Mario Carneiro (Jan 04 2021 at 03:30):

you can find it in the zulip stream list

view this post on Zulip Mario Carneiro (Jan 04 2021 at 03:31):

#graph theory

view this post on Zulip Mario Krenn (Jan 04 2021 at 03:35):

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

view this post on Zulip Johan Commelin (Jan 04 2021 at 05:52):

@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.

view this post on Zulip Mario Krenn (Jan 04 2021 at 09:02):

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!

view this post on Zulip Johan Commelin (Jan 04 2021 at 14:25):

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

view this post on Zulip Bhavik Mehta (Jan 04 2021 at 14:31):

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

view this post on Zulip Johan Commelin (Jan 04 2021 at 14:33):

That's cool news!

view this post on Zulip Johan Commelin (Jan 04 2021 at 14:33):

That was indeed the main missing bit.

view this post on Zulip Kyle Miller (Jan 04 2021 at 20:45):

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!

view this post on Zulip Eric Rodriguez (Mar 26 2021 at 14:16):

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

view this post on Zulip Yakov Pechersky (Mar 26 2021 at 14:25):

Maybe we can use the new set_like to define them

view this post on Zulip Yakov Pechersky (Mar 26 2021 at 14:26):

And give set_like some additional power about closure

view this post on Zulip Eric Rodriguez (Mar 26 2021 at 14:32):

is this what you're on about?

view this post on Zulip Eric Rodriguez (Mar 26 2021 at 14:32):

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

view this post on Zulip Eric Rodriguez (Mar 26 2021 at 14:33):

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

view this post on Zulip David Wärn (Mar 26 2021 at 14:38):

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

view this post on Zulip Eric Rodriguez (Mar 26 2021 at 14:51):

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

view this post on Zulip Heather Macbeth (Mar 27 2021 at 00:56):

@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.


Last updated: May 13 2021 at 22:15 UTC