Looking for a first project (Graph Theory / Combinatorics)

Stream: new members

[Cường Võ]

Hi everyone,

I've just set up Lean 4 and Mathlib on my machine. I'm looking for a 'good first issue' or a beginner-friendly project to start contributing.

My background is in C++ and I'm particularly interested in Graph Theory (e.g., paths, cycles, trees). Is there any specific lemma or theorem in this area that is missing and suitable for a beginner to formalize?

Thanks for your guidance!

[Thomas C.]

Hi!

I might have something to suggest. As discussed in an earlier thread, I just finished a small project I was working on to practice Lean, which consists in the formalization of the Kleene tree (a computable infinite binary tree that does not have a computable path).

I figured that adding a formalization of the weak Kőnig's lemma, specialized for the BinartyTree structure I implemented, would be nice.

That should be something like this:

theorem weak_konig_lemma {tree : BinaryTree} (hinf : tree.nodes.Infinite) :
  ∃ p : Path, (∀ n : ℕ, p.get_node n ∈ tree.nodes) := sorry

The project is here : https://github.com/tchaumeny/KleeneTree, in particular, if you're interested, you might want to have a look at the paper by Andrej Bauer in the References.

[Snir Broshi]

Yay, new graph theory contributor, welcome!
Compared to other fields I think there are a lot of beginner friendly graph-theory formalizations missing.
Off the top of my head:

• "any two longest paths in a preconnected graph intersect",
  using docs#SimpleGraph.Preconnected. See docs#SimpleGraph.Walk.exists_isPath_forall_isPath_length_le_length for how to say that a path is longest

• G ⊑ H → G.degree v ≤ H.degree v and G ⊑ H → G.maxDegree ≤ H.maxDegree (the weird less-than symbol is docs#SimpleGraph.IsContained) (edit: #35011)

• Change docs#SimpleGraph.Connected.connected_delete_edge_of_not_isBridge to only require Preconnected, then delete have h_conn in the proof of docs#SimpleGraph.isEdgeConnected_two
• Define maximal and maximum cliques/independent-sets in Combinatorics/SimpleGraph/Clique.lean using docs#Maximal and docs#MaximalFor respectively, and prove basic theorems about them
• Define the edge-connectivity number of a pair of vertices and of the entire graph in Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean, and prove basic theorems about them
• Menger's theorems, but that might be a pretty big project

[Snir Broshi]

You can also define and prove theorems about perfect graphs:
https://www.youtube.com/watch?v=Koc63QhxPgk
https://www.youtube.com/watch?v=fnE81FLHfcc

[Snir Broshi]

btw there's a #graph theory channel if you want to discuss how to best define stuff

[Snir Broshi]

(please let me know if you're working on one of these)

[Cường Võ]

@Thomas C. Thanks for the suggestion! The project on Weak Kőnig's lemma looks fascinating, especially the connection to computable trees. However, since I'm just starting with Lean, I think I'll stick to finite Graph Theory for my very first contribution to get comfortable with the syntax first. I might circle back to this later!

[Cường Võ]

@Snir Broshi Thank you for the warm welcome and the detailed list!

I think I will start with defining maximal/maximum cliques and independent sets, as these concepts are familiar to me from my CS classes.

Could you point me to the specific file or folder in Mathlib where I should add these definitions? I'll start by reading the existing Clique.lean file you mentioned.

[Snir Broshi]

Sounds good! I think you should add them in Clique.lean, you'll also see it already uses Maximal in a few places but without defining maximal cliques as a separate definition. As for maximums, it has definitions but they don't use the idiomatic docs#MaximalFor and should probably be replaced (unless I'm missing something that makes it not equivalent to using MaximalFor)

[Snir Broshi]

You can check out #32555 at the bottom for similar definitions (but for matchings)

[Abhinav N]

Snir Broshi said:

Yay, new graph theory contributor, welcome!
Compared to other fields I think there are a lot of beginner friendly graph-theory formalizations missing.
Off the top of my head:

• "any two longest paths in a preconnected graph intersect",
  using docs#SimpleGraph.Preconnected. See docs#SimpleGraph.Walk.exists_isPath_forall_isPath_length_le_length for how to say that a path is longest

• G ⊑ H → G.degree v ≤ H.degree v and G ⊑ H → G.maxDegree ≤ H.maxDegree (the weird less-than symbol is docs#SimpleGraph.IsContained)

• Change docs#SimpleGraph.Connected.connected_delete_edge_of_not_isBridge to only require Preconnected, then delete have h_conn in the proof of docs#SimpleGraph.isEdgeConnected_two
• Define maximal and maximum cliques/independent-sets in Combinatorics/SimpleGraph/Clique.lean using docs#Maximal and docs#MaximalFor respectively, and prove basic theorems about them
• Define the edge-connectivity number of a pair of vertices and of the entire graph in Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean, and prove basic theorems about them
• Menger's theorems, but that might be a pretty big project

We have completed the second proof and the proof that every non trivial tree has atleast 2 leaves ,we intend to raise a PR, how should we go about it?

[Snir Broshi]

Abhinav N said:

We have completed the second proof and the proof that every non trivial tree has atleast 2 leaves ,we intend to raise a PR, how should we go about it?

Nice! Can you open a PR in Mathlib?
Here's a guide if you're not familiar with git or GitHub: https://leanprover-community.github.io/contribute/git.html#open-a-pull-request

[Snir Broshi]

Also can you update your Zulip profile to include your GitHub username?

[Snir Broshi]

Cường Võ said:

I think I will start with defining maximal/maximum cliques and independent sets, as these concepts are familiar to me from my CS classes.

Hey, any updates? I've opened an issue (#34962) for it but I don't know your GitHub username.

[Chintada Srinivasa]

Hey, I am currently trying to work on:

• G ⊑ H → G.degree v ≤ H.degree v and G ⊑ H → G.maxDegree ≤ H.maxDegree.
  I have a few doubts:
  1) Does maxDegree mean that every vertex needs to have a finite neighbor set and if so, how would be prove that a vertex has a finite neighbour set using [DecidableRel G.Adj]. If not, can G technically not be a finite copy of an infinite graph?
  2) I have finished the first part G ⊑ H → G.degree v ≤ H.degree v. How can I get a code review to understand if the theorem type is what you are looking for or if you wish to rewrite the theorem.
  3) Also, should I put the theorem in Copy.lean or Finite.lean?
  Thanks.

[Snir Broshi]

Chintada Srinivasa said:

Hey, I am currently trying to work on:

• G ⊑ H → G.degree v ≤ H.degree v and G ⊑ H → G.maxDegree ≤ H.maxDegree.

Hello :wave:
Great!

Chintada Srinivasa said:

1) Does maxDegree mean that every vertex needs to have a finite neighbor set and if so, how would be prove that a vertex has a finite neighbour set using [DecidableRel G.Adj]. If not, can G technically not be a finite copy of an infinite graph?

docs#SimpleGraph.maxDegree requires [Fintype V] which means that the entire graph is finite.
What do you mean by "a finite copy of an infinite graph"? Both G and H are finite graphs, otherwise Lean won't let you talk about their maxDegree.

Chintada Srinivasa said:

2) I have finished the first part G ⊑ H → G.degree v ≤ H.degree v. How can I get a code review to understand if the theorem type is what you are looking for or if you wish to rewrite the theorem.

Nice! Can you open a PR to Mathlib?
To clarify: I don't have any authority to accept or rewrite your theorem. The list I wrote contained suggestions for things I think we should work on, but you have every right to do whatever you want. Mathlib encourages everyone to review open PRs, so if you open a PR in Mathlib I might review it with my thoughts. I have no power to accept code into Mathlib.

Chintada Srinivasa said:

3) Also, should I put the theorem in Copy.lean or Finite.lean?
Thanks.

Intuitively I'd say Finite.lean, since that's the place for stuff about degrees, but actually currently that's impossible since Copy.lean defines copies and imports the degree stuff.
So you should probably put stuff about both degrees and copies in Copy.lean, and perhaps reviewers will suggest creating a new file instead.

[Daan Deckers]

Snir Broshi said:

Yay, new graph theory contributor, welcome!
Compared to other fields I think there are a lot of beginner friendly graph-theory formalizations missing.
Off the top of my head:

• "any two longest paths in a preconnected graph intersect",
  using docs#SimpleGraph.Preconnected. See docs#SimpleGraph.Walk.exists_isPath_forall_isPath_length_le_length for how to say that a path is longest

• G ⊑ H → G.degree v ≤ H.degree v and G ⊑ H → G.maxDegree ≤ H.maxDegree (the weird less-than symbol is docs#SimpleGraph.IsContained)

• Change docs#SimpleGraph.Connected.connected_delete_edge_of_not_isBridge to only require Preconnected, then delete have h_conn in the proof of docs#SimpleGraph.isEdgeConnected_two
• Define maximal and maximum cliques/independent-sets in Combinatorics/SimpleGraph/Clique.lean using docs#Maximal and docs#MaximalFor respectively, and prove basic theorems about them
• Define the edge-connectivity number of a pair of vertices and of the entire graph in Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean, and prove basic theorems about them
• Menger's theorems, but that might be a pretty big project

Hello, I am also a beginner interested in contributing to graph theory. And I was wondering if these (including perfect graphs, excluding the ones Cường Võ is working on) are still in need of formalization. And if not, what would you consider good projects relating to this field? :)

[Snir Broshi]

Daan Deckers said:

Hello, I am also a beginner interested in contributing to graph theory. And I was wondering if these (including perfect graphs, excluding the ones Cường Võ is working on) are still in need of formalization. And if not, what would you consider good projects relating to this field? :)

Hello! :wave:
Sure, AFAIK the 2nd and 4th items in the list above are claimed but the rest are still missing (I also opened an issue #34961 for the 5th item).
There are many things to do, here are a few other stuff I recently found were missing (I think):

• G.IsClique .univ → G = ⊤
• (s : Set V) → (⊤ : SimpleGraph V).IsClique s
• (⊤ : SimpleGraph (Fin n)) ⊑ G ↔ ∃ s, G.IsNClique n s (one direction should use isNClique_map_copy_top)
• ⊤.induce s = ⊤
• G.IsClique s → G.IsClique s → G.IsClique (s ∩ t)
• (s : ι → Set V) → (∀ i, G.IsClique (s i)) → G.IsClique (⋂ i, s i)

and the equivalent statements for independent sets. Also G.induce s = ⊥ ↔ G.IsIndepSet s

Edit: Clique.lean contains a lot of statements about cliques and almost nothing about independent sets. I suggest taking a few clique statements and adding the equivalent ones about independent sets.

[Daan Deckers]

I am currently looking into perfect Graph, for which I didn't see support. But thank you for the suggestions! :)