José A. AlonsoFormalization of template formulas in the modal μ-calculus in Isabelle/HOL. ~ Lise Arendsen. https://pure.tue.nl/ws/portalfiles/portal/390531427/Arendsen_L.pdf #IsabelleHOL #ITP #Logic
Readings shared June 22, 2026. https://jaalonso.github.io/vestigium/posts/2026/06/22-readings_shared_06-22-26 #AI4Math #Agda #ChatGPT #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog
#RetoLean4: Propuesta del reto 7 (Demostrar que la composición de funciones inyectivas es inyectiva). https://t.me/Retos_Matematicos/109557/140783 #LeanProver #ITP #Math
J.A. Alonso in Retos Matemáticos
El reto de esta semana consiste en demostrar, con Lean 4, que la composición de funciones inyectivas es inyectiva. Para ello, completar la siguiente teoría de Lean 4: import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by sorry El enunciado se encuentra en Lean 4 Web. Las soluciones pueden publicarse hasta el domingo 28 de junio de 2026. #RetoLean4 #14Jun26
#RetoLean4: Soluciones del reto 6 (Demostrar el teorema del emparedado: Si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L). https://live.lean-lang.org/#url=https://github.com/jaalonso/Retos/blob/main/src/Reto_6.lean #LeanProver #ITP #Math
Finishing Oltean's completeness proof in Lean 4 for hybrid logic L(∀). ~ Lars Warren Ericson. https://arxiv.org/abs/2606.19761 #LeanProver #ITP #Logic
Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\forall)$
We present a machine-checked completeness theorem, in Lean 4, for the hybrid logic $L(\forall)$: propositional modal logic with nominals, the satisfaction-style binder $\forall$, and the box modality. (Machine-checked completeness for basic hybrid logic, without binders, was pioneered by Asta Halkjær From in Isabelle/HOL.) We build on Alex Oltean's 2023 Lean 4 formalization, which mechanized the syntax, semantics, Hilbert-style proof system, and soundness following Blackburn's Hybrid Completeness (1998), but left completeness unfinished. Finishing it requires manufacturing fresh names at two structurally different points, and our central finding is that they call for two different tools. (1) The root witnessed maximal consistent set, built by an extended Lindenbaum construction, needs at each step a nominal fresh for the whole set; the right tool is structural freshness: extend the language so an infinite supply of nominals is reserved by construction. We survey the design space (Oltean's odd/even encoding inside $\mathbb{N}$, the disjoint-sum $N \oplus \mathbb{N}$ parameterization suggested by Bud Mishra, and From's synthetic-completeness frameworks) and explain the encoding we adopt. (2) The witnessed $\Diamond$-successor of a maximal consistent set cannot be obtained this way: its canonical box-reduct provably mentions every nominal, so no reserved name is fresh. Here the right tool is one Oltean chose but left incomplete: an existence-lemma Henkin construction drawing each witness from the predecessor's witnessedness through a fresh state variable; we complete it with a data-carrying witness accumulator and a compactness argument. The theorem $Γ\models φ\to Γ\vdash φ$ is fully formalized: the development is sorry-free, and #print axioms reports only propext, Classical.choice, and Quot.sound. We port the development to Lean v4.30.0 / mathlib v4.30.0.
Prismriver: Formalization of music theory and algorithmic composition in Lean 4. ~ Leni Aniva, Claire Wang. https://arxiv.org/abs/2606.19936 #LeanProver #ITP
Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4
Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structure which can be verified and expressioned in the precise language of a proof assistant. In this paper, we present Prismriver, a formalization of music theory in Lean 4. By formalizing music theory in Lean 4, we open the door to verifiable algorithmic composition and accompaniment generation. We also enable the analysis of monadic analysis of structures in music.
A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness. ~ Karen Sargsyan. https://arxiv.org/abs/2606.20351 #Agda #ITP
A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness
The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $Σ$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and Pearl's d-separation theorem (soundness) on arbitrary $n$-vertex finite directed acyclic graphs (DAGs) in both interventional and Bayesian forms. The probability monad is also verified as a Markov category; the abstract interface discharges at $Q$.
Formalizing extended complex numbers, Mobius transformations, and cross ratio in Lean 4. ~ Fubin Yan, Kenneth W. Shum. https://arxiv.org/abs/2606.20358 #LeanProver #ITP #Math
Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4
The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by Möbius transformations, with the cross ratio serving as a central invariant. We present a formalization of these concepts in the Lean4 theorem prover. The extended complex plane is represented using Mathlib's Option type over $\mathbb{C}$, where the additional element represents the point at infinity. On this foundation, we define Möbius transformations, their action on the extended complex plane, and the cross ratio. We formalize several basic properties of Möbius transformations, including their group structure, and identify them with a projective general linear group. We also prove the uniqueness of a Möbius transformation mapping any three distinct points to any other three distinct points, and the invariance of the cross ratio. All proofs are machine-checked in Lean 4. The complete development comprises approximately 6,000 lines of Lean code, including about 40 definitions and 150 lemmas and theorems. This work provides a verified foundation for future formalizations of conformal geometry, hyperbolic models, modular forms, and applications in mathematical physics.
The Dottie number (in Isabelle/HOL). ~ Lawrence C. Paulson. https://isa-afp.org/entries/Dottie_Number.html #IsabelleHOL #ITP #Math
A formalization of the exponential blowup in the transformations between CNF and DNF (in Isabelle/HOL). ~ Leon Raffael Schulz, Martin Desharnais-Schäfer, Jan Johannsen. https://isa-afp.org/entries/CNF_DNF_Exp_Blowup.html #IsabelleHOL #ITP
