Abstract

Let $$H$$ be a real Hilbert space. We prove that if $$a>0.6934$$ and $$E\subset H$$ is Borel, $$\mathcal H^1(E)<\infty$$, and $$\Theta^1_*(E,x)\ge a$$ for $$\mathcal H^1$$-almost every $$x\in E$$, then $$E$$ is countably $$1$$-rectifiable. Most of the proof and its formalization were generated by AI under human direction.

1 Introduction and notation

Definition 1.1 (Straight measure). A Borel measure $$\mu$$ on $$H$$ is straight¹ if $$\mu(A)\le\operatorname{diam} A$$ for every Borel set $$A\subset H$$.

Definition 1.2 (Rectifiability threshold). Define

$$\sigma_1(H):=\inf\left\{a\ge0: \begin{gathered} \Theta^1_*(E,x)\ge a\text{ for }\mathcal H^1\text{-a.e. }x\in E\\ \Longrightarrow E\text{ is countably }1\text{-rectifiable} \end{gathered}\right\},$$

where $$E$$ ranges over Borel sets with $$\mathcal H^1(E)<\infty$$.

Definition 1.3 (Besicovitch pair condition). The space $$H$$ satisfies $$\mathrm{BPC}(\beta)$$ if, for every straight measure $$\mu$$, there is $$\tau>0$$ such that for every $$\lambda>0$$ there is $$\delta>0$$ with the following property. If $$E_1,E_2$$ are nonempty Borel sets with $$0<\operatorname{dist}(E_1,E_2)<\delta$$ and $$\mu(B(x,r))>2\beta r$$ for $$x\in E_1\cup E_2$$ and $$0<r<\lambda$$, then there is an open set $$V$$ meeting both $$E_1$$ and $$E_2$$ such that $$\mu(V\setminus(E_1\cup E_2))>\tau\operatorname{diam}V$$. We say that $$V$$ leaks¹ from $$E_1\cup E_2$$.

Preiss–Tišer [PT92] showed that $$\mathrm{BPC}(\beta)\Longrightarrow\sigma_1(H)\le\beta$$. Thus we seek to establish $$\mathrm{BPC}(\beta)$$ for $$\beta$$ as close to $$1/2$$ as possible. De Lellis, Glaudo, Massaccesi, and Vittone [De +26] introduced an optimization framework and proved $$\sigma_1(\mathbb R^2)\le0.7$$. We propose a different optimization problem to obtain $$\sigma_1(H)\le0.6934$$.

2 The six-point game

Definition 2.1 (Admissible configuration and score). An admissible six-point configuration at $$s\in(1/2,1]$$ consists of blue points $$o,p_1,p_2$$ and red points $$e,q_1,q_2$$ such that $$d(o,e)=1$$, $$d(o,p_i),d(e,q_i)\le1$$, and $$d(p_1,p_2),d(q_1,q_2)\ge2s$$. The six labelled points need not be distinct. A move selects at least one point of each colour and assigns radii $$r_i\in[0,1]$$ to each selected point such that $$r_i+r_j\le d(x_i,x_j)$$ whenever $$i\ne j$$ and $$x_i,x_j$$ have the same colour, which guarantees that balls of the same colour are disjoint. The virtual diameter and score of a move are

$$D:=\max_{i,j}\bigl(d(x_i,x_j)+r_i+r_j\bigr),\qquad S_s:=\sum_i r_i-\frac{D}{2s}.$$

The six-point property holds at $$s$$ if every admissible configuration has a move with $$S_s\ge0$$.

Figure 1. The six-point game. Each sibling segment has length at least $$2s$$.

Theorem 2.1. If the six-point property holds at $$s$$, then $$H$$ satisfies $$\mathrm{BPC}(\beta)$$ for every $$\beta>s$$. Consequently, $$\sigma_1(H)\le s$$.

Proof. Fix $$\beta>s$$ and choose $$q\in(s/\beta,1)$$. Choose $$\tau>0$$ so small that

$$\tau(2+q^{-1})<2(\beta-s/q),\qquad (1+\tau)s<\beta q.$$

Let $$\mu$$ be straight. Given $$\lambda>0$$, set $$\delta=\lambda$$ and take $$E_1,E_2$$ as in Definition 1.3. Write $$d=\operatorname{dist}(E_1,E_2)$$. Choose roots $$x_i\in E_i$$ with $$d\le\ell:=d(x_1,x_2)<d/q$$ and put $$U=B(x_1,d)\cup B(x_2,d)$$. If $$U$$ leaks, then we are done. Otherwise,

$$\mu(U\setminus(E_1\cup E_2))\le\tau\operatorname{diam}U <\tau(2+q^{-1})d.$$

Each root ball misses the opposite set. Since $$d<\lambda$$, the density hypothesis gives,

$$\begin{aligned} 2\beta d&<\mu(B(x_i,d))\\ &=\mu(B(x_i,d)\cap E_i)+\mu(B(x_i,d)\setminus E_i)\\ &\le\mu(B(x_i,d)\cap E_i)+\mu(U\setminus(E_1\cup E_2))\\ &<\mu(B(x_i,d)\cap E_i)+\tau(2+q^{-1})d. \end{aligned}$$

Thus straightness implies

$$\begin{aligned} \operatorname{diam}(B(x_i,d)\cap E_i)&\ge\mu(B(x_i,d)\cap E_i)\\ &>2\beta d-\tau(2+q^{-1})d\\ &>2sd/q>2s\ell. \end{aligned}$$

Hence we can choose $$x_{i1},x_{i2}\in B(x_i,d)\cap E_i$$ with $$d(x_{i1},x_{i2})>2s\ell$$. Dividing all distances by $$\ell$$ gives an admissible six-point configuration, with the points in $$E_1$$ blue and those in $$E_2$$ red.

Take a nonnegative-score move. Denote its selected centres by $$y_j$$, its radii by $$r_j$$, and its virtual diameter by $$D$$. The six-point property gives $$D\le2s\sum_j r_j$$. Since the move selects both colours, we have $$D>0$$ and hence $$\sum_j r_j>0$$. For each $$r_j>0$$, consider the ball $$B(y_j,q\ell r_j)$$. This ball misses the opposite set and since $$q\ell r_j<d<\lambda$$, $$\mu(B(y_j,q\ell r_j))>2\beta q\ell r_j$$. Balls of the same colour are disjoint, because $$q\ell(r_i+r_j)\le q\,d(y_i,y_j)<d(y_i,y_j)$$. Consequently, a point lying in two such balls does not belong to $$E_1\cup E_2$$.

It is possible that the radius of a selected centre is zero in this move, so for all $$\varepsilon>0$$, we consider the set $$V_\varepsilon=\bigcup_j B(y_j,q\ell r_j+\varepsilon)$$. This open set meets both $$E_1$$ and $$E_2$$, and $$\operatorname{diam}V_\varepsilon\le\ell D+2\varepsilon$$. The aforementioned overlap observation gives the pointwise bound

$$\sum_{j:r_j>0}\mathbf1_{B(y_j,q\ell r_j)} \le\mathbf1_{V_\varepsilon}+\mathbf1_{V_\varepsilon\setminus(E_1\cup E_2)}.$$

Integrating with respect to $$\mu$$ and assuming that $$V_\varepsilon$$ does not leak for any $$\varepsilon>0$$, we obtain

$$\begin{aligned} 2\beta q\ell\sum_j r_j&<\sum_{j:r_j>0}\mu(B(y_j,q\ell r_j))\\ &\le\mu(V_\varepsilon)+\mu(V_\varepsilon\setminus(E_1\cup E_2))\\ &\le(1+\tau)\operatorname{diam}V_\varepsilon\\ &\le(1+\tau)(\ell D+2\varepsilon). \end{aligned}$$

Letting $$\varepsilon\downarrow0$$ and using $$D\le2s\sum_j r_j$$, we obtain $$2\beta q\ell\sum_j r_j\le2(1+\tau)s\ell\sum_j r_j$$. As $$0<\sum_j r_j$$, this inequality contradicts $$(1+\tau)s<\beta q$$. Hence, one of the $$V_\varepsilon$$ leaks and $$\mathrm{BPC}(\beta)$$ holds. □

3 AI-generated formalization in Lean

Theorem 3.1 (Machine-checked bound). $$\sigma_1(H)\le0.6934$$.

The author does not understand the proof of this theorem. However, the proof has been verified in Lean and uses Theorem 2.1. The code is available at github.com/CoolRmal/Besicovitchs-1-2. The repository includes a Lean Comparator check. The result is also registered on Palomar at PALOMAR-2026-09-02-000011 (version 1).

Theorem 3.1 is also compelling when viewed in comparison with the method of Preiss–Tišer [PT92]: their argument uses information from only one of the sets $$E_1$$ and $$E_2$$, whereas Theorem 2.1 exploits information from both.

Let $$s_*$$ denote the infimum of all $$s$$ for which the six-point property holds at $$s$$. An initial AI-generated proof established that $$s_*$$ is algebraic and $$s_*\approx0.6933064218$$. Formalizing that argument requires substantially more computation, so the author chose the weaker threshold $$0.6934$$.

4 Potential improvements

In the proof of Theorem 2.1, we consider two cases according to whether $$B(x_1,d)\cup B(x_2,d)$$ leaks, and we extract six points in the case that it does not leak. We can then also consider two cases according to whether $$\bigcup_{i=1}^6 B(x_i,d)$$ leaks. In the case that this union of six balls does not leak, for each colour, we can extract one root, two children, and four grandchildren, suggesting a fourteen-point game. An AI-guided numerical search suggested that this larger game may remain nonnegative near $$s=0.65$$, but this is not verified in Lean as it is much more computationally heavy.

Acknowledgement

The author thanks Professor Robin Neumayer for helpful discussions.

References

[De +26]

Camillo De Lellis, Federico Glaudo, Annalisa Massaccesi, and Davide Vittone. “Besicovitch’s 1/2 Problem and Linear Programming”. In: Transactions of the American Mathematical Society 379.7 (2026), pp. 5051–5098. DOI: 10.1090/tran/9609. arXiv: 2404.17536.

[PT92]

David Preiss and Jaroslav Tišer. “On Besicovitch’s 1/2-Problem”. In: Journal of the London Mathematical Society. 2nd ser. 45.2 (1992), pp. 279–287. DOI: 10.1112/jlms/s2-45.2.279.