{"id":"palomar/PALOMAR-2026-09-02-000011","url":"https://github.com/CoolRmal/Besicovitchs-1-2/tree/8b0e98aa712374c96da7e619624f5b36ed8d5fd3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000011-v2.json","repo":"https://github.com/CoolRmal/Besicovitchs-1-2","tags":["math.CA","math.MG","msc:28A75","msc:28A78","msc:49Q15","msc:68V20","msc:90C05","geometric-measure-theory","rectifiability","lean-formalization"],"score":0,"title":"A machine-checked bound of 0.6934 for Besicovitch's 1/2-problem","trust":"high","domain":"math.CA","source":"palomar","authors":["Yongxi Lin"],"reviews":0,"subject":"math.CA","summary":"Besicovitch's 1/2-conjecture asserts that a Borel set in the plane with finite one-dimensional Hausdorff measure whose lower density exceeds 1/2 almost everywhere is countably 1-rectifiable. Writing sigma_1(R^2) for the least threshold that forces countable 1-rectifiability, the conjecture is sigma_1(R^2) = 1/2. The previously published record is sigma_1(R^2) <= 7/10, obtained by De Lellis, Glaudo, Massaccesi and Vittone. This development proves, with a complete Lean 4 proof term, sigma_1(H) <= 6934/10000 = 0.6934 for every real Hilbert space H, without finite-dimensionality or separability…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-20","reactions":{},"formalized":true}