-
Notifications
You must be signed in to change notification settings - Fork 57
Create the problem statement for IMO 2025 #4 #111
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Conversation
|
Sorry, I don't know why Github links |
| def A₀ := { a₀ | ∃ a, a 0 = a₀ ∧ IsAllowed a } | ||
|
|
||
| variable {x : ℕ+} | ||
|
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Any of these items that are necessary for stating the problem should be hidden inside snip begin ... snip end, as descirbed here: https://github.com/dwrensha/compfiles?tab=readme-ov-file#extracting-problems
…add a link to the youtube proof
| The infinite sequence a₁, a₂, ... consists of positive integers, each of which has at least three proper | ||
| divisors. For each n ≥ 1, the integer aₙ + 1 is the sum of the three largest proper divisors of aₙ. | ||
| Determine all possible values of a₁. | ||
| Proof follows https://www.youtube.com/watch?v=Kb4h_GVFT1k |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please put any comments about the proof either inside the snip begin ... snip end, or within in the tactic body of the problem proof, so that they don't show up as spoilers on the extracted problem webpage.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done. I'll contribute more to the solution over the next few months
Using https://www.youtube.com/watch?v=Kb4h_GVFT1k