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-126-variants-islittleo

Command line, then a pull request on GitHub.

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«126»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos126.erdos_126.variants.isLittleO" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ (f : ℕ → ℕ), Erdos126.IsMaximalAddFactorsCard f → (fun n => ↑(f n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

Original conjecture source: FormalConjectures/ErdosProblems/126.lean

Source type SHA-256: sha256:e51da61bab02dff3343888e4508dfbd1cb0dcede06e43085d132d5f8a50b05e1
Task id: fc-8432eac9-variants-islittleo-10e93a8905-formalized-v1
Task commitment: sha256:d42f8be261a21dd49442a629eeb17b3163832856bc6f56110697670b34283706

References

Erdős problem 126 - is Little O · Conjectures.io

Every problem here was open when it entered the pool.

Erdős problem 126 - is Little O

Solve it

Add the first piece

What has been built

Where this lives