Zulip Chat Archive

Stream: triage

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

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: Dec 20 2023 at 11:08 UTC