mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Archive/Imo): formalize IMO 1982q1

Open AlexBrodbelt opened this issue 1 year ago • 4 comments

Formalized question 1 of the 1982 IMO.

Made a mistake with my original PR as I made a branch from Imo1982Q3, this should be fixed now.

Fixed the domain of the function to be the positive naturals according to @vihdzp comments - took less effort than expected.

Please let me know if I have made a mistake or if there are any further comments or improvements.

Open in Gitpod

AlexBrodbelt avatar Sep 17 '24 09:09 AlexBrodbelt