# Zulip Chat Archive

## Stream: new members

### Topic: Basic graph theory

#### 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?

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

#### 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)`

.)

#### 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
```

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

#### 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
```

#### 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!

#### 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
```

#### modderme123 (Sep 16 2020 at 22:46):

Wow, this is awesome!

#### 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
```

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

#### Anton Lorenzen (Sep 22 2020 at 13:23):

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

#### Kyle Miller (Sep 22 2020 at 17:15):

Done!

#### Thomas Lehéricy (Oct 10 2020 at 12:42):

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

#### Patrick Massot (Oct 10 2020 at 13:02):

Welcome Thomas!

#### Patrick Massot (Oct 10 2020 at 13:03):

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

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

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

#### 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?

#### Patrick Massot (Oct 10 2020 at 19:27):

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

#### Kyle Miller (Oct 10 2020 at 19:34):

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

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

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

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

#### 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

#### 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?

#### 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

#### Patrick Massot (Oct 10 2020 at 19:54):

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

#### Kyle Miller (Oct 10 2020 at 19:54):

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

#### Bryan Gin-ge Chen (Oct 10 2020 at 19:54):

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

#### Patrick Massot (Oct 10 2020 at 19:55):

Weird.

#### Patrick Massot (Oct 10 2020 at 19:55):

I force reloaded the page and it works now!

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

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

#### 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

#### Joseph Myers (Oct 10 2020 at 23:00):

Kyle Miller said:

A finite simple graph is

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

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

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

#### 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!

#### 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

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

#### 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!

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

#### Mario Krenn (Jan 04 2021 at 03:29):

Oh super interesting. How could i join?

#### Mario Carneiro (Jan 04 2021 at 03:30):

it's not really secret anymore

#### Mario Carneiro (Jan 04 2021 at 03:30):

you can find it in the zulip stream list

#### Mario Carneiro (Jan 04 2021 at 03:31):

#### Mario Krenn (Jan 04 2021 at 03:35):

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

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

#### 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!

#### Johan Commelin (Jan 04 2021 at 14:25):

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

#### 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

#### Johan Commelin (Jan 04 2021 at 14:33):

That's cool news!

#### Johan Commelin (Jan 04 2021 at 14:33):

That was indeed the main missing bit.

#### 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!

#### 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

#### Yakov Pechersky (Mar 26 2021 at 14:25):

Maybe we can use the new `set_like`

to define them

#### Yakov Pechersky (Mar 26 2021 at 14:26):

And give `set_like`

some additional power about `closure`

#### Eric Rodriguez (Mar 26 2021 at 14:32):

is this what you're on about?

#### Eric Rodriguez (Mar 26 2021 at 14:32):

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

#### 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

#### 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

#### 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

#### 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