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?
Kevin Buzzard (Nov 05 2020 at 23:23):
This doesn't look too hard to knock off...
Kevin Buzzard (Nov 07 2020 at 16:54):
#4935 . It seemed easier (for me) to start again.
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.
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!
Kevin Buzzard (Nov 07 2020 at 21:14):
Thanks for inspiring me :D
Last updated: May 18 2021 at 23:14 UTC