Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×formalized ×source:gpt-erdos ×Clear all

Problem ledger

19 problemsGraph view
declared open · formalizederdos:91
(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ True
geometrydistancesA186704 · possible3 sources
declared open · formalized · $10000erdos:142
∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry
additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources
declared open · formalizederdos:274
sorry ↔ ∀ (G : Type u_1) [inst : Group G], 1 < ENat.card G → ∀ (ι : Type u_2) [inst_1 : Fintype ι] (P : Erdos274.Group.ExactCovering G ι), 1 < Fintype.card ι → ∃ i j, i ≠ j ∧ Cardinal.mk ↥(P.parts i) = Cardinal.mk ↥(P.parts j)
group theorycovering systemsN/A3 sources
declared open · formalizederdos:302
∀ (f : ℕ → ℕ), (∀ (N : ℕ), Erdos302.IsMaxNoTripleCard N (f N)) → Filter.Tendsto (fun N => ↑(f N) / ↑N) Filter.atTop (nhds sorry)
number theoryunit fractionsA3903953 sources
declared open · formalizederdos:332
∀ (A : Set ℕ), sorry A → Erdos332.HasBoundedGaps (Erdos332.D_A A)
number theoryN/A3 sources
declared open · formalizederdos:517
sorry ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (k : ℕ), a k ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → ∀ (z : ℂ), {x | f x = z}.Infinite
analysisN/A3 sources
declared open · formalizederdos:538
If each integer has at most rr representations m=pam = pa with pp prime and a∈A⊆[1,N]a \in A \subseteq [1, N], what is the best upper bound for ∑a∈A1/a\sum_{a \in A} 1/a? The candidate proof gives the matching order Θr(log⁡N/log⁡log⁡N)\Theta_r(\log N / \log\log N).
number theoryN/A5 sources
declared open · formalizederdos:539
For ∣A∣=n|A| = n, how small can the cofactor set Q(A)={a/gcd⁡(a,b):a,b∈A}Q(A) = \{a / \gcd(a,b) : a, b \in A\} be? The answer is h(n)=n1/2+o(1)h(n) = n^{1/2 + o(1)}: a new upper bound h(n)≤n1/2exp⁡(O(log⁡n))h(n) \le n^{1/2} \exp(O(\sqrt{\log n})) matches the classical lower bound.
number theorypossible5 sources
declared open · formalizederdos:602
¬Erdos602.disjoint_without_infinite_claim
combinatoricsset theoryN/A3 sources
declared open · formalizederdos:655
False ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))), X.card = n → Erdos655.IsValid X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)
geometrydistancespossible3 sources
declared open · formalizederdos:686
sorry ↔ ∀ N ≥ 2, ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
number theoryN/A4 sources
declared open · formalizederdos:726
True ↔ Asymptotics.IsEquivalent Filter.atTop (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n => Real.log (Real.log ↑n) / 2
number theoryN/A3 sources
declared open · formalizederdos:796
If g3(n)g_3(n) is the largest size of A⊆[1,n]A \subseteq [1,n] with fewer than three representations of every product a1a2a_1 a_2, does its conjectured second-order normalized term converge? The candidate proof gives an explicit limit constant.
number theorypossible5 sources
declared open · formalizederdos:850
True ↔ ∃ x y, x ≠ y ∧ x.primeFactors = y.primeFactors ∧ (x + 1).primeFactors = (y + 1).primeFactors ∧ (x + 2).primeFactors = (y + 2).primeFactors
number theoryprimesA3431013 sources
declared open · formalizederdos:893
True ↔ Filter.Tendsto (fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n)) Filter.atTop Filter.atTop
number theorydivisorsA046801 · possible3 sources
declared open · formalizederdos:906
Is there an entire non-zero function f:C→Cf:\mathbb{C}\to \mathbb{C} such that, for any infinite sequence n1<n2<⋯n_1<n_2<\cdots, the set {z:f(nk)(z)=0 for some k≥1}\{ z: f^{(n_k)}(z)=0 \textrm{ for some }k\geq 1\} is everywhere dense? The literal question is trivial for polynomials, so the claims address the transcendental entire case, in the affirmative.
analysisiterated functionsN/A5 sources
declared open · formalizederdos:943
True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(AdditiveCombinatorics.sumRep Nat.Powerful n) ≤ ↑n ^ o n
number theorypossible4 sources
declared open · formalizederdos:1063
have upper_bound := sorry; (fun k => ↑(Erdos1063.n k)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun k => ↑k * (Finset.Icc 1 (k - 1)).lcm fun n => ↑n
number theoryA3893603 sources
declared open · formalizederdos:1084
∀ {n : ℕ}, n ≠ 0 → Erdos1084.f 2 n < 3 * n
geometrydistancesA045945 · possible3 sources

Search problems.science

Find a Problem, Result, source, or page