REVIEW 3 major objections 4 minor 14 references
Certified algorithms for numerical semigroups in Rocq
T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read Machine-checked proofs certify numerical semigroup algorithms
desk verdict Competent formalization effort whose central claim is unauditable because the Rocq sources are promised but never linked; otherwise the math is clean. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central mechanism is the gap-list representation: a numerical semigroup $M$ is identified with its sorted, duplicate-free list $g_M$ of gaps, so every algorithm works with a unique finite object. The generation side is carried by multiplicity index lists, decreasing lists of indices into the generator list, with a successor function $\mathrm{next}_m$; iterating it yields a complete enumeration of exactly the index lists in $L_m^{\geq}$. The combinatorial backbone is the lexicographic-ordering lemma that upgrades generation from all lists of length $k$ to length $k+1$, together with the theorem $\mathrm{mgen\_complete\_lt}$, which guarantees that after generating $k$ linear combinations, every element of $M$ below $|\mathrm{gen}L_{|a|-1}(k)|\cdot\min a$ has already appeared; this makes the stopping condition in the small-elements algorithm sound.
What would settle it
Compile the accompanying Rocq development and check that the named theorems apery_spec, lgen_complete, and mgen_complete_lt exist and type-check; then run the extracted algorithms on a small example such as generators {4, 7, 10} and compare the computed gaps and Apéry sets against direct definitional computation.
Extended reading notes
Core claim
On the paper's own terms, the central claim is that a numerical semigroup — a cofinite additive submonoid of $\mathbb{N}$ — can be represented inside Rocq as an ordered, duplicate-free list of its gaps, and that on top of this representation one can build certified algorithms for the multiplicity, the Apéry set with respect to any $n$, the small elements, the conductor, and the Frobenius number expressed through the conductor. The authors further prove that the computed Apéry set together with $n$ generates the semigroup, and that an enumerator of multiplicity index lists eventually produces exactly the semigroup generated by a given finite generator list. In the paper's telling, this is the first formalization of numerical semigroups in a proof assistant, and every invariant returned by the algorithms is accompanied by a machine-checked proof of correctness.
Load-bearing premise
The claim collapses if the Rocq code that the paper says accompanies it is not actually available and compilable, since the certified status is exactly the machine-checked proof, and one key lemma's proof is deferred to a textbook rather than formalized.
Editorial extensions
If this is right
- Every invariant produced by the certified functions (multiplicity, gaps, Apéry set, small elements, conductor) comes with a proof object establishing that it is the correct mathematical value.
- The equivalence theorem gives a constructive way to turn any decidable cofinite additive submonoid of $\mathbb{N}$ into the gap-list representation, so that representation is complete, not merely convenient.
- The theorem that the Apéry set with respect to $n$, together with $n$, generates $M$ makes the computation of a generating set from invariants a certified by-product.
- Future algorithms can be checked against this one: proving equivalence to the certified functions transfers correctness to the new implementations.
- Expressing Frobenius-related statements through the conductor keeps the development entirely in $\mathbb{N}$, avoiding a separate integer type.
Reading between the lines
- Editorial inference: the enumeration of multiplicity index lists is essentially a ranking of multisets over a finite alphabet, so the same combinatorial core could be reused to certify algorithms for other finitely generated commutative monoids.
- Editorial inference: because no complexity analysis is given, a natural next step is to benchmark the extracted algorithms against existing software and to add complexity bounds; the non-monotonicity of the linear-combination generator makes the stopping criterion worth stress-testing on larger generator sets.
- Editorial inference: the claim of being the first formalization is inherently search-dependent, so the durable contribution is the gap-list representation and the generation-to-gaps pipeline, which could be ported to other proof assistants or to generalized numerical semigroups.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper develops a Rocq (Coq) formalization of numerical semigroups, representing a semigroup by the sorted, duplicate-free list of its gaps. It presents certified algorithms for computing the multiplicity, the Apéry set, the small elements, the conductor, and the gaps list of the semigroup generated by a finite list of generators. Theorems 1–9 state correctness results for these algorithms, with informal proof sketches in the text, and the authors claim this is the first formalization of numerical semigroups in a proof assistant. The central component of the claimed contribution, however, is the machine-checked Rocq development, which is asserted to be public but is not actually linked or identified in the manuscript.
Significance. If the associated Rocq development exists, compiles, and contains exactly the named theorems, this would be a worthwhile contribution: it would give the first machine-checked proofs of correctness for algorithms computing standard invariants of numerical semigroups. The paper has genuine technical content: the adaptation of the Apéry-set definition to truncated subtraction in (1) is handled carefully, the use of gaps lists as a canonical representation is sensible, and Theorem 9 provides a concrete completeness bound that is falsifiable and useful. The constructive proof in Theorem 5 is also a nice feature. However, the verification of the central claim depends on access to the sources, and the manuscript as submitted does not provide a repository URL, commit hash, or build instructions. The proof of Lemma 1 is also explicitly omitted. These are not mathematical counterexamples, but they prevent the certified status from being independently confirmed from the paper alone.
major comments (3)
- [§4, Conclusions; §2.2 and §3.3 references to sources] The central claim that the algorithms are certified by Rocq is unauditable from the submitted manuscript. The introduction says 'Throughout the paper we provide ( links) to the Rocq sources', and §4 says 'Our formalization is public and counts ~3000 lines of Rocq code', but no repository URL, commit hash, or build instructions appear anywhere in the text. An auditor cannot check that the named theorems apery_spec, apery_2_correct, lgen_complete, mgen_complete_lt, and the small-elements correctness statement exist, state what the paper claims, or compile under a specified Rocq version. This issue is load-bearing for the main contribution and must be fixed, e.g. by including a stable link and commit hash plus build/compiler-version information.
- [§2.2, Lemma 1 (apery_spec_2)] The proof of Lemma 1 is explicitly omitted: 'We do not present the proof of this lemma here, since it is essentially a formalization of the (informal) proof given in [2].' Lemma 1 is not a peripheral fact: Theorem 3 and the generator property in Theorem 4 both depend on it. In a paper whose contribution is a formalization, a central lemma cannot simply be delegated to a textbook, especially because the paper's own adapted definition of the Apéry set in (1) differs from the textbook definition. Either the Rocq proof must be made available and cited at the level of the named theorem, or the proof strategy must be summarized in the text.
- [§3.3, Algorithm 1] The Small-Elements function in Algorithm 1 takes an unexplained fuel parameter n and loops 'while i < n', yet no theorem states how large n must be, no termination bound is given, and the behavior for too-small n is not specified. The informal correctness argument that precedes the algorithm is not tied to a named formal theorem or to a specific Rocq definition. Since computing small elements is one of the paper's advertised certified algorithms, this is a central gap. The authors should either state a formal specification of Small-Elements with an explicit termination condition and correctness theorem, or provide the corresponding Rocq statement and prove that the pseudocode is an accurate rendition of it.
minor comments (4)
- [§2.2, Definition 2] Definition 2 says Ap(g, n) is obtained 'by removing the elements in g from the lists t', which is a typo: the proof and the example indicate that the elements of g are removed from the concatenation s ++ t. The proof text 'x ∈ s t' also needs the explicit concatenation symbol.
- [§3.3, Theorem 9 discussion] In the paragraph after Theorem 9, the text says 'after generating k elements ... smaller than |genMa (k)| · m have been forgotten', but genMa(k) is a natural number and the intended expression is |genL_{|a|-1}(k)| · min a, as in the theorem statement. This should be corrected.
- [§1 and §2] The abstract and introduction list the Frobenius number among the computed invariants, but the text later notes that no explicit Frobenius function is implemented and only the conductor is computed. Since the Frobenius number is conductor minus one, this is harmless, but the wording should be aligned to avoid overstating what is formalized.
- [§3.1, Definition 4] The inference-rule presentation of next_m is hard to read: the sentence 'Note that nextm(t) cannot be the empty list, and so the third rule is never used' refers to a rule that is not clearly separated from the others in the typeset text. A cleaner functional definition with explicit cases would make the formalization easier for readers to compare with the Rocq definition.
Circularity Check
No circularity: algorithms are proved against standard external definitions, and cited results come from the literature, not from the authors' own prior work.
full rationale
The paper's derivation chain is self-contained in the relevant sense: Rocq definitions are given for gaps, multiplicity, Apéry set, small elements, conductor, and generation by a finite list, and the correctness theorems (multiplicity_min, apery_spec, apery_2_correct, apery_generates, lgen_correct/lgen_complete, mgen_complete, mgen_complete_lt) are proved against those definitions. The truncated-subtraction amendment to the Apéry set definition is an explicit representational choice that preserves the standard invariant, not a way to force the target theorem. Lemma 1 is deferred to the textbook [2] rather than proved in the paper, but it is an external mathematical result, not a result of the present authors, so it is independent support rather than a self-citation. Theorems 5 and the finite-generation statement are likewise cited from the standard literature. No fitted parameters are renamed as predictions, no quantity is defined in terms of the target result, and the authors do not invoke their own prior uniqueness theorems or ansatze to rule out alternatives. The absence of a repository URL or commit hash is a verifiability and reproducibility concern, not a circularity concern: it affects whether the Rocq sources can be independently audited, but it does not make any proof step equivalent to its input by construction.
Assumptions & free parameters
assumptions (4)
- domain assumption Every numerical semigroup is finitely generated
- domain assumption The Apéry set of a numerical semigroup with respect to n in M without 0 has exactly one element in each residue class modulo n
- domain assumption Decidability of membership for submonoids represented by a gaps list
- domain assumption A numerical semigroup is represented uniquely by a sorted duplicate-free finite list of its gaps
Cite this review
Pith. "Pith review of Certified algorithms for numerical semigroups in Rocq." pith.science (2026). https://pith.science/paper/P6PQIH3T
@misc{pith2026250523205,
author = {Pith},
title = {Pith review of: Certified algorithms for numerical semigroups in Rocq},
year = {2026},
howpublished = {\url{https://pith.science/paper/P6PQIH3T}},
note = {Machine review of arXiv:2505.23205}
}
read the original abstract
A numerical semigroup is a co-finite submonoid of the monoid of non-negative integers under addition. Many properties of numerical semigroups rely on some fundamental invariants, such as, among others, the set of gaps (and its cardinality), the Ap\'ery set or the Frobenius number. Algorithms for calculating invariants are currently based on computational tools, such as GAP, which lack proofs (either formal or informal) of their correctness. In this paper we introduce a Rocq formalization of numerical semigroups. Given the semigroup generators, we provide certified algorithms for computing some of the fundamental invariants: the set of gaps, of small elements, the Ap\'ery set, the multiplicity, the conductor and the Frobenius number. To the best of our knowledge this is the first formalization of numerical semigroups in any proof assistant.
Reference graph
Works this paper leans on
-
[2]
Assi, A., D’Anna, M., García-Sánchez, P.A.: Numerical Semigroups and Applica- tions. Springer (2020)
work page 2020
-
[1]
The GAP-Group, GAP – Groups, Algorithms, and Programming, version 4.12.2, (2022), https://www.gap-system.org
work page 2022
-
[3]
Journal of Commutative Algebra2(3) (2010).https://doi.org/10.1216/ JCA-2010-2-3-281
Barucci, V.: Decompositions of ideals into irreducible ideals in numerical semi- groups. Journal of Commutative Algebra2(3) (2010).https://doi.org/10.1216/ JCA-2010-2-3-281
work page 2010
-
[4]
The Electronic Journal of Combinatorics12 (2005)
Beihoffer, D., Hendry, J., Nijenhuis, A., Wagon, S.: Faster algorithms for Frobenius numbers. The Electronic Journal of Combinatorics12 (2005). https://doi.org/ 10.37236/1924
-
[5]
Blanco, V., García-Sánchez, P.A., Puerto, J.: Counting numerical semigroups with short generating functions. International Journal of Algebra and Compu- tation 21(07), 1217–1235 (2011).https://doi.org/10.1142/S0218196711006911, https://doi.org/10.1142/S0218196711006911
-
[6]
Journal of the London Mathematical So- ciety 60(2), 420–430 (10 1999)
Campillo, A., Delgado, F., Gusein-Zade, S.M.: On generators of the semi- group of a plane curve singularity. Journal of the London Mathematical So- ciety 60(2), 420–430 (10 1999). https://doi.org/10.1112/S0024610799007917, https://doi.org/10.1112/S0024610799007917
-
[7]
Journal of Algebra and Its Applications20(05) (2021)
Cisto, C., Delgado, M., García-Sánchez, P.A.: Algorithms for generalized numerical semigroups. Journal of Algebra and Its Applications20(05) (2021). https://doi. org/10.1142/S0219498821500791
-
[8]
Delgado, M., García-Sánchez, P.A., Morais, J.: NumericalSgps, A package for numerical semigroups, version 1.4.0 (2024), Refereed GAP package, https:// gap-packages.github.io/numericalsgps 15
work page 2024
Show all 14 references
-
[9]
IEEE Transactions on Information Theory60(1), 282–295 (2014).https://doi.org/10.1109/TIT.2013
Delgado, M., Farrán, J.I., García-Sánchez, P.A., Llena, D.: On the weight hierar- chy of codes coming from semigroups with two generators. IEEE Transactions on Information Theory60(1), 282–295 (2014).https://doi.org/10.1109/TIT.2013. 2285217
2014 doi
-
[10]
Journal für die reine und angewandte Mathematik336, 165–184 (1982), http://eudml.org/ doc/152474
García, A.: Semigroups associated to singular points of plane curves. Journal für die reine und angewandte Mathematik336, 165–184 (1982), http://eudml.org/ doc/152474
1982
-
[11]
Oxford University Press (2005)
Ramírez-Alfonsín, J.L.: The Diophantine Frobenius Problem. Oxford University Press (2005)
2005
-
[12]
Springer (2009)
Rosales, J.C., García-Sánchez, P.A.: Numerical Semigroups. Springer (2009)
2009
-
[13]
Semigroup Forum67(1), 145–158 (2003), https://doi.org/10.1007/s00233-002-0007-3
Rosales, J.C., García-Sánchez, P.A., García-García, J.I., Jiménez Madrid, J.A.: The oversemigroups of a numerical semigroup. Semigroup Forum67(1), 145–158 (2003), https://doi.org/10.1007/s00233-002-0007-3
2003 doi
-
[14]
Journal of Pure and Applied Algebra 189(1), 301–313 (2004)
Rosales, J.C., García-Sánchez, P.A., García-García, J.I., Jiménez-Madrid, J.A.: Fundamental gaps in numerical semigroups. Journal of Pure and Applied Algebra 189(1), 301–313 (2004). https://doi.org/https://doi.org/10.1016/ j.jpaa.2003.10.024, https://www.sciencedirect.com/scie...
2004
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.