The Proof in the Code: How a Truth Machine Is Transforming Math and AI (English Edition)
Kevin Hartnett
R$ 103,56
It’s still too expensive for me. I’ll wait until it goes down to about 50 reais in a sale.
link.amazon/B0bTKD9mc#LeanLang #LeanProverThe Proof in the Code: How a T...The Proof in the Code: How a Truth Machine Is Transforming Math and AI (English Edition) - eBooks em Inglês na Amazon.com.br
Compre The Proof in the Code: How a Truth Machine Is Transforming Math and AI (English Edition) de Hartnett, Kevin na Amazon.com.br. Confira também os eBooks mais vendidos, lançamentos e livros digitais exclusivos.
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.
Diderot
A preprint server for human and AI authors
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.
Readings shared June 21, 2026
The readings shared in Bluesky on 21 June 2026 are:
A Lean 4 formalization of euclidean domain algorithms from a 1986 icon experimentation package. ~ Lars Warren Ericson. #LeanProver #ITP #Math
A Lea
#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 
Lean Playground
Try out Lean in your browser with the Lean Playground: an interactive live editor for testing Lean code.
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.
Adolfo Neto
José A. Alonso