pith. sign in

arxiv: 2606.09600 · v1 · pith:XPPRCVSZnew · submitted 2026-06-08 · 💻 cs.IT · math.IT

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Andreas Florath This is my paper

Pith reviewed 2026-06-27 14:43 UTC · model grok-4.3

classification 💻 cs.IT math.IT
keywords covering codesformal verificationLean 4q-ary Hamming spacesphere covering boundproof-carrying certificatesK_q(n,r)
0
0 comments X

The pith

Lean 4 supplies machine-checked certificate predicates for upper and lower bounds on the minimal size of q-ary covering codes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds a Lean 4 library that defines predicates capturing upper bounds, lower bounds, and exact values for the covering number K_q(n,r). It proves the volume formula for q-ary Hamming balls, the sphere-covering lower bound, product constructions, and selected exact small cases. An end-to-end workflow then transcribes explicit upper bounds from an existing table and verifies them inside Lean, storing each bound together with a replayable proof trace. The result is a reusable, auditable foundation rather than new numerical records.

Core claim

Certificate predicates for upper bounds, lower bounds, and exact covering numbers K_q(n,r) can be defined so that Lean 4 can both prove elementary properties of covering codes and check concrete numerical bounds transcribed from the literature, yielding a proof-carrying database of those bounds.

What carries the argument

Certificate predicates for upper bounds, lower bounds, and exact values of K_q(n,r), which encode the covering property and allow Lean to replay proofs of those predicates.

If this is right

  • Any bound stored in the database comes with a Lean trace that can be replayed to confirm the predicate.
  • Product and relation rules can be applied formally to derive new certificates from existing ones.
  • Small exact values can be certified by exhibiting a covering set and proving minimality via the lower-bound predicate.
  • The same machinery applies uniformly to any q, n, and r once the Hamming-ball volume formula is in place.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach could be extended to larger parameter ranges by importing more bounds and running the checker on them.
  • Similar certificate predicates could be written for related objects such as error-correcting codes or constant-weight codes.
  • The database format makes it possible to compare bounds across independent sources by checking which ones survive the formal predicates.

Load-bearing premise

The transcribed upper bounds from the 1989 table are represented correctly in Lean and the predicate definitions match the intended mathematical notions of covering.

What would settle it

A concrete upper-bound certificate that Lean accepts but whose corresponding covering set fails to cover the space, or a discrepancy between a Lean-proved lower bound and an explicit exhaustive search for the same parameters.

read the original abstract

Covering codes in finite Hamming spaces ask for small sets of words whose Hamming balls cover the whole space. This paper presents a Lean 4 formalization of the elementary theory of q-ary covering codes, centered on certificate predicates for upper bounds, lower bounds, and exact covering numbers $K_q(n,r)$. The formalization proves the q-ary Hamming-ball volume formula, the sphere-covering lower bound, elementary exact cases, product and relation rules, and selected small exact certificates. It also demonstrates an end-to-end workflow for checking explicit upper bounds transcribed from van Laarhoven et al. (1989). The accompanying database is proof-carrying: stored bounds have traces that replay to Lean proofs of the corresponding upper- or lower-bound predicates. The contribution is not new record bounds or a reproduction of known tables, but a reusable, auditable foundation for machine-checked covering-code certificates.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. This paper presents a Lean 4 formalization of the elementary theory of q-ary covering codes, centered on certificate predicates for upper bounds, lower bounds, and exact values of K_q(n,r). It includes machine-checked proofs of the q-ary Hamming-ball volume formula, the sphere-covering lower bound, elementary exact cases, product and relation rules, and demonstrates an end-to-end workflow for verifying explicit upper bounds transcribed from van Laarhoven et al. (1989), with a proof-carrying database of bounds whose traces replay to Lean proofs.

Significance. If the formalization is sound, the work supplies a reusable, auditable foundation for machine-checked covering-code certificates. This is valuable because it enables verification of literature bounds without manual checking and provides a platform for extending tables with guaranteed correctness. The explicit use of proof-carrying certificates and the encoding of standard definitions into Lean are strengths that support long-term reliability of covering-code tables.

major comments (2)
  1. [demonstration of the end-to-end workflow for checking explicit upper bounds] The end-to-end workflow for upper-bound certificates (described in the abstract and the demonstration section) relies on manual transcription of codes from van Laarhoven et al. (1989) into Lean terms that inhabit the upper-bound predicate. The manuscript should supply an explicit cross-check (e.g., a table or auxiliary lemma) confirming that the transcribed (q,n,r,code) tuples match the 1989 source; without it, a mismatch would allow the predicate to be inhabited by a term that does not correspond to a genuine covering from the literature.
  2. [formalization overview and abstract] The abstract and formalization overview supply no information on library completeness, the presence of admitted lemmas, or the verification status of the transcribed bounds. Because soundness of the certificate predicates rests on these details, the manuscript should report the number of admitted axioms (if any) and the status of the core definitions relative to the standard mathematical notion of a covering (every vector lies in a Hamming ball of radius r).
minor comments (1)
  1. The notation for the certificate predicates could be clarified with an explicit statement of the predicate definitions (e.g., what fields the upper-bound certificate record contains) to make it easier for readers to confirm they match the intended mathematical notions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive suggestions. Both major comments identify opportunities to strengthen transparency and verifiability; we will incorporate the requested details via minor revisions.

read point-by-point responses

  1. Referee: [demonstration of the end-to-end workflow for checking explicit upper bounds] The end-to-end workflow for upper-bound certificates (described in the abstract and the demonstration section) relies on manual transcription of codes from van Laarhoven et al. (1989) into Lean terms that inhabit the upper-bound predicate. The manuscript should supply an explicit cross-check (e.g., a table or auxiliary lemma) confirming that the transcribed (q,n,r,code) tuples match the 1989 source; without it, a mismatch would allow the predicate to be inhabited by a term that does not correspond to a genuine covering from the literature.

    Authors: We agree that an explicit cross-check is a useful addition. In the revised manuscript we will insert a table in the demonstration section that lists each transcribed (q,n,r,code) tuple together with its precise reference (page and entry) from van Laarhoven et al. (1989). We will also add a short auxiliary Lean lemma that records the correspondence for the examples used, so that any future reader can verify the transcription directly from the source. revision: yes

  2. Referee: [formalization overview and abstract] The abstract and formalization overview supply no information on library completeness, the presence of admitted lemmas, or the verification status of the transcribed bounds. Because soundness of the certificate predicates rests on these details, the manuscript should report the number of admitted axioms (if any) and the status of the core definitions relative to the standard mathematical notion of a covering (every vector lies in a Hamming ball of radius r).

    Authors: We accept the point on transparency. The formalization contains no admitted axioms in the core definitions or main theorems. The covering predicate is defined precisely as the standard mathematical notion: a set C is a covering if every vector in the ambient space lies in some Hamming ball of radius r centered at a codeword of C. We will revise the formalization-overview section to state explicitly that the number of admitted lemmas is zero for the core theory and to confirm the alignment of the predicate with the literature definition. The transcribed bounds inherit their verification status directly from the predicate. revision: yes

Circularity Check

0 steps flagged

No circularity; formalization encodes external definitions and literature bounds directly

full rationale

The paper defines covering-code predicates from standard mathematical notions (Hamming balls, covering), proves volume and bound formulas from those definitions, and checks transcribed upper bounds from an external 1989 reference by different authors. No step reduces a claimed result to a fitted parameter, self-citation chain, or renamed input by construction. The transcription workflow is a manual encoding step whose soundness is external to the formalization itself.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based solely on the abstract, the formalization rests on standard mathematical definitions of Hamming spaces and covering; no free parameters, ad-hoc axioms, or invented entities are described.

axioms (1)
  • standard math Standard definitions of q-ary Hamming space, Hamming distance, and ball volume hold in Lean 4.
    Invoked when proving the volume formula and sphere-covering bound.

pith-pipeline@v0.9.1-grok · 5679 in / 1242 out tokens · 20396 ms · 2026-06-27T14:43:32.757673+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references · 10 canonical work pages · 1 internal anchor

  1. [1]

    Football Pools—A Game for Mathematicians

    H. H¨am¨al¨ainen et al. “Football Pools—A Game for Mathematicians”. In:The American Mathematical Monthly102.7 (1995), pp. 579–588.DOI:10.1080/00029890.1995.12004624

    work page doi:10.1080/00029890.1995.12004624 1995

  2. [2]

    Ternary Covering Codes

    Laurent Habsieger. “Ternary Covering Codes”. In:The Electronic Journal of Combinatorics3.2, R23 (1996).DOI: 10.37236/1281.URL:https://www.combinatorics.org/ojs/index.php/eljc/article/view/v3i2r23

    work page doi:10.37236/1281.url:https://www.combinatorics.org/ojs/index.php/eljc/article/view/v3i2r23 1996

  3. [3]

    Error Detecting and Error Correcting Codes

    Richard W. Hamming. “Error Detecting and Error Correcting Codes”. In:The Bell System Technical Journal29.2 (1950), pp. 147–160.DOI:10.1002/j.1538-7305.1950.tb00463.x

    work page doi:10.1002/j.1538-7305.1950.tb00463.x 1950

  4. [4]

    G´erard Cohen et al.Covering Codes. V ol. 54. North-Holland Mathematical Library. Amsterdam: North-Holland, 1997. 541 pp.ISBN: 978-0-444-82511-7.URL:https://books.google.com/books?id=7KBYOt44sugC

    1997

  5. [5]

    The Lean 4 Theorem Prover and Programming Language

    Leonardo de Moura and Sebastian Ullrich. “The Lean 4 Theorem Prover and Programming Language”. In:Automated Deduction – CADE 28. Ed. by Andr´e Platzer and Geoff Sutcliffe. V ol. 12699. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2021, pp. 625–635.ISBN: 978-3-030-79876-5.DOI: 10.1007/978-3-030-79876- 5_37

    work page doi:10.1007/978-3-030-79876- 2021

  6. [6]

    Florence Jessie MacWilliams and Neil James Alexander Sloane.The Theory of Error-Correcting Codes. V ol. 16. North-Holland Mathematical Library. Amsterdam: North-Holland, 1977. 762 pp.ISBN: 978-0-444-85010-2

    1977

  7. [7]

    van Lint.Introduction to Coding Theory

    Jacobus H. van Lint.Introduction to Coding Theory. Third. V ol. 86. Graduate Texts in Mathematics. Berlin, Heidelberg: Springer, 1999. XIV+234.ISBN: 978-3-540-64133-9.DOI:10.1007/978-3-642-58575-3

    work page doi:10.1007/978-3-642-58575-3 1999

  8. [8]

    New Upper Bounds for the Football Pool Problem for 6, 7, and 8 Matches

    P. J. M. van Laarhoven et al. “New Upper Bounds for the Football Pool Problem for 6, 7, and 8 Matches”. In:Journal of Combinatorial Theory, Series A52.2 (1989), pp. 304–312.DOI:10.1016/0097-3165(89)90036-8

    work page doi:10.1016/0097-3165(89)90036-8 1989

  9. [9]

    Upper bounds for q-ary covering codes

    Patric R. J. ¨Osterg˚ard. “Upper bounds for q-ary covering codes”. In:IEEE Transactions on Information Theory37.3 (1991), pp. 660–664.DOI:10.1109/18.79926

    work page doi:10.1109/18.79926 1991

  10. [10]

    Semidefinite lower bounds for covering codes

    Dion Gijswijt and Sven Polak.Semidefinite Lower Bounds for Covering Codes. 2025.DOI: 10.48550/arXiv.2504. 01932. arXiv:2504.01932 [math.CO].URL:https://arxiv.org/abs/2504.01932

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2504 2025

  11. [11]

    Gerzson K´eri.Tables for Bounds on Covering Codes.URL: https://old.sztaki.hu/˜keri/codes/index.htm (visited on 05/17/2026)

    2026

  12. [12]

    A Library for Formalization of Linear Error-Correcting Codes

    Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. “A Library for Formalization of Linear Error-Correcting Codes”. In:Journal of Automated Reasoning64.6 (2020), pp. 1123–1164.DOI:10.1007/s10817-019-09538-8

    work page doi:10.1007/s10817-019-09538-8 2020

  13. [13]

    2020 , pages =

    The mathlib Community. “The Lean Mathematical Library”. In:Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2020. New York, NY , USA: Association for Computing Machinery, 2020, pp. 367–381.ISBN: 978-1-4503-7097-4.DOI:10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020