Bennett's conjecture in Lean 4: Counter-models for the PSR-reducibility of Spinoza's propositions V and XIV. ~ Yuki Nakamura.
https://arxiv.org/abs/2605.02331v1 #LeanProver #ITP
Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV
In A Study of Spinoza's Ethics (1984, §17), Jonathan Bennett argues that the demonstration of Proposition V of Spinoza's Ethica contains identifiable invalid moves and that, even granted those moves, "cannot yield more than the conclusion that two substances could not have all their attributes in common" -- while Spinoza concludes that they cannot share any. Bennett doubts that any valid reconstruction is available from Spinoza's stated resources without importing further commitments. Michael Della Rocca (Spinoza, 2008, ch. 2) responds that the proposition can be derived if the Principle of Sufficient Reason (PSR) is committed substantively. The debate has remained at the level of prose argument for forty years. This paper provides the first machine-checked evidence in the debate. We formalise Ethica Pars I in Lean 4, encoding Bennett's reading of Spinoza's stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class. The derivation attempt yields a partial result -- substances sharing all attributes are identical -- but cannot reach the full "sharing-any-attribute -> identity" content of Proposition V, mechanically tracking Bennett's own all-attributes ceiling. A four-element counter-model satisfying both axiom sets while falsifying Proposition V's content establishes the irreducibility against this specific augmentation. A second counter-model establishes the analogous result for axiom A15, a load-bearing universality clause for Spinoza's Proposition XIV. Bennett's diagnosis receives its first kernel-level confirmation against the Della-Rocca PSR-substance reconstruction; stronger PSR variants remain open as future mechanical projects.
Certified qualitative analysis of the SIR ODE and reusable scalar lemmas in Isabelle/HOL. ~ David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz.
https://arxiv.org/abs/2605.02474v1 #IsabelleHOL #ITP #Math
Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
We present a mechanically checked Isabelle/HOL bridge from the Picard-Lindelof flow infrastructure in the Archive of Formal Proofs (AFP) to selected qualitative facts for the mass-action, closed-population SIR epidemic ODE. The epidemiological facts are classical; the contribution is reusable theorem infrastructure connecting the AFP local-flow construction to global forward existence, uniqueness, forward invariance of the nonnegative orthant, conservation, monotonicity, the Kermack-McKendrick conserved phase-plane relation, compartment bounds, and threshold-ratio conditions for infectious growth and monotonicity.
The proof first establishes sign and conservation facts for local AFP flow segments, then uses the conserved nonnegative simplex as the compactness witness for extending the flow to all forward times. The finite-interval qualitative facts are then transferred to the unique AFP forward flow on arbitrary intervals [0,b] with b>0, so the results apply to the constructed Isabelle/AFP SIR solution rather than to an assumed trajectory.
The reusable layer provides homogeneous-linear scalar compartment lemmas for equations X'(t)=f(t)X(t), derivative-sign monotonicity, three-compartment conservation, and an SIR transfer bridge to the AFP flow infrastructure. We do not formalize stability, final-size, or asymptotic theory. The accompanying Isabelle artifact builds with Isabelle 2024 and AFP 2024 and contains no sorry or oops proof placeholders.
A shallow embedding of Datalog in Lean. ~ Ramy Shahin.
https://arxiv.org/abs/2605.02113v1 #LeanProver #ITP
A Shallow Embedding of Datalog in Lean
Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of Inductive Constructions (CIC). Datalog is more constrained and less expressive than Lean but has a long history of established deduction algorithms. Writing definitions and queries in the Datalog fragment of Lean would be more succinct and understandable than writing them in Lean itself.
This paper outlines the design and implementation of a shallow embedding of Datalog as a Domain Specific Language (DSL) on top of Lean. Bidirectional interoperability between the Datalog DSL and Lean is a primary goal of this design. In addition to rules and facts, backward chaining queries are automatically translated into theorems with tactic-based proofs. The paper also includes three simple examples of how the DSL can be used.
Stokes' theorem for smooth singular cubes in Lean 4: True pullback, bridges to mathlib4, and chain-level d^2=0. ~ David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz.
https://arxiv.org/abs/2605.01028v1 #LeanProver #ITP #Math
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
We present a sorry-free Lean 4/mathlib4 formalization of Stokes' theorem for smooth singular cubes in arbitrary dimension, using true differential-form pullback via the Frechet derivative. The development also includes a bridge to mathlib4's abstract extDeriv, chain-level Stokes extended by Z-linearity, d^2=0 for singular cubical chains, box Stokes for axis-aligned cubes, dimensional specializations, and a structured comparison with Harrison's HOL Light formalization.
Formal verification of Pohlig-Hellman algorithm for computing discrete logarithms with Coq. ~ Jeremiah Daniel A. Regalario et als.
https://www.atlantis-press.com/article/126023793.pdf #CoqProver #ITPCoherent rollout oracles for finite-horizon sequential decision problems. ~ Nishant Shukla.
https://arxiv.org/abs/2604.25962v1 #LeanProver #ITP
Coherent Rollout Oracles for Finite-Horizon Sequential Decision Problems
Coherent quantum rollout for sequential decision problems requires a unitary simulator: randomness must live in explicit quantum registers, and basis-state selectors must be mapped to actions reversibly. With branch-dependent valid actions, this mapping is totalized coherent rank-select over an entangled $N$-bit validity mask: return the position of the $r$-th valid bit, or a sentinel if $r$ is out of range.
We give the first reversible-circuit complexity analysis of this primitive. For selector width $w = \lceil \log_2(N+1) \rceil$, rank-select admits an $O(Nw)$-gate low-ancilla bounded-span scan, proved gate-optimal in its model, and an $O(N\log w)$-gate low-ancilla blocked construction when long-range gates are available; across all bounded-fan-in layouts, the unconditional gate lower bound is $Ω(N)$. Composing rank-select with reversible transition and predicate-evaluation circuits gives an explicit polynomial-size coherent rollout oracle for finite-horizon planning problems satisfying these primitive assumptions.
The resulting oracle satisfies the access model of the best-arm pipeline of Wang et al., yielding $\widetilde{O}(\sqrt{k}/\varepsilon)$ coherent oracle calls against the standard classical $Ω(k/\varepsilon^2)$ arm-pull lower bound. We give a bounded-influence lifting theorem that extends this lower-bound construction from a base configuration to an exponential family of configurations. We instantiate the construction on SIR epidemic intervention, with a stochastic placement-game sanity check, and machine-check the main results in Lean 4. Code and proofs: https://github.com/BinRoot/b01t/tree/main/demos/rollout.
Between Qed and truth (The permanent axiom trust boundary in machine-verified mathematics). ~ Ryan Christopher Fields.
https://philarchive.org/archive/FIEBQA #CoqProver #ITP #Math
Readings shared May 4, 2026
The readings shared in Bluesky on 4 May 2026 are:
Compfiles: Catalog of math problems formalized in Lean. ~ David Renshaw et als. #LeanProver #ITP #Math
Primitive pythagorean triples in lean and redu
Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon.
https://arxiv.org/abs/2405.03264v1 #Agda #ITP #HoTT
Delooping generated groups in homotopy type theory
Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces (up to continuous deformation) and proofs as homotopy invariant constructions. In this context, the loop spaces of types with a distinguished element (more precisely, pointed connected groupoids), provide a natural representation of groups, what we call here internal groups. The construction which internalizes a given group is called delooping, because it is a formal inverse to the loop space operator. As we recall in the article, this delooping operation has a concrete definition for any group G given by the type of G-torsors. Those are particular sets together with an action of G, which means that they come equipped with an endomorphism for every element of G. We show that, when a generating set is known for the group, we can construct a smaller representation of the type of G-torsors, using the fact that we only need automorphisms for the elements of the generating set. We thus obtain a concise definition of (internal) groups in homotopy type theory, which can be useful to define deloopings without resorting to higher inductive types, or to perform computations on those. We also investigate an abstract construction for the Cayley group of a generated group. Most of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.
Nagata factoriality (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz.
https://www.isa-afp.org/entries/Nagata-Factoriality.html #IsabelleHOL #ITP #Math
Nagata Factoriality
Nagata Factoriality in the Archive of Formal Proofs
José A. Alonso