Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×factorials ×Clear all

Problem ledger

6 problemsGraph view
declared proved (Lean) · formalizederdos:392
∀ (A : ℕ → ℕ), (∀ n > 0, IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n ^ 2), t + 1 = x} (A n)) → (fun n => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n
number theoryfactorialspossible5 sources
declared proved (Lean) · formalizederdos:401
True ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (r : ℕ), 1 ≤ r → {n | ∃ a₁ a₂, 0 < a₁ ∧ 0 < a₂ ∧ ↑a₁ + ↑a₂ > ↑n + f r * Real.log ↑n ∧ a₁.factorial * a₂.factorial ∣ n.factorial * (∏ i ∈ Finset.range r, Nat.nth Nat.Prime i) ^ n}.Infinite
number theoryfactorialsN/A6 sources
declared proved (Lean) · formalizederdos:403
True ↔ {p | (∀ a ∈ p.2, 0 < a) ∧ 2 ^ p.1 = ∑ a ∈ p.2, a.factorial}.Finite
number theoryfactorialsN/A4 sources
declared proved (Lean) · formalizederdos:646
True ↔ ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → {n | ∀ p ∈ S, Even (padicValNat p n.factorial)}.Infinite
number theoryfactorialsN/A5 sources
declared proved (Lean) · formalizederdos:728
Whether there are infinitely many integers a,b,na, b, n with a,b≥εna, b \ge \varepsilon n such that a!⋅b!a!\cdot b! divides n!⋅(a+b−n)!n!\cdot(a+b-n)! while a+ba+b exceeds nn by more than C⋅log⁡nC\cdot\log n.
number theoryfactorialsN/A6 sources
declared proved (Lean) · formalizederdos:729
True ↔ ∀ C > 0, ∃ K ≥ 3, {(a, b, n) | a > 0 ∧ b > 0 ∧ n > 0 ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ∀ (p : ℕ), Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite
number theoryfactorialsN/A6 sources

Search problems.science

Find a Problem, Result, source, or page