José A. Alonso
#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.
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.
A Lean-certified proof of K₈(4, 2) = 23. ~ Andreas Florath. https://arxiv.org/abs/2606.16688v1 #LeanProver #ITP #Math
A Lean-Certified Proof of $K_8(4, 2) = 23$
We prove the exact octonary covering-code value $K_8(4, 2) = 23$ in Lean 4. The upper bound is given by an explicit 23-word radius-two code in $(Fin\:8)^4$ , checked over all $8^4$ ambient words. The lower bound excludes covers with at most 22 words. A fiber-counting and missing-pair argument first rules out covers with at most 21 words. In the remaining 22-word case, the proof reduces a hypothetical cover to six missing-pair graphs coming from the coordinate-pair projections. Fiber-counting arguments constrain these graphs, and two Lean-checked Linear RAT (LRAT) refutations of stored conjunctive-normal-form (CNF) instances force a common 3 + 3 + 2 block structure. This structure is incompatible with a 22-word cover: the two three-symbol components already force 18 codewords, while the remaining two-symbol component would require a binary strength-two array of length four with at most four rows, which is impossible. The result is packaged as a proof-carrying Lean artifact: the explicit upper bound, structural lower bound, CNF instances, and LRAT refutations are checked inside Lean, with no external SAT solver used during proof replay.
EconCSLib: A Lean library for computational economics and AI-Assisted research. ~ Xiaohui Bei, Jiajun Ma, Zhan Jing, Hongfei Fu, Zhihao Gavin Tang. https://arxiv.org/abs/2606.16144v1 #LeanProver #ITP
EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research
Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative library for Lean, illustrates the potential of this approach. Recent progress in AI-assisted programming and theorem proving is also making large-scale formalization more practical. This paper presents EconCSLib, an early Lean 4 library for computational economics, as both infrastructure and a case study for AI-assisted formalization. The library aims to provide reusable definitions and theorems for game theory, mechanism design, social choice, and related areas. Beyond verified proofs of existing results, the library also aims to host machine-checked open problems and formalization of modern research papers. We discuss the design principles behind the library, the lessons learned from its development, and future directions for AI-assisted formalization in computational economics.
Formalizing chip-firing and Riemann-Roch for graphs in Lean 4. ~ Dhyey Dharmendrakumar Mavani, Nathan Pflueger. https://arxiv.org/abs/2606.16679v1 #LeanProver #ITP
Formalizing chip-firing and Riemann--Roch for graphs in Lean 4
The Riemann--Roch theorem for graphs, due to Baker and Norine, is a foundational result establishing a powerful analogy between finite graphs and algebraic curves. We describe a complete formal proof of this theorem implemented in the Lean 4 theorem prover. Our formalization includes the existence and uniqueness of q-reduced divisors, a modified form of Dhar's burning algorithm, the bijection between acyclic orientations with unique source and maximal superstable configurations, and Clifford's theorem. We also include several challenges for future formalization.
LeanLean 4.31.0 is released.
This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.
Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.
Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.31.0/
