google-deepmind / google-deepmind/formal-conjectures
Erdős Problem 711
Open
ams-11: Number theory
erdos-problems
new conjecture
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 328
Description
### What is the conjecture
https://www.erdosproblems.com/711
Let $f(n,m)$ be minimal such that in $(m,m+f(n,m))$ there exist distinct integers $a_1,\ldots,a_n$ such that $k\mid a_k$ for all $1\leq k\leq n$. Prove that
$$\max_m f(n,m) \leq n^{1+o(1)}$$
and that
$$\max_m (f(n,m)-f(n,n))\to \infty.$$
Status: open
Contributor guide
Assessment
This issue has not been assessed yet.