Skip to content

Conversation

@a2435191
Copy link

@a2435191
Copy link
Author

Sorry, I don't know why Github links #4 in the title to an old merge. I'll write P4 in the future

@dwrensha
Copy link
Owner

Are you aware of IMOLean? It has formalizations of problem statements for recent years. Here is its formalization of this problem.

@a2435191
Copy link
Author

Are you aware of IMOLean? It has formalizations of problem statements for recent years. Here is its formalization of this problem.

Thank you! I know the OrderEmbedding in the problem statement was clunky. I am now using Finset.sort. Does this seem like an okay idea to you?

def A₀ := { a₀ | ∃ a, a 0 = a₀ ∧ IsAllowed a }

variable {x : ℕ+}

Copy link
Owner

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

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
Copy link
Owner

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.

Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants