Number theory

Erdős problem 25

Let

n_1 < n_2 < \dots

be an arbitrary sequence of integers, each with an associated residue class

a_i \pmod{n_i}

. Let

A

be the set of integers

n

such that for every

i

either

n < n_i

n \not\equiv a_i \pmod{n_i}

. Must the logarithmic density of

A

exist?

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«25»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos25.erdos_25" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ),
    (∀ (i : ℕ), 0 < seq_n i) →
      StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d

Original conjecture source: FormalConjectures/ErdosProblems/25.lean

Source type SHA-256: sha256:0296f636686c1a8f82bdf2d005e25e6259d09e61f6181662bdea0e64f94d3e24
Task id: fc-v2-erdos25-erdos-25-8f1f295f7d42d4099e1ee516-formalized
Task commitment: sha256:49e2ee1eb3500e6037d3a5759fd356ee1f3766813ff55f6cf79cd71a50374bf7

References

erdosproblems.com/25

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord