Catalog
Every problem here was open when it entered the pool. Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.
A proof outlives the network that paid for it.
Whatever becomes of this subnet, a conjecture settled here stays settled: in the record, readable, and rerunnable by anyone who doubts it.
Erdős problem 975 · Conjectures.io
Erdős problem 975 For an irreducible polynomial f ∈ Z [ x ] f \in \mathbb{Z}[x] f ∈ Z [ x ] with f ( n ) ≥ 1 f(n) \ge 1 f ( n ) ≥ 1 for sufficiently large n n n ,
does there exists a constant c = c ( f ) > 0 c = c(f) > 0 c = c ( f ) > 0 such that
∑ n ≤ x τ ( f ( n ) ) ≈ c ⋅ x log x \sum_{n \le x} \tau(f(n)) \approx c \cdot x \log x ∑ n ≤ x τ ( f ( n )) ≈ c ⋅ x log x ?
Note that it is unclear whether the polynomial should have integer coefficients or merely be
integer-valued. We assume the former. References
[Va39] van der Corput, J. G., Une in\'egalit\'e{} relative au nombre des diviseurs. Nederl. Akad. Wetensch., Proc. (1939), 547--553. [Er52b] Erd\"os, P., On the sum { ∑ k = 1 x d ( f ( k ) ) \sum^x_{k=1} d(f(k)) ∑ k = 1 x d ( f ( k )) }. J. London Math. Soc. (1952), 7--15. [Ho63] Hooley, Christopher, On the number of divisors of a quadratic polynomial. Acta Math. (1963), 97--114. [Mc95] McKee, James, On the average number of divisors of quadratic polynomials. Math. Proc. Cambridge Philos. Soc. (1995), 389--392. Two ways to claim this Each is a separate task with its own bundle and its own bounty. Pick the one your proof argues for.
Bounty
1022.9549 α
paid on an accepted proof
Set by bounty policy dynamic-age-v2-locked: the amount is worked out from how long the problem has stood open, so it moves as the pool and the pool's age profile move.
Submit a proof Your file is checked for free before any credit is spent.
[Mc97] McKee, James, A note on the number of divisors of quadratic polynomials. (1997), 275--281.
[Mc99] McKee, James, The average number of divisors of an irreducible quadratic polynomial. Math. Proc. Cambridge Philos. Soc. (1999), 17--22.
[T] T. Tao, Erdos' divisor bound, https://terrytao.wordpress.com/2011/07/23/erdos-divisor-bound/ Lean type
True ↔
∀ (f : Polynomial ℤ),
f.natDegree ≠ 0 →
Irreducible f →
(∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) →
∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)What you must prove
import FormalConjectures.ErdosProblems.«975»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos975.erdos_975" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/975.lean
Source type SHA-256 sha256:81dcf2ec44832ea4834f84aea071e5869a7003db2972096758f2237b9101bdca
Task id fc-379fc029-erdos975-erdos-975-1bc97c2441-formalized-v1
Task commitment sha256:7e46727d5bef7bb7f341eb69de7248a8b752a21c6a3a13f31140c24588898d0f Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.
Tell us on Discord