Number theory

Erdős problem 1106 - part ii

Let

p(n)

be the partition number of

n

and

F(n)

be the number of distinct prime factors of

∏_{i= 1} ^ {n} p(n)

F(n)>n

for sufficiently large

n

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.«1106»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1106.erdos_1106.parts.ii" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, (∏ i ∈ Finset.Icc 1 n, Erdos1106.p i).primeFactors.card > n

Original conjecture source: FormalConjectures/ErdosProblems/1106.lean

Source type SHA-256: sha256:3a79424001452961961cc10b1ab7e9653b853758d2edcf306248b0b9a775c8f8
Task id: fc-v2-parts-ii-dd3b65e8537f915527d14aa3-formalized
Task commitment: sha256:161d6a7dcb9819311b850ea16bdaff869f900443e77f4d5fffa744bc64023899

References

erdosproblems.com/1064

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