Skip to content

Problems · Vela Mathematics Program

Narrowed togeometry ×source:vibemathed ×Clear all

Problem ledger

14 problemsGraph view
declared disproved (Lean) · formalized · $500erdos:90
Conjectured upper bound on how many pairs among nn points in the plane can be exactly one unit apart.
geometrydistancesA1867055 sources
declared falsifiableerdos:106
If f(n)f(n) is the maximum total side length of nn interior-disjoint squares packed in the unit square, is f(k2+1)=kf(k^2 + 1) = k? An exact rational configuration packs 1717 squares with total side length greater than 44, refuting the identity at k=4k = 4.
geometryN/A3 sources
declared openerdos:654
If nn planar points have no four concyclic, must some point determine (1−o(1))n(1 - o(1))n distinct distances? Failing that, can one always force more than (1/3+c)n(1/3 + c)n?
geometrydistancespossible3 sources
declared proved (Lean) · formalizederdos:659
True ↔ ∃ A, (∀ (n : ℕ), (A n).card = n ∧ ∀ S ⊆ A n, S.card = 4 → 3 ≤ EuclideanGeometry.distinctDistances S) ∧ (fun n => ↑(EuclideanGeometry.distinctDistances (A n))) =O[Filter.atTop] fun n => ↑n / √(Real.log ↑n)
geometrydistancespossible6 sources
declared openerdos:662
Among sufficiently large one-separated planar point sets, does the triangular lattice maximize the number of distances below each threshold? Explicit rational oblique lattices beat the triangular lattice under several closed- and strict-shell readings.
geometrydistancesN/A3 sources
declared openerdos:670
Erdős asked whether every nn-point set in Euclidean space whose pairwise distances are mutually at least 1 apart must have diameter at least (1+o(1))n2(1+o(1))n^2. Disproved: an explicit high-dimensional construction beats the conjectured constant.
geometrydistancesN/A2 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 disproved (Lean) · formalizederdos:846
False ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), ∀ ε > 0, A.Infinite → Erdos846.NonTrilinearFor A ε → Erdos846.WeaklyNonTrilinear A
geometryN/A6 sources
declared openerdos:953
What is the largest possible measure of a subset of a radius-RR disk in R2\mathbb{R}^2 containing no pair of points at a positive integer distance? A Poisson-Bessel kernel argument gives M(R)≪R1/2M(R) \ll R^{1/2}; with Sárközy's lower construction, M(R)=R1/2+o(1)M(R) = R^{1/2 + o(1)}.
geometrydistancesN/A3 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 disprovederdos:960
Erdős problem 960
geometrypossible3 sources
declared solvederdos:1089
Erdős problem 1089
geometrydistancespossible3 sources
declared solvederdos:1091
Erdős problem 1091
geometrychromatic numberN/A3 sources
declared disproved · formalizederdos:1092
False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)
geometrychromatic numberN/A5 sources