{"id":"palomar/PALOMAR-2026-10-07-000005","url":"https://github.com/BenKeene/semigroup-betti/tree/c94da4f5cb07e2ccf62c9ae18887aedd73e95bf2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-07-000005-v1.json","repo":"https://github.com/BenKeene/semigroup-betti","tags":["math.AC","math.CO","msc:13D02","msc:20M14","msc:13F65","msc:05E40","numerical-semigroups","commutative-algebra","betti-numbers","lean-formalization"],"score":0,"title":"Linear upper bounds for the first Betti number of four-generated numerical semigroups","trust":"high","domain":"math.AC","source":"palomar","authors":["Ben Keene"],"reviews":0,"subject":"math.AC","summary":"A Lean 4 formalization, against Mathlib, of the theorem that the first Betti number (minimal number of generators of the toric ideal) of a numerical semigroup minimally generated by four elements n0 = 4 (an informal companion result; sharpness is not formalized).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-07","reactions":{},"formalized":true}