Zulip Chat Archive

Stream: triage

Topic: PR #4369: feat(archive/imo): formalize IMO 1964 problem 1


view this post on Zulip Random Issue Bot (Nov 05 2020 at 14:16):

Today I chose PR 4369 for discussion!

feat(archive/imo): formalize IMO 1964 problem 1
Created by @None (@mushokunosora) on 2020-10-02
Labels: WIP, awaiting-author, imo

Is this PR still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 23:23):

This doesn't look too hard to knock off...

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 16:54):

#4935 . It seemed easier (for me) to start again.

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 16:56):

@Kenji Nakagawa if you want to fill in the sorries of your proof then I'm happy to close my PR and go with yours instead; this triage stream is an attempt to clear up some old PR's.

view this post on Zulip Kenji Nakagawa (Nov 07 2020 at 20:34):

@Kevin Buzzard Feel free to merge yours and I'll close my PR, I ran into quite a few difficulties using zmod (or just setting it up right), so I think your method is better. Thanks for helping formalize this problem!

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 21:14):

Thanks for inspiring me :D


Last updated: May 18 2021 at 23:14 UTC