Elijah Beregovsky

Stream: new members

[Elijah Beregovsky]

Hi, everyone!
My name is Elijah and I've just finished my Bachelor's (a weird mix of physics, chemistry and biology) and am now embarking on my Master's. I knew about Lean for a while, but only last week I finally got to learning it, and I'm absolutely in love with it already. The NNG was addictive as heck, and as a result lasted me only two days, and now I want more. (I also immediately saw its power as a teaching tool, because it was the first time I got my younger brothers enthusiastic about maths, and not for lack of trying.)
At the moment I'm looking at the graph theory part of mathlib and I can't help but notice how many very basic undergrad results are missing from there. I would love to contribute! However, my knowledge of the language and the library is not enough to do that yet, so I'd appreciate some pointers. For example, I can't quite understand how one would write an induction on vertex number
PS: I also love combinatorial optimisation and integer sequences, so I also want to look into some OEIS-like theorems

[Yaël Dillies]

Welcome! It's always good to have more people interested in graph theory. If you want to contribute, I would suggest you find a self-contained graph theory result with a not-so-long proof. Then we will be able to help you more concretely.

[Daniel Weber]

You might also want to take a look at #graph theory

[Elijah Beregovsky]

Self-contained as in "not requiring to prove a large number of theorems not already in the library"? Right now I'm trying (and failing miserably. oh well, learning is a process) to prove a couple very basic tree-related theorems that are not in Acyclic. Specifically I want to prove the converse of IsTree.card_edgeFinset -- if the number of edges in a connected graph is one less than the number of its vertices then the graph is a tree. I want to do that by induction on the vertex number, but I can't figure out how to formalise it. (I also feel like I'd need a lemma like "a tree has a leaf vertex" for it, which seems like a useful lemma to have anyway)

[Rida Hamadani]

Welcome Elijah, happy to see that you are interested in formalizing graph theory too. Can you post a #mwe of the problem you are facing?

On the other hand, do you want recommendations for such "self-contained" results to work on and contribute?

[Elijah Beregovsky]

Rida Hamadani said:

On the other hand, do you want recommendations for such "self-contained" results to work on and contribute?

Yes! Absolutely!

[Yaël Dillies]

That sounds like a self-contained result indeed! I would suggest you do something like

set n := Fintype.card V with hn
clear_value n
induction' n using Nat.induction with n ih generalizing V

where V is your type of vertices

[Daniel Weber]

Would it be easier to use docs#Fintype.induction_empty_option ?

[Yaël Dillies]

Possibly! I would need to see the code to give more precise suggestions

[Rida Hamadani]

Elijah Beregovsky said:

Yes! Absolutely!

There is a TODO item in the SimpleGraph/Diam.leam file that I believe is ready to be worked on (sorry can't link, on mobile). The definitions are all there, we might want to add 1 more definition to make the proof cleaner, but also maybe not.

I plan to do this once I'm done with what I'm working on at the moment, but feel free to work on it.

[Daniel Weber]

You can do file#Mathlib/Combinatorics/SimpleGraph/Diam to link to it