Stream: maths

Topic: countable De Bruijn–Erdős theorem

Kyle Miller (Jun 09 2020 at 22:22):

Greetings from the Berkeley Lean Seminar, where a bunch of us are learning Lean this summer. As my first "real" project, I decided to formalize the Nash-Williams argument for the following version of the De Bruijn–Erdős theorem, that if a graph with countably many vertices has the property that every finite subgraph can be n-colored, then the graph can be n-colored. This involved proving a specialization of Kőnig's lemma, that the inverse limit of an ℕ-indexed family of nonempty finite sets is nonempty.

So, fresh off the presses, here it is:

Coloring statement: https://github.com/kmill/lean-graphcoloring/blob/master/src/graph.lean#L347

The proofs are terrible, but, hey, it's proved. (While any hints to clean things up would be appreciated, I don't want to harm any of your eyes with its very hacky state. I feel like much of it was constructed through pure force of will.)

Many decisions were made for pedagogical reasons, to learn different parts of Lean. Probably a more straightforward proof would be for the full De Bruijn–Erdős theorem, using ultrafilters to construct a coloring from a choice of coloring for each finite subgraph. (That is, a compactness argument.)

Johan Commelin (Jun 10 2020 at 06:34):

@Kyle Miller Nice! We also wrote a bunch of graph colouring stuff on the hedetniemi branch. But it hasn't made it into mathlib master yet.

Johan Commelin (Jun 10 2020 at 06:34):

Are you planning to PR this to mathlib?

Kenny Lau (Jun 10 2020 at 06:37):

feature request: GUI for hedetniemi branch

Johan Commelin (Jun 10 2020 at 06:37):

Assigned to: @Kenny Lau :rofl: :oops: :stuck_out_tongue_wink:

David Wärn (Jun 10 2020 at 09:52):

Very nice! I agree that the full theorem might be easier to prove -- either using ultrafilters, or Tychonoff, or Zorn (consider the poset of partial colourings that can be extended to cover any finite subgraph).

Kevin Buzzard (Jun 10 2020 at 10:02):

I want to say that this follows from the compactness theorem from logic but I'm no expert in this area

Patrick Massot (Jun 10 2020 at 10:03):

Who hacked Kevin's Zulip account again?

Patrick Massot (Jun 10 2020 at 10:04):

We already had people posting type theory messages using his account and now logic?!

David Wärn (Jun 10 2020 at 10:11):

Yes, compactness theorem for propositional logic is basically same thing as Tychonoff for products of finite spaces

Dave (Jun 10 2020 at 11:51):

^This is not totally true. Tychonoff implies it, yes, but you only need Boolean prime ideal theorem (they are equivalent), which is weaker than choice and so weaker than Tychonoff.

David Wärn (Jun 10 2020 at 13:14):

Right, I'm saying it's equivalent to "product of finite spaces is compact", which is all you need for De Bruijn–Erdos

Patrick Lutz (Jun 10 2020 at 16:59):

@Kevin Buzzard Yes, there is a pretty straightforward proof using the compactness theorem for first order logic. That proof also works for uncountable graphs, unlike the Konig's lemma proof (but like the Tychonoff proof).

Kyle Miller (Jun 11 2020 at 22:46):

Johan Commelin said:

Are you planning to PR this to mathlib?

I'm willing to create PRs, but I'm not exactly sure what the criteria for inclusion is. I've at least now factored out and cleaned up some possibly useful results in mylist, myoption, and myfintype (https://github.com/kmill/lean-graphcoloring/tree/master/src). The proof of this specialization of Konig's lemma has also been cleaned up a bit.

Johan Commelin (Jun 12 2020 at 04:46):

@Kyle Miller The criteria for inclusion are: it should follow the style guidelines, and it should not be "crackpot". If you cook up a definition of boolalas and prove 10.000 lines of code about them, without any connection to the outside world... then we probably aren't very interested. (Clearly, this doesn't apply to whay you've done.)

Mario Carneiro (Jun 12 2020 at 04:50):

I don't know, boolala sounds pretty interesting if there is that much to say about it

Scott Morrison (Jun 12 2020 at 04:50):

If it's "recognisably maths", it passes the interest criterion. :-)

Mario Carneiro (Jun 12 2020 at 04:51):

I've been wondering about whether to submit my formalization of the type theory of C to mathlib. It's definitely starting to rot but it's also very far removed from everything else currently in mathlib

Johan Commelin (Jun 12 2020 at 04:52):

Why don't you start a computer_science/ top-level directory?

Johan Commelin (Jun 12 2020 at 04:53):

You could always put it in archive/

Last updated: May 11 2021 at 15:12 UTC