Erdős problem 307
Are there two finite set of primes and such that
Sources
FormalConjectures/ErdosProblems/
307.lean
Retained formal statement
A machine-checked barrier for Erdős 307 (Bonfioli, 2026): any solution with Q nonempty uses at least 59 primes in total, and (∏_{p ∈ P} p)² ≥ 4·10¹¹² — i.e. ∏_{p ∈ P} p ≥ 2·10⁵⁶ (and, by symmetry, the same for ∏ Q); so no solution lies below a prime-product of 2.09·10⁵⁶. The full sorry-free proof is in the linked repository (Closed.lean at tag v1.0.0): the left conjunct is card_ge_59, the right is erdos307_barrier_closed. The only non-logical input is a native_decide evaluation of the first 59 primes; the axioms are propext, Classical.choice, Quot.sound together with that native_decide.
∀ {P Q : Finset ℕ}, (∀ p ∈ P, Nat.Prime p) → (∀ q ∈ Q, Nat.Prime q) → Q.Nonempty → 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹ → 59 ≤ (P ∪ Q).card ∧ 4 * 10 ^ 112 ≤ (∏ p ∈ P, ↑p) ^ 2