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.

Formal statement

Disproof target

import FormalConjectures.ErdosProblems.«859»
import TaskSupport

namespace Bounty

theorem target : ¬ (fcTypeOfName% "Erdos859.erdos_859") := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∃ c₁ > 0,
  ∃ c₂ > 0,
    ∃ d,
      (∀ t > 0, (Erdos859.DivisorSumSet t).HasDensity (d t)) ∧
        Asymptotics.IsEquivalent Filter.atTop (fun t => d t) fun t => c₁ / Real.log ↑t ^ c₂

Original conjecture source: FormalConjectures/ErdosProblems/859.lean

Source type SHA-256: sha256:ae157d2fa9710fa23cfda48f0ca94e3aaeb9d2b29385bed2a2e1d533af009db9
Task id: fc-6a786f99-erdos859-erdos-859-9a02c99a6c-counterexample-v1
Task commitment: sha256:107473b4c482f581571820568e3dd9beb7f0588b498149f1f65df183fb034857

References

Erdős problem 859 · Conjectures.io

Every problem here was open when it entered the pool.

Erdős problem 859

What has been built

Where this lives