Is the infinitary Ramsey theorem in mathlib?

Stream: new members

[Ching-Tsun Chou]

I mean theorems like this one:

https://en.wikipedia.org/wiki/Ramsey%27s_theorem#Infinite_graphs

[Ching-Tsun Chou]

In fact, I need only the n = 1 case for now. Later I may need the n = 2 case.

[Matt Diamond]

#12773 is infinite Ramsey for hypergraphs

[Matt Diamond]

seems like it stalled last year though

[Matt Diamond]

@Peter Nelson

[Peter Nelson]

I can try dusting it off.

[Peter Nelson]

It was all typechecking at the time.

[Matt Diamond]

the n = 1 case should be easy to prove if we don't already have it

[Matt Diamond]

relevant: docs#Cardinal.infinite_pigeonhole

[Ching-Tsun Chou]

Thanks for the pointers!

[Ching-Tsun Chou]

Will the PR #12773 make its way into mathlib any time soon? I need the n = 2 case (see: https://en.wikipedia.org/wiki/Ramsey%27s_theorem#Infinite_graphs) in my project. Before PR #12773 is merged into mathlib, is there a stopgap solution that I can use? Of course, I can just prove the n = 2 case myself, but I want to explore the possibilities before I spend the time.

[Yaël Dillies]

I will make sure to review this PR when Reuben gets it green again

[Yaël Dillies]

cc @Peter Nelson if ever you happen to have time to revive your own PR (it's ok if not!)

[Yaël Dillies]

@Ching-Tsun Chou, are you interested in taking over #12773? I think it would be a very valuable contribution and you are well positioned to handle it

[Ching-Tsun Chou]

Sure. But I'm not familiar with the mechanics. Is there a cheatsheeet explaining the process? Also, I'll need some time to get familiar with the code.

[Peter Nelson]

No time right now - but I'm happy to seepeople looking at this!

[Ruben Van de Velde]

@Ching-Tsun Chou There's some documentation at https://leanprover-community.github.io/contribute/index.html and more at the bottom of the left navigation bar - I think the most useful thing to do right now would be to create small new PRs for changes in #12773 that stand on their own (like I did in #27211)

[Ching-Tsun Chou]

Recently there was a change in the mathlib contribution process: #mathlib4 > New contribution model: PRs from forks . Has #12773 been migrated to the new process?

[Bryan Gin-ge Chen]

It has not, but we can still merge PRs into the branch of that PR (ramsey_hypergraph) and finally merge that PR when it's ready. Alternatively, if both you and @Peter Nelson are up for it, you can try migrating the PR to your fork of mathlib4 (with the script in scripts/migrate_to_fork.py), and you can work on it in a new PR.

[Ching-Tsun Chou]

Will scripts/migrate_to_fork.py keep the PR # and continue to use the same Github PR entry (https://github.com/leanprover-community/mathlib4/pull/12773)? If not, then I think we should use the old PR branch ramsey_hypergraph.

[Bryan Gin-ge Chen]

It will create a new PR that links to the old one.

[Ching-Tsun Chou]

I don't know. What is the option preferred by the mathlib maintainers?

[Ruben Van de Velde]

Create a new one

[Ching-Tsun Chou]

Just migrated the PR to the fork-based workflow. New PR:
https://github.com/leanprover-community/mathlib4/pull/27217

[Ruben Van de Velde]

Thanks!

[Ching-Tsun Chou]

Now that I've looked at the code more closely, I'm not sure I understand it. It seems to me that the last theorem Ramsey.exists_monochromatic_infinite_subset in HypergraphRamsey.lean is essentially the Ramsey theorem that Bhavik Behta proved in Lean3 in 100 lines of code (https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean). Why is the new proof so much longer (over 300 lines) and also involves so many other files? Is it because several variations of the results are also proved? I also don't quite understand the proof strategy. I'm no expert in the subject matter. But it seems to me that Ramsey.exists_monochromatic_infinite_subset is the conceptually simplest among the proved results, because it involves only the concept of cardinality and nothing about ordering. Shouldn't all other results be derived from it, rather than the other way around?

[Peter Nelson]

The way I did it allows for things in the direction of the canonical Ramsey theorem, which inherently involves orderings. It's quite annoying to get from the unordered to the ordered version, but vice versa is not so bad.

[Ching-Tsun Chou]

I created a new PR for the Data.Finset.Sort part of #27217:
https://github.com/leanprover-community/mathlib4/pull/27233

[Yaël Dillies]

@Ching-Tsun Chou, thanks! I've fixed your PR title and description (the rules are written in the commit convention: https://leanprover-community.github.io/contribute/commit.html)

[Ching-Tsun Chou]

PR #27217 is now dependent on PR #27233.

[Ching-Tsun Chou]

I split out the Order.Extension.Linear and related part of #27217 into a new PR #27271. So #27217 now depends on #27271 and #27233, which in turn depends on #27211 (#27211 is now in the master branch).

[Ching-Tsun Chou]

@Peter Nelson, Please take a look at @Bhavik Mehta 's comment in https://github.com/leanprover-community/mathlib4/pull/27271. Thanks!

[Adam Lehavi]

Hey guys! I'm new to Lean and got introduced to it because I'm interested in formalizing some Ramsey Theory. What's the progress on general infra/statements about two color Ramsey theory bounds on complete graphs in Mathlib right now? I've looked through the thread but it's a lot to parse through. I'm mostly interested in lower and upper bounds as well as counter example checking. Does that or anything close to that exist, or is there anyone interested in this area as well?

[Yaël Dillies]

@Bhavik Mehta has proved both the classical Erdos lower bound using the probabilistic method and the recent 3.999^k for diagonal Ramset numbers

[Yaël Dillies]

His machinery is slowly making its way to mathlib

[Bhavik Mehta]

I also verified the values of R(3,3), R(3,4), R(4,4) and R(3,3,3). You might also be interested in the recent formal work - not in Lean - on R(4,5) here https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.16

[Adam Lehavi]

Great to know and thanks for the quick response! The paper actually was what motivated my look into formalization. I was wondering what the utility would be of proving that or other gluing approaches in LEAN? I recently tried coming up with an alternate construction / gluing approach with a runtime tradeoff, but proof of correctness seemed like something that would be best achieved formally.

[Ching-Tsun Chou]

I proved the Ramsey theorem for infinite graph:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Mathlib/InfGraphRamsey.lean
because I need the result in my automata theory project:
https://github.com/ctchou/AutomataTheory/blob/fe363bc04474d44b447d9abff8be3f74fcfd67c1/AutomataTheory/Congruences/BuchiCongr.lean#L145
I basically followed the argument in Wikipedia for the case n = 2:
https://en.wikipedia.org/wiki/Ramsey%27s_theorem#Infinite_graphs
It seems quite possible to generalize the proof to all n via induction, as outlined in the Wikipedia article. But I don't have a good sense of how hard that is.