Email Gateway (Oct 26 2026 at 10:35): Email Gateway (Oct 26 2026 at 10:35):From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Following the Isabelle release, the AFP is now available for Isabelle2026 from
https://isa-afp.org
There are now more than 5.51 million lines of Isabelle proof in 1042 entries by 614
authors.
Seven new entries have become available from the home page that were previously only
available in the development version:
Modular Forms
by Manuel Eberl, Anthony Bordg, Lawrence C. Paulson and Wenda Li
This entry provides the definition and proofs of basic properties of modular forms and
modular functions. These are holomorphic or meromorphic functions in the complex upper
half plane that satisfy certain symmetries with respect to the modular group SL_2(Z) or a
subgroup thereof. They are a cornerstone of modern number theory and an essential
ingredient in the proof of Fermat's Last Theorem.
Most of the work focuses on level 1 modular forms/functions (i.e. the full modular group
rather than a proper subgroup). Some notable results include:
The valence formula for level 1 meromorphic forms, giving the number of zeros and poles
(including both the special cases of modular forms and modular functions).
Basic level 1 modular forms such as Eisenstein series E_k and the modular discriminant
Delta.
The Ramanujan tau function and the identity Delta = (2 pi)^12 eta^24 relating the
modular discriminant to the Dedekind eta function.
Properties of Klein's J invariant, including bijectivity, non-conformality, covering
properties, and that the level 1 modular functions are exactly the rational functions of
J.
The graded ring structure of the space of modular forms M_k, including its dimension and
explicit bases in terms of E_4, E_6, and Delta.
Zagier's theory of level 1 quasimodular forms, including the structure theorem in terms
of E_2, E_4, and E_6.
The Serre derivative operator.
A number of applications are also provided:
Ramanujan-type identities for the divisor sigma functions (using the Serre derivative
and the structure theorem for M_k), e.g. 20 sigma_3(n) = (24 n - 4) sigma_1(n) + 48
sum_{i=1}^{n-1} sigma_1(i) sigma_1(n-i)
The Eisenstein inversion theorem, relating elliptic curves to lattices (using the
properties of Klein's J invariant).
A short proof of Picard's Little Theorem using the fact that J is a covering map.
The proofs and definitions mostly follow Apostol's "Modular Functions and Dirichlet Series
in Number Theory".
https://www.isa-afp.org/entries/Modular_Forms.html
Countable Infinite Version of Dilworth's Theorem
by Fabián Fernando Serran Suárez, Thaynara Arielly de Lima and Mauricio Ayala-Rincón
Dilworth's Theorem states that in any finite partially ordered set, the size of a largest
antichain equals the minimum number of chains needed to cover the set. We report a
complete, machine-checked formalization of Dilworth's Theorem and of its extension to
countable partial orders of finite width in the Isabelle/HOL proof assistant. The finite
case is obtained from a formalization of the Koenig-Egervary Theorem on the construction
of a bipartite digraph associated with the partial order. For finite width, the countable
case reduces to the finite one through a compactness argument: the incomparability graph
of the partial order is shown to be k-colorable whenever every finite induced subgraph is,
by appealing to a formalization of the De Bruijn-Erdos coloring theorem, itself a
consequence of the compactness of propositional logic. We describe the formal statements,
the central definitions, and the two top-level theorems together with their Isar proofs.
This development continues the previous work on the mechanization of combinatorial
theorems over countable infinite structures derived from propositional compactness.
https://www.isa-afp.org/entries/Dilworth_Countable.html
The Steiner Deltoid as the Tangent Envelope of Wallace--Simson Lines in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
We formalize the classical Steiner deltoid construction in Isabelle/HOL using only the
published Archive of Formal Proofs entry for the Wallace--Simson line. In
unit-circumcircle coordinates, the deltoid has an explicit complex parametrisation. We
prove its derivative formula, characterize the stationary parameters by m^3 = abc, and
certify them as ordinary cusps using the second and third derivatives. We then prove an
equality of sets between the appropriate Wallace--Simson line and the tangent line, for
every parameter, including the cusp cases. The development uses complex coordinates and
handles a vertex parameter by cycling to the alternate pair of feet.
https://www.isa-afp.org/entries/Steiner_Deltoid.html
IMP_concur - A Semantics for a Language with Concurrency based on HOL-CSP
by Burkhart Wolff
The theory IMPconcur provides a programming-language aspect to HOL-CSP. It extends the
well-known imperative language IMP originated by Glenn Winskell by concurrent primitives
like lock and unlock for semaphores, thread-local and system global program variables and
the notion of threads that run in interleaving semantics. Threads can be parametric and
used to construct concurrent process architectures.
Representing IMPconcur semantics can be done by a straight-forward translation into
HOL-CSP; thus, IMPconcur can be seen as a thin layer on top of the theory of Concurrent
Sequential Processes of Hoare, Brookes and Roscoe in its formalization HOL-CSP in
Isabelle/HOL.
Notwithstanding its simplicity, IMPconcur covers many aspects of concurrency,
non-termination, divergence, synchronization, states and race-conditions. We believe that
IMPconcur may be relevant for readers interested in the link between programming languages
and process algebras. Resulting new ways to concurrent program verification are an
interesting target for future study. We also present a language extension for dynamic
reconfigurations of thread- architectures.
This session is complemented by a syntactic frontend for IMPconcur, called CIL, which has
been authored by Mathilde Needham and Zineddine Kermadj on their internship project in
summer 2025.
https://www.isa-afp.org/entries/IMP_concur.html
HOL in HOL over a set-theoretic universe: consistency of NK with infinity and choice
by Christoph Benzmüller and Daniel Kirchner
This companion to the entry "A deep embedding of HOL in HOL" certifies the
natural-deduction calculus NK of that entry consistent with a genuine Dedekind-style axiom
of infinity — an injective, non-surjective self-map of the individuals — and, because its
standard model has full function spaces, with the relational axiom of choice as well. Such
an axiom has no finite models, so the compactness argument of the main entry — which lifts
arbitrarily large finite models to an infinity scheme — does not apply: a genuinely
infinite model is required. We construct one over Paulson's ZFC_in_HOL: the individuals
are interpreted as the finite ordinals ω, with full function spaces at every type,
yielding a standard Σ-model of NK over the set-theoretic universe V. As this meta-theory
is stronger and non-conservative, the guarantee is relative consistency at ZF strength;
the machine-checked formalisation lives in Isabelle/HOL with Paulson's ZFC_in_HOL (the ZF
reading is metatheoretic, made precise in the introduction). Because NK already provides
extensionality and typed description (after Andrews), this certifies the consistency of
full classical higher-order logic in Church's sense, choice included as a separate
relational scheme.
The infinity axiom and the weaker infinity scheme of the main entry turn out to be
logically independent. That the scheme does not entail the axiom is shown in the main
entry; the present entry settles the other direction, since the axiom does not entail any
of the scheme's individual inequalities: its set-theoretic model interprets all individual
constants alike, so those inequalities fail while the axiom holds. Neither sentence, then,
implies the other.
The plain-HOL results — soundness, Henkin completeness, and finite-model consistency,
including the compactness route to the infinity scheme — are proved in the main entry and
imported here unchanged. What the present entry adds is the set-theoretic route to axioms
that plain HOL alone cannot model.
This contribution is part of the LogiKEy project.
https://www.isa-afp.org/entries/HOL_in_HOL_Deep_Infinity_ZFC.html
Steiner's Line Theorem in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
We formalize Steiner's line theorem in Isabelle/HOL. For a nondegenerate triangle and a
point on its circumcircle, the reflections of that point in the three sidelines are
collinear, and the resulting line passes through the orthocenter. The development uses
complex coordinates and imports the published Wallace–Simson line entry for its
perpendicular-foot and collinearity infrastructure.
https://www.isa-afp.org/entries/Steiner_Line_Theorem.html
Rely-Guarantee Specification of a Concurrent Garbage Collector
by Roger C. Su and Nisansala P. Yatapanage
We specify a model of the Ben-Ari concurrent garbage collector in the rely-guarantee
paradigm, and verify its correctness. The aim is to show that the algorithm can be
verified with rely-guarantee without the use of shared auxiliary variables. The approach
is to reason that a certain property is maintained by one component for all instances of a
variable, and then instantiate it to the particular instance required by the rely of the
other component.
https://www.isa-afp.org/entries/RG_VDM_Garbage_Collector.html
Enjoy!
Gerwin
Last updated: Oct 29 2026 at 04:52 UTC