Zulip Chat Archive

@Michael Stoll, are you still interested in having your mathlib3 PR !3#18789 merged. It is marked as not-too-late, but also marked WIP. We'd like to clear out this backlog so it would be good to know your intentions here.

Michael Stoll (Jul 25 2023 at 13:11):

I think it would make sense to integrate this with the more general Matroid Theory development, but I can't really tell how much work that would be (but this would probably mean not to merge the mathlib3 PR). @Peter Nelson what do you think?

What the current PR is missing is a refactor of Hall's Theorem using the more general result, but that would not be a lot of work.
However, I'm at a workshop this week that I am organizing, and so I won't have time to work on this now.

Peter Nelson (Jul 25 2023 at 13:24):

I agree, and I think it'd be doable, though I haven't looked at the proof in detail. One would have to define a constructor for Matroid as per rank_fn in your code, and then to prove it gives a Matroid that is Finitary, whose independent sets are precisely the finite sets with rank equal to cardinality. Then it would be a matter of using the existing Matroid API to make the proof go through, which possibly involves adding a few lemmas for Finitary.

The relevant (lean4) code is here : https://github.com/apnelson1/Matroid. I'm planning to PR the first Data.Matroid contribution imminently (review is almost complete for the last prereq), but the rank stuff is a few PRs away. So if there's no hurry, it will fit in smoothly in (I imagine) a month or two.

Michael Stoll (Jul 25 2023 at 13:38):

OK, good. That time frame would fit quite well for me (I'll be back from vacation).

Scott Morrison (Jul 26 2023 at 23:08):

@Michael Stoll, would it be okay with you, in that case, if we closed !3#18789 for now, and plan to integrate this work later? It's also okay to leave it open: we do want to clear out the mathlib3 queue so we can stick a fork in it and say we're done, but not at the expense of losing appealing contributions.

Michael Stoll (Jul 27 2023 at 07:18):

@Scott Morrison It is OK with me to close it (unless that would mean that the code gets deleted eventually; I would like to keep it on record at least until a version of it makes it into mathlib(4)).

Scott Morrison (Jul 27 2023 at 07:32):

No, there are no plans that anything will even be deleted from the mathlib3 repository!

Scott Morrison (Jul 27 2023 at 07:33):

I've closed.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib