Back to Problems

erdos_288.variants.i2_card_eq_1

Specification

This is still open even if $|I_2| = 1$.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem erdos_288.variants.i2_card_eq_1 : answer(sorry) ↔ Set.Finite { (I, n₂) : (ℕ+ × ℕ+) × ℕ+ |
    I.1 ≤ I.2 ∧ ∃ n : ℕ+, ∑ n₁ ∈ Set.Icc I.1 I.2, (n₁⁻¹ : ℚ) + (n₂⁻¹ : ℚ) = n }
ID: ErdosProblems__288__erdos_288.variants.i2_card_eq_1
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.