Erdős problem 538
If each integer has at most representations with prime and , what is the best upper bound for ? The candidate proof gives the matching order .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/538.leanTrue ↔ ∀ (r : ℕ), 2 ≤ r → ∃ c, 0 < c ∧ Filter.Tendsto (fun N => Erdos538.maxMass r N * Real.log (Real.log ↑N) / Real.log ↑N) Filter.atTop (nhds c)OpenStatement only, no proof
Proof manifests naming this Problem
- William Blair Lean proofs
williamjblair:Erdos538.erdos538_matching_order
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Subtle errors
argument
- Machine
- Reported outcome