Zulip Chat Archive

Stream: general

Topic: PR 15000

Yaël Dillies (Jun 25 2022 at 14:14):

What should #15000 be? People suggested I take it for the isoperimetric inequality, but my current progress makes me think it will rather be #16000. Maybe Dedeking-Kummer?

Thomas Browning (Jun 25 2022 at 16:21):

If there aren't any other candidates, then there's always the option of claiming #15000, and adding the code later (I think something like that happened with #10000).

Yaël Dillies (Jun 25 2022 at 16:22):

Yes, that's what I meant by "taking it" above.

Yaël Dillies (Jun 27 2022 at 09:53):

If no one else puts a proposition forward, I will snipe it for the isoperimetric inequality.

Eric Rodriguez (Jun 27 2022 at 09:54):

I quite liked the idea of Dedekind-Kummer, and I thought that was closer to a finished proof

Yaël Dillies (Jun 27 2022 at 09:55):

Sure, then go for it!

Paul Lezeau (Jun 27 2022 at 12:26):

Sure then I'll claim it if for Dedekind-Kummer it's still available

Anne Baanen (Jun 27 2022 at 12:56):

Paul asked me if I can open this PR, I have the title and description ready for creation.

Anne Baanen (Jun 27 2022 at 14:36):

#15000 created! :tada:

Last updated: Dec 20 2023 at 11:08 UTC