Getting Started

Stream: graph theory

[Aatman Supkar]

Hi! I am new to Lean and I wanted to start working on graph theory, but I have plans exclusively for finite graphs. Are there previous works in particular that I should know before I start?

[Kevin Buzzard]

To get a feeling for what mathlib already has, you might want to go to the mathlib docs here and then click around on the left in the Mathlib/Combinatorics/SimpleGraph directory, reading the module docstring (i.e. the stuff at the top) of each file you click on.

[Yaël Dillies]

We have plenty of results about finite graphs, eg Bhavik and I proved Szemerédi's Regularity Lemma

[Aatman Supkar]

But I can't quite find in the documentation how to explicitly declare that my graph is on a finite vertex set. Can you help me out with this? Maybe the answer is indeed in the documentation, but it is overwhelming somehow.

[Kevin Buzzard]

Here are some examples (from my course) of basic usage of graph theory. As you can see from the example at the bottom of sheet 3, [Fintype V] is how to make the vertex set finite.

[Aatman Supkar]

Yaël Dillies said:

We have plenty of results about finite graphs, eg Bhavik and I proved Szemerédi's Regularity Lemma

Then, could you recommend results to formalise that you know aren't dealt with yet?

[alindeng]

Im a new user lean for graph theory