PRs for Turán's theorem

Stream: PR reviews

[Jeremy Tan]

I'm still waiting for a maintainer merge on #8735 regarding parts of finpartitions. Why does noone want to review this after four months or so?

This is a prerequisite for my proof of Turán's theorem in #9317.

[Jeremy Tan]

List of related PRs (all are independent):

• #8735
• #9348 (used to count the number of edges in the Turán graph)
• #9645 (first part of Turan.lean)

[Yaël Dillies]

because I want to sit down and review things properly, but I'm currently doing Part III

[David Loeffler]

@Yaël Dillies Is there nobody else you would trust to review these in your place? Perhaps you can volunteer someone. After all, you can hardly expect Jeremy to wait until June when your Part III exams finish.

[Yaël Dillies]

There are only two combinatorics maintainers: @Kyle Miller and @Bhavik Mehta. One is busy with the FRO, the other with writing a PhD thesis. I am the sole reviewer specialised in combinatorics.

[Yaël Dillies]

Anybody can review, of course! But official support for combinatorics is lacking... cf my very own PRs like #8304 or #8896 which also languish for six months at a time.

[David Loeffler]

Sounds like we need to press-gang some more people then!

[Ruben Van de Velde]

Congratulations on becoming our resident combinatorics expert, @David Loeffler !

[David Loeffler]

Clearly I should have said "more competent people"

[Antoine Chambert-Loir]

Yaël Dillies said:

Anybody can review, of course! But official support for combinatorics is lacking... cf my very own PRs like #8304 or #8896 which also languish for six months at a time.

I added a few remarks to #8304.

[Jeremy Tan]

#11989 and #11990 are now independent and mature enough parts of #9317 to be included in mathlib

[Yaël Dillies]

Sorry I won't have time to review before a month

[Jeremy Tan]

Yaël Dillies said:

Sorry I won't have time to review before a month

When does Part III end anyway?

[Yaël Dillies]

June

[Jeremy Tan]

Oh, and #12196 too

[Jeremy Tan]

#12196 has been updated with the full part-preserving equivalence

[Jeremy Tan]

#11990 is now really ready for review. I've polished it and it now contains the entire forward direction of Turán's theorem

[Jeremy Tan]

I'd also like a review of #11989

[Jeremy Tan]

@Yaël Dillies https://github.com/leanprover-community/mathlib4/pull/11989#issuecomment-2164348613

[Jeremy Tan]

Also, reminder to review #11990 – I don't think there's anything contentious about it, it can be merged as it is now

[Yaël Dillies]

Sorry, short on time today

[Jeremy Tan]

#11990 has now been put on the maintainer merge queue. Any maintainer free to merge this?

[Jeremy Tan]

With my massiive simplification of the reverse direction of the proof, the plan is that after #11990 is merged #9317 can be merged directly, and the other PRs that were once prerequisites are now merely additions to #9317

[Jeremy Tan]

#9317 is (finally) ready for review

[Yaël Dillies]

My review days are (mostly) over for June, but if you ping me on the 6th of July I can have a look

[Johan Commelin]

I left a review. 1 comment, otherwise LGTM

[Jeremy Tan]

I have addressed the comment (to the best of my ability)

[Johan Commelin]