# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json # formalization.yaml v0.4 — adopted from https://github.com/mathlib-initiative/formalization.yaml version: "v0.4" project: name: "Linear upper bounds for the first Betti number of four-generated numerical semigroups" description: >- 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 < n1 < n2 < n3 is at most 2W, where W = (n3 - n0) / gcd(n1 - n0, n2 - n0, n3 - n0); in particular at most twice the width n3 - n0. This replaces the conjectured quadratic bound (w+1 choose 2) of Herzog–Stamate (2014) and Caviglia–Moscariello–Sammartano (2024) in embedding dimension four; the bound 2w is attained for every width w >= 4 (an informal companion result; sharpness is not formalized). authors: - "Ben Keene" license: "Apache-2.0" responsible_maintainers: - "Ben Keene" repository: role: substantive-development classification: arxiv: [math.AC, math.CO] msc2020: ["13D02", "20M14", "13F65", "05E40"] status: scope: >- COMPLETE (2026-10-06). Both theorems of record (upper bounds) are proved in Solution.lean by thin bridges into the development library SemigroupBetti/ (2,431 lines): the combinatorial invariant beta1 (fiber graphs of factorizations in N^4), the bound beta1 <= 2W (Lemmas 1-16 of the informal write-up), and the bridge spanRank(toric ideal) <= beta1. Not formalized: sharpness of the bound and the reverse inequality beta1 <= spanRank. The only two sorrys in the repository are the deliberate holes in Challenge.lean (Comparator convention); both Solution theorems depend on exactly propext, Classical.choice and Quot.sound. Built with `lake build` on Lean v4.35.0-rc3 / Mathlib v4.35.0-rc3 (c55e6e786f), all files in the module system (9036 jobs). sorry_count: 2 sorry_in_definitions: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] main_results: - "SemigroupBetti.beta1_le_two_mul_normalizedWidth" - "SemigroupBetti.beta1_le_two_mul_width" fidelity: divergences: >- The informal theorem is stated for the cardinality of a minimal presentation of the semigroup; the formal statement bounds Submodule.spanRank of the toric ideal ker(K[X0..X3] -> K[t], Xi |-> t^(n i)), which equals the minimal number of generators of the ideal. Minimal generation of the semigroup is stated as: no n i lies in the additive submonoid generated by the other three. Sharpness (the bound is attained) is not part of the formal statement. sources: - title: "Linear upper bounds for the first Betti number of four-generated numerical semigroups (result first presented by this formalization)" authors: ["Ben Keene"] type: "original-proof" relationship: other note: >- Unpublished manuscript. The informal proofs were produced with AI assistance (see automation.methods). The combinatorial proof (support counting on factorization graphs) is the one formalized. A second, independent proof via Minkowski's second theorem and a complete intersection (PROOF.md) is not formalized. - title: "Bounds for syzygies of monomial curves" authors: ["Giulio Caviglia", "Alessio Moscariello", "Alessio Sammartano"] type: "article" id: "https://doi.org/10.1090/proc/16862" relationship: background note: "Conjecture 1.3 (the quadratic width bound) and Theorem 1.5 (embedding dimension four, width >= 40)." - title: "On the defining equations of the tangent cone of a numerical semigroup ring" authors: ["Jürgen Herzog", "Dumitru I. Stamate"] type: "article" id: "https://doi.org/10.1016/j.jalgebra.2014.07.008" relationship: background note: "Conjecture 2.1, the origin of the width conjecture." related_formalizations: [] automation: methods: - method: agent models: ["Claude Fable 5.1 (Anthropic)", "Claude Opus 5.5 (Anthropic)", "GPT-6 Astra (OpenAI)"] framework: "Claude Code; Codex app-server (for GPT-6 Astra)" tool_setup: >- Claude Code agents (Fable 5.1 directing, Opus 5.5 coding subagents) writing Lean against a local Lean/Mathlib toolchain with `lake build` feedback; GPT-6 Astra invoked through the Codex app-server as independent prover and adversarial reviewer of the informal proof. cost: wall_time: "not tracked" spend_usd: "subscription-based" hardware: "local machine (Apple silicon Mac) plus API/subscription model access" prompting_notes: >- Astra was given role prompts (independent prover, adversary, reviewer) and never told that a proposed argument was probably right; Lean work was driven stage by stage from an explicit lemma-by-lemma write-up. spend_usd: "subscription-based" notes: >- The informal proofs were found by GPT-6 Astra acting as an independent prover, reviewed adversarially by further Astra runs, and checked line by line by Claude; the explicit Lean-oriented write-up was produced by Astra. The Lean source was written by Claude (Fable 5.1 directing, Opus 5.5 coding agents) in Claude Code under the direction and review of the author, who selected the target, made the mathematical decisions and audited the Challenge statements against the informal theorem. review: status: self-assessed reviewers: - "Ben Keene" notes: >- The informal proof passed two independent adversarial reviews and one reviewer pass (GPT-6 Astra) and exhaustive computational checks for all widths <= 39. No external human review has been performed. Every formal step is checked by Lean. known_gaps: [] limitations: - >- The mathematical result is new (no prior statement located in the literature as of 2026-10-06); novelty is asserted on the basis of literature audits, not of publication. - >- Sharpness of the bound is established informally only. - >- The reverse bridge inequality (the combinatorial invariant is at most spanRank, hence equal to it) is not formalized; it is not needed for the statements of record. alignment: namespace: "SemigroupBetti" statements: - source: "Main theorem: beta_1(S) <= 2W for every minimally four-generated numerical semigroup" lean: "SemigroupBetti.beta1_le_two_mul_normalizedWidth" module: "Challenge (statement), Solution (proof)" status: proved note: >- The formal statement bounds Submodule.spanRank of the toric ideal; the informal theorem bounds the cardinality of a minimal presentation. Only the inequality spanRank <= beta1 is formalized (the bridge Lemma 0 in the direction needed); the equality mu(I) = beta1 is informal only. - source: "Corollary: beta_1(S) <= 2 wd(S)" lean: "SemigroupBetti.beta1_le_two_mul_width" module: "Challenge (statement), Solution (proof)" status: proved acknowledgements: >- Mathlib and the Lean FRO toolchain (Lean, Lake, lake comparator); the PalomarTemplate verification scripts.