Latin Tableau Conjecture #1385
Latin Tableau Conjecture #1385
Conversation
Paul-Lez
left a comment
Paul-Lez
left a comment
There was a problem hiding this comment.
Thanks for the PR! A few initial comments:)
| noncomputable def independenceNumK (G : SimpleGraph α) (k : ℕ) : ℕ := | ||
| sSup { n | ∃ f : Fin k → Set α, (∀ i, G.IsIndepSet (f i)) ∧ ((⋃ i, f i).ncard = n) } | ||
|
|
||
| /- A finite graph is cdsColorable if it has a proper coloring |
There was a problem hiding this comment.
| /- A finite graph is cdsColorable if it has a proper coloring | |
| /-- A finite graph is cdsColorable if it has a proper coloring |
|
|
||
| namespace SimpleGraph | ||
|
|
||
| /- The maximum size of the union of k finite independent sets. -/ |
There was a problem hiding this comment.
| /- The maximum size of the union of k finite independent sets. -/ | |
| /-- The maximum size of the union of k finite independent sets. -/ |
| ∃ (C : G.Coloring Nat), ∀ k : Nat, k > 0 → | ||
| ∑ i ∈ Finset.range k, (C.colorClass i).ncard = independenceNumK G k | ||
|
|
||
| open YoungDiagram |
There was a problem hiding this comment.
Typically we'd put conjectures (in fact, the whole file containing a conjecture) in a namespace. Here I'd suggest LatinTableau as the namespace.
|
|
||
| variable {α : Type*} [DecidableEq α] | ||
|
|
||
| namespace SimpleGraph |
There was a problem hiding this comment.
If these definitions are standard, it may be worth adding them to the ForMathlib subdirectory.
| limitations under the License. | ||
| -/ | ||
|
|
||
| import Mathlib |
There was a problem hiding this comment.
| import Mathlib | |
| import FormalConjectures.Util.ProblemImports |
|
All of Paul-Lez's comments look good to me. At first, I tried to imitate other submissions to Formal Conjectures, but I was getting errors, probably because the import FormalConjectures command wasn't working for me. Do I need to make the above changes myself and resubmit, or can someone else make them on my behalf? The only nontrivial question, I think, is which (if any) of these definitions are "standard" enough to consider adding to mathlib. I'd say that independenceNumK is the only one I'd consider "standard," and if it's added, then an analogous cliqueNumK should probably be added as well. And maybe a bunch of helper functions should be added too? Since I'm still a beginner, I wasn't planning to go down this rabbit hole, so maybe I should just skip this for now? |
YaelDillies
added
the
awaiting-author
|
I see that the "awaiting-author" label has been added. What does this mean? I guess I'm supposed to do something? |
@tchow12000-coder Sorry for the slow reply! We tend to follow the usual Github workflow, i.e. making changes directly to the pull request (so this would mean you should make the changes yourself and then push to this PR). Concerning the definitions, I think it's reasonable to add the standard definitions to the The awaiting-author label just means that the PR has been reviewed and some changes have been recommended. This is useful to keep track of the status, but we tend to take a look these relatively often too to make sure we haven't missed any new stuff being added. |
|
Okay, I think I pushed the changes (though I'm not very fluent with Git so I may have missed a step). I'm still a bit hesitant to submit independenceNumK to mathlib. My first attempt used Finset rather than Set, and I decided on Set because the formalization is shorter, but it's possible that that wasn't the "right" decision. My conjecture concerns finite graphs only, so either choice is formally correct for the purposes of my conjecture, but in a more general setting I'm not sure which choice is better. I feel like I need to gain more experience with Lean before I start submitting things to mathlib. Also, what I'm calling independenceNumK is equivalent to the maximum size of a k-colorable subgraph, so maybe it's better to frame it that way in mathlib. |
3 participants
The Latin Tableau Conjecture states that the graph associated to any (finite) Young diagram (i.e., whose vertices are the cells of the diagram, with edges between cells in the same row or column) is CDS-colorable, meaning that there exists a proper coloring of the vertices of the graph such that for all k > 0, the number of vertices with color < k equals the maximum size of the union of k independent sets of the graph.