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.

Solve it

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

Submit a proof

Add the first piece

Even one lemma helps. Whoever finishes this later shares the pool with everyone who got them there.

contrib new erdos-243

Command line, then a pull request on GitHub.

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«243»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos243.erdos_243" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ (a : ℕ → ℕ),
  StrictMono a →
    Filter.Tendsto (fun n => ↑(a n) / ↑(a (n - 1)) ^ 2) Filter.atTop (nhds 1) →
      (Summable fun x => 1 / ↑(a x)) → ∀ᶠ (n : ℕ) in Filter.atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

Original conjecture source: FormalConjectures/ErdosProblems/243.lean

Source type SHA-256: sha256:c02a0aba123879a2d3528458728b4b61afc85f63bc046b43fd0a71a4c419a6e1
Task id: fc-8432eac9-erdos243-erdos-243-41edec662c-formalized-v1
Task commitment: sha256:0065b83f78c44954907882c24ca4ac2d35ba22672b49e0e3e08d2516571207c7

References

Erdős problem 243 · Conjectures.io

Every problem here was open when it entered the pool.

Erdős problem 243

Solve it

Add the first piece

What has been built

Where this lives