Skip to content

Erdős Problem 422 #692

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.

Sign up for GitHub

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

Open
wants to merge 11 commits into
base: main
Choose a base branch
from
Open

Erdős Problem 422 #692

Changes from 9 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
8591cd1
Erdős Problem 422
rao107 Sep 28, 2025
8951771
Change def of f to start at 1
rao107 Sep 28, 2025
aa5caa7
Update comment
rao107 Sep 28, 2025
4ed7626
Merge https://github.com/rao107/formal-conjectures into erdos_422
rao107 Sep 28, 2025
e43a805
Update FormalConjectures/ErdosProblems/422.lean
rao107 Sep 29, 2025
00c0c01
add in answer(sorry)
rao107 Sep 29, 2025
534e360
Add more related statements
rao107 Oct 2, 2025
bc1438d
Merge branch 'main' of https://github.com/rao107/formal-conjectures i…
rao107 Oct 19, 2025
a59c08f
Add eventually const variant to Erdős Problem 422
rao107 Oct 19, 2025
6166ffc
Add Calle Sonne's suggestions
rao107 Oct 28, 2025
107f7fe
Merge https://github.com/rao107/formal-conjectures into erdos_422
rao107 Oct 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 73 additions & 0 deletions FormalConjectures/ErdosProblems/422.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjectures.Util.ProblemImports

/-!
# Erdős Problem 422

*Reference:* [erdosproblems.com/422](https://www.erdosproblems.com/422)
-/

namespace Erdos422

open Filter
open scoped Topology

instance : Norm ℕ+ where
norm n := n
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
instance : Norm ℕ+ where
norm n := n

I'm not sure if you want to add this as a global instance. For example there seems to be no Norm instance on ℕ in mathlib (that I can find). I believe the reason for this is that you don't want it as an instance as a priori there are multiple possible norms (such as the p-adic norms as well). I'm assuming you are adding this in order to talk about the growth rate below, but what you can do is just to view f as a function valued in R for that statement. See my suggestion below.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I didn't realize I could do that! Thank you so much!


/--
Let $f(1) = f(2) = 1$ and for $n > 2$
$$
f(n) = f(n - f(n - 1)) + f(n - f(n - 2)).
$$
-/
partial def f : ℕ+ → ℕ+
| 1 => 1
| 2 => 1
| n => f (n - f (n - 1)) + f (n - f (n - 2))
-- Note: It is not known whether $f(n)$ is well-defined for all $n$.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here I think it would be interesting to add two statements:

  1. The question of the surjectivity of f (seems to be open)
  2. The question of whether the sequence f must eventually terminate (presumably not? admittedly I haven't thought too much about whether or not this is hard to prove)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Those sound like good ideas. I'll also add in a question of the function's growth rate since that's open as well.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hey, I added your suggestions but I had a bit of trouble with the second.

For it, I removed the partial definition for f and defined the function with sorry. I don't think this is what you had in mind when you suggested it so I'd welcome any other ways to define that f must eventually terminate.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps by termination @Paul-Lez meant whether f becomes stationary at some point? I.e., does there exist m and N for which f n = m for all n larger than N. Termination can be quite surprising in this sense, see for example the Goodstein sequence which eventually decreases and terminates at 0.

The other interpretation of termination here is whether one reaches a point at which f n cannot be defined (e.g, if n - f (n - 1) < 0), but I think this sense is already captured in the definition.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apologies for the delay! I've added another variant for f eventually becoming stationary. 🙂

/--
Does $f(n)$ miss infinitely many integers?
-/
@[category research open, AMS 11]
theorem erdos_422 : Set.Infinite {n | ∀ x, f x ≠ n} ↔ answer(sorry) := by
sorry

/--
Is $f$ surjective?
-/
@[category research open, AMS 11]
theorem erdos_422.variants.surjective : f.Surjective ↔ answer(sorry) := by
sorry

/--
How does $f$ grow?
-/
@[category research open, AMS 11]
theorem erdos_422.variants.growth_rate : f =O[atTop] (answer(sorry) : ℕ+ → ℕ+) := by
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
theorem erdos_422.variants.growth_rate : f =O[atTop] (answer(sorry) : ℕ+ → ℕ+) := by
theorem erdos_422.variants.growth_rate :
(fun n ↦ (f n : ℝ)) =O[atTop] (answer(sorry) : ℕ+ → ℝ) := by

sorry

/--
Does $f$ become stationary at some point?
-/
@[category research open, AMS 11]
theorem erdos_422.variants.eventually_const : (∃ n, EventuallyConst f n) ↔ answer(sorry) := by
sorry

end Erdos422