{"id":"palomar/PALOMAR-2026-09-21-000001","url":"https://github.com/Inspectordaniel/metric-surgery-lean/tree/91c2fc65884c9b284fdc6ba4071aa63c12ded471","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-21-000001-v1.json","repo":"https://github.com/Inspectordaniel/metric-surgery-lean","tags":["math.FA","msc:49Q15","msc:30L99","msc:28A75","functional-analysis","metric-currents","geometric-measure-theory","lean"],"score":0,"title":"An atomic decomposition of one-dimensional metric currents without boundary","trust":"high","domain":"math.FA","source":"palomar","authors":["Daniel Spector (NTNU, Taipei)"],"reviews":0,"subject":"math.FA","summary":"This project formalizes all five main results of arXiv:2502.09871, \"An atomic decomposition of one-dimensional metric currents without boundary\" (Chen, Goodman, Hernandez, Spector), in Lean 4 against Mathlib.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-21","reactions":{},"formalized":true,"formalizes":[{"title":"An atomic decomposition of one-dimensional metric currents without boundary","identifier":"arXiv:2502.09871","relationship":"formalizes"}]}