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 726 As n → ∞ n\to \infty n → ∞ ranges over integers
∑ p ≤ n 1 n ∈ ( p / 2 , p ) ( m o d p ) 1 p ∼ log log n 2 \sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2} ∑ p ≤ n 1 n ∈ ( p /2 , p ) ( mod p ) p 1 ∼ 2 l o g l o g n ?
A conjecture of Erdős, Graham, Ruzsa, and Straus [EGRS75].
By
n ∈ ( p / 2 , p ) ( m o d p ) n\in (p/2,p)\pmod{p} n ∈ ( p /2 , p ) ( mod p ) we mean
n ≡ r ( m o d p ) n\equiv r\pmod{p} n ≡ r ( mod p ) for some integer
with
.
References
[EGRS75] Erdős, P., and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of ( \sp 2 n \sb n ) (\sp{2n}\sb{n}) ( \sp 2 n \sb n ) . Math. Comp. (1975), 83-92. 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
$591
paid on an accepted proof
Set by bounty policy dynamic-age-v1: 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.
3ddd79b5dceb · 5 hours ago
Lean type
True ↔
Asymptotics.IsEquivalent Filter.atTop
(fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n =>
Real.log (Real.log ↑n) / 2What you must prove
import FormalConjectures.ErdosProblems.«726»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos726.erdos_726" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/726.lean
Source type SHA-256 sha256:ce45905671b87d2b8e912323952f79c5f01c9b6842424f53069d9d7cb801dac4
Task id fc-379fc029-erdos726-erdos-726-55bb740cb2-formalized-v1
Task commitment sha256:e034e446c5debd786eab69c7a3c560528a31b471bf0388e2c299d5f148342e41 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
Erdős problem 726 · Conjectures.io