Skip to content

Problems · Vela Mathematics Program

Narrowed tosource:williamjblair-lean-proofs ×Clear all

Problem ledger

15 problemsGraph view
declared open · formalizederdos:130
For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.
graph theorychromatic numberN/A4 sources
declared proved (Lean) · formalizederdos:154
True ↔ ∀ (m : ℕ), 2 ≤ m → ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ), Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop → (∀ (k x : ℕ), x ∈ A k → x ≤ N k) → (∀ (k : ℕ), IsSidon ↑(A k)) → Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) → ∀ i < m, Filter.Tendsto (fun k => ↑{s ∈ A k + A k | s % m = i}.card / ↑(A k + A k).card) Filter.atTop (nhds (1 / ↑m))
sidon setsN/A6 sources
declared open · formalizederdos:254
If A⊆NA \subseteq \mathbb{N} has unbounded dyadic-shell counts and ∑n∈A∥θn∥=∞\sum_{n \in A} \|\theta n\| = \infty for every 0<θ<10 < \theta < 1, must AA be complete - is every sufficiently large integer a sum of distinct elements of AA?
number theoryN/A4 sources
declared open · formalizederdos:267
If n1<n2<⋯n_1 < n_2 < \cdots with nk+1/nk≥c>1n_{k+1}/n_k \ge c > 1, must ∑k1/Fnk\sum_k 1/F_{n_k} be irrational? The proposed proof closes the range 1<c<21 < c < 2 left open by earlier criteria.
irrationalityN/A4 sources
declared open · formalizederdos:394
For the least tk(n)t_k(n) with n∣tk(n)(tk(n)+1)⋯(tk(n)+k−1)n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1), do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with c=1/2048c = 1/2048 admissible in the t2t_2 bound.
number theoryA3440054 sources
declared open · formalizederdos:450
How large must y(ε,n)y(\varepsilon, n) be so that every interval (x,x+y)(x, x+y) contains at most εy\varepsilon y integers having a divisor in (n,2n)(n, 2n)? The candidate proof gives the sharp fixed-ε\varepsilon order y=Θε(n)y = \Theta_\varepsilon(n), uniformly in the translate.
number theorydivisorsN/A4 sources
declared open · formalizederdos:489
If AA is a forbidden-divisor set with ∣A∩[1,x]∣=o(x)|A \cap [1,x]| = o(\sqrt{x}) and B={b1<b2<⋯ }B = \{b_1 < b_2 < \cdots\} the sifted set, must x−1∑bi<x(bi+1−bi)2x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2 converge to a finite limit?
number theoryN/A4 sources
declared open · formalizederdos:521
False ↔ Erdos521.Claim
analysispolynomialsprobabilityN/A4 sources
declared open · formalizederdos:522
For Pn(z)=∑k=0nεkzkP_n(z) = \sum_{k=0}^n \varepsilon_k z^k with independent uniform signs, does the number RnR_n of roots in ∣z∣≤1|z| \le 1 satisfy Rn/(n/2)→1R_n/(n/2) \to 1 almost surely? The manuscript proves the strong law with Rn=n/2+Oω(n149/150)R_n = n/2 + O_\omega(n^{149/150}).
analysispolynomialsprobabilityN/A4 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:730
True ↔ Erdos730.S.Infinite
number theorybinomial coefficientsbase representationsA1295154 sources
declared open · formalizederdos:769
For the least cutoff c(n)c(n) after which every kk occurs as the number of homothetic cubes in a decomposition of the unit nn-cube, is c(n)≫nnc(n) \gg n^n? The Lean proof shows c(n)=o(nn)c(n) = o(n^n) along odd dimensions.
number theorygeometryA014544 · possible4 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:959
How large can the difference between the largest and second-largest distance multiplicities be among nn planar points?
geometrydistancesN/A4 sources
declared open · formalizederdos:1188
Estimate the number F(x)F(x) of minimal distinct covering systems whose moduli all lie in [1,x][1, x]. The candidate proof gives log⁡log⁡F(x)/log⁡x→1\log\log F(x)/\log x \to 1, i.e. F(x)=exp⁡(x1+o(1))F(x) = \exp(x^{1+o(1)}).
number theorycovering systemspossible4 sources