Email Gateway (Jul 14 2026 at 09:17): Email Gateway (Jul 14 2026 at 09:17):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Chevalley-Warning and Equality-Saturation-Checker
Dear all,
I’m happy to announce two new AFP entries by
Arthur Freitas Ramos,
David Barros Hulak, and
Ruy Jose Guerra Barretto de Queiroz.
The Chevalley-Warning Theorem
This development formalizes the Chevalley--Warning theorem for finite fields: if
finitely many multivariate polynomials over a finite field have total degree sum
strictly smaller than the number of variables, then the number of their common
zeros is divisible by the characteristic. Polynomials are represented by finite
sparse term lists, and the proof follows the standard finite-field power-sum
argument. AI assistance was used for proof engineering. The final definitions,
statements, and proofs are checked by Isabelle.
https://isa-afp.org/entries/Chevalley_Warning.html
and
Checking Equality-Saturation Merge and Extraction Certificates
Equality-saturation engines maintain equalities in an e-graph and later extract
a representative from an e-class. This entry verifies an executable checker for
the corresponding engine boundary. It directly parses the flat annotated
S-expression format returned by egg 0.11.0’s explanation API; flat explanations
may apply numbered rewrite rules at positions or reuse equalities from earlier
checked e-class merges. For extraction, a finite e-graph is represented as a
topologically ordered e-class DAG. An executable bottom-up dynamic program
selects a representative, and a formal proof establishes minimum additive cost
over every term represented by the designated class. Class-aligned equality
certificates additionally prove the selected term equivalent to the canonical
class term. The development reuses the term, substitution, position, context,
and rewriting infrastructure of the AFP entries First-Order Terms and
First-Order Rewriting. Its soundness statements target their existing conversion
relation. It does not introduce another first-order term datatype, rewrite
relation, generic equational proof calculus, or proof of Birkhoff’s theorem.
Those generic equational results and a checker for equality proofs already exist
in IsaFoR/CeTA. The new material is the chronological e-graph merge discipline,
positional reuse of recorded merges, certified e-class DAG semantics, and
globally optimal dynamic-programming extraction.
https://isa-afp.org/entries/Equality_Saturation_Checker.html
Enjoy,
René
Last updated: Jul 22 2026 at 14:00 UTC