Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×factorials ×Clear all

Problem ledger

16 problemsGraph view
declared open · formalizederdos:18
∀ᶠ (n : ℕ) in Filter.atTop, Erdos18.practicalH n.factorial < n
number theorydivisorsfactorialsA0051532 sources
declared open · formalizederdos:373
Erdos373.S.Finite
number theoryfactorialsA0031352 sources
declared open · formalizederdos:390
Let f(n)f(n) be the least mm for which n!n! can be written as a1⋯aka_1\cdots a_k with n<a1<⋯<ak=mn < a_1 < \cdots < a_k = m - the smallest possible largest factor in a factorization of n!n! into distinct integers all exceeding nn. Erdős, Guy and Selfridge proved f(n)−2n≍n/log⁡nf(n) - 2n \asymp n/\log n. Erdős asked whether there is a constant cc with f(n)−2n∼c nlog⁡n,f(n) - 2n \sim c\,\frac{n}{\log n}, and what it is. This preprint answers yes and names the constant: lim⁡n→∞(f(n)−2n)log⁡nn=402963959825970038185≈0.15516.\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.
number theoryfactorialsA1934294 sources
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 falsifiable · formalizederdos:398
sorry ↔ {n | ∃ m, n.factorial + 1 = m ^ 2} = {4, 5, 7}
number theoryfactorialsA146968 · A1413992 sources
declared disproved (Lean) · formalizederdos:399
False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)
number theoryfactorialsN/A5 sources
declared open · formalizederdos:400
True ↔ ∀ k ≥ 2, ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x => c * ↑x * Real.log ↑x
number theoryfactorialspossible3 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 solved (Lean) · formalizederdos:419
{x | MapClusterPt x Filter.atTop Erdos419.factorialDivisorRatio} = Erdos419.limitPointSet
number theoryfactorialsN/A5 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 open · formalizederdos:727
True ↔ ∀ k ≥ 2, {n | (n + k).factorial ^ 2 ∣ (2 * n).factorial}.Infinite
number theoryfactorialsA002503 · A343507 · A3893962 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
declared open · formalizederdos:912
∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => c * (↑n / Real.log ↑n) ^ (1 / 2)
number theoryfactorialsA0716262 sources
declared open · formalizederdos:1108
True ↔ ∀ k ≥ 2, {a | a ∈ Erdos1108.FactorialSums ∧ ∃ m, m ^ k = a}.Finite
number theoryfactorialsA051761 · A115645 · A0254942 sources

Search problems.science

Find a Problem, Result, source, or page