José A. AlonsoPerron's formula (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Perrons_Formula.html #IsabelleHOL #ITP #Math
Formalizing a many-sorted hybrid polyadic modal logic in Lean. ~ Andrei-Alexandru Oltean, Bogdan Macovei, Ioana Leuştean. https://arxiv.org/abs/2606.27041 #LeanProver #ITP #Logic
Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification and dynamic logics, and is designed to serve as a uniform axiomatic foundation for specifying and verifying programming languages and security protocols. We expose a DSL for users to define languages and protocols as many-sorted signatures, specify the relevant domain-specific axioms, and reason about program executions or protocol runs. We provide a machine-checked proof of its soundness theorem and showcase the framework's versatility through several applications: an imperative programming language for code verification, the BAN logic for security protocols, and the modal system S5. We have designed our formalization to be intrinsically sorted, that is, well-sorted formulas in the base language are well-typed terms in Lean. Thanks to intrinsic sorting, all domain specific applications can be easily embedded in our framework via the DSL, at no additional syntactic overhead required for the user to prove. All code presented in this paper is openly accessible in the following repository: https://github.com/alexoltean61/msphml-lean
AXLE: A cloud infrastructure for Lean 4 theorem proving utilities. ~ Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, Jannis Limperg. https://arxiv.org/abs/2606.26442v1 #LeanProver #ITP #AI4Math
AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
We present AXLE (Axiom Lean Engine), a cloud service for Lean 4 proof manipulation, extraction, and verification. Recent progress in AI for mathematics -- reinforcement learning pipelines, agentic proving workflows, dataset curation -- demands Lean 4 tooling that scales to millions of requests while remaining correct and robust; existing infrastructure offers parallel compilation but not scalable proof verification, higher-level proof manipulation, multi-version support, or per-request isolation at the throughput modern AI workflows require. AXLE provides 14 Lean 4 metaprogramming tools spanning strict proof verification, declaration metadata extraction, semantic source manipulation, deterministic proof repair and simplification, and lemma extraction. The service runs as a multi-tenant cloud deployment with per-request isolation and concurrent support for multiple Lean 4 and Mathlib versions, accessible via a Python SDK, command-line interface, web UI, MCP server, and raw HTTP API. AXLE is publicly available and free to use at https://axle.axiommath.ai and via the axiom-axle PyPI package, with no local Lean 4 installation required. It has served over 500 million requests to date and is the underlying infrastructure for Axiom Math's proving efforts, including its 12/12 score on the 2025 Putnam competition.
A weighted Turán sieve for twin primes via the Krafft geometry. ~ Fernando Portela. https://projectdiderot.com/papers/3bcc794d-824c-40ee-9cd7-e84d5d86cd63 #LeanProver #ITP #Math
Discovering new theorems via LLMs with in-context proof learning in Lean. ~ Kazumi Kasaura, Naoto Onda, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, Sho Sonoda. https://arxiv.org/abs/2509.14274 #AI4Math #LeanProver #ITP
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called Conjecturing-Proving Loop (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4. A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning. We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously. Moreover, our experiments show that reusing the LLM's own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.
Formalization of line search methods by Lean. ~ Yiyang Zhang, Kenneth W. Shum. https://arxiv.org/abs/2606.25412 #LeanProver #ITP #Math
Formalization of Line Search Methods by Lean
This paper presents a formalization of line search methods in the Lean 4 theorem prover. Our goal is to advance machine verification of nonlinear optimization theory by translating standard textbook definitions and convergence arguments into rigorous Lean code. We formalize fundamental notions related to gradient descent and descent directions, adaptive step-size selection via backtracking line search, and several classical line search criteria, including the Armijo, Goldstein, and Wolfe conditions, as well as nonmonotone variants. We further formalize a key convergence result, namely the Zoutendijk theorem, which plays a central role in the global convergence analysis of gradient-based iterative methods. By providing machine-checkable definitions and proofs for line search theory, this work complements existing formalizations of first-order optimization methods and establishes a foundation for the verified development of more advanced algorithms in nonlinear programming.
Formalization 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
#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
