Skip to content

Problems · Vela Mathematics Program

Narrowed tofalsifiable ×number theory ×Clear all

Problem ledger

8 problemsGraph view
declared falsifiable · formalizederdos:242
∀ (n : ℕ), 2 < n → ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z
number theoryunit fractionsA073101 · A075245 · A075246 · A075247 · A075248 · A2871162 sources
declared falsifiable · formalizederdos:287
True ↔ ∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i, 1 / ↑(s i) = 1 → 3 ≤ Erdos287.max_gap k s
number theoryunit fractionsN/A2 sources
declared falsifiable · formalizederdos:375
True ↔ Erdos375.Erdos375Prop
number theoryN/A2 sources
declared falsifiable · formalizederdos:398
sorry ↔ {n | ∃ m, n.factorial + 1 = m ^ 2} = {4, 5, 7}
number theoryfactorialsA146968 · A1413992 sources
declared falsifiable · formalizederdos:458
True ↔ ∀ (k : ℕ), Erdos458.lcm_upto (Nat.nth Prime (k + 1) - 1) < Nat.nth Prime k * Erdos458.lcm_upto (Nat.nth Prime k)
number theoryprimesA0566042 sources
declared falsifiable · formalizederdos:488
True ↔ ∀ (A : Finset ℕ), A.Nonempty → 0 ∉ A → 1 ∉ A → ∀ (n m : ℕ), m > n → A.max ≤ ↑n → ↑{x ∈ Finset.Icc 1 m | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑m < 2 * ↑{x ∈ Finset.Icc 1 n | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑n
number theoryN/A3 sources
declared falsifiable · formalizederdos:699
True ↔ ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → ∃ p, Nat.Prime p ∧ i ≤ p ∧ p ∣ (n.choose i).gcd (n.choose j)
number theorybinomial coefficientsN/A2 sources
declared falsifiable · formalizederdos:779
∀ n ≥ 1, have P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i; ∃ p, Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P
number theoryprimesA0052352 sources

Search problems.science

Find a Problem, Result, source, or page