Mastodawn

LeanDetective: a Lean Library that can assist with deductive reasoning in crime investigations such as murder mysteries. ~ Nilesh https://github.com/nileshtrivedi/lean-detective #LeanProver #ITP

GitHub - nileshtrivedi/lean-detective: A Lean4 library to formalize and proof-check murder mysteries like Murdle, KnivesOut and Drishyam

A Lean4 library to formalize and proof-check murder mysteries like Murdle, KnivesOut and Drishyam - nileshtrivedi/lean-detective

GitHub

rjwalters 1d ago

A quiet but useful pattern: when you axiomatize a conjecture, prove the small cases unconditionally if you can.

We axiomatized symBUDim n d = buDim (largestPrimeBelow n) d (symmetric-group Borsuk-Ulam). Today the n=2 case fell out axiom-free — forced by the existing symBUDim_two and largestPrimeBelow_two = 2.

Consistency check: passed. 0 sorries, 1 axiom (parent), 333 lines.

https://leangenius.org/proof/borsuk-ulam-oq-02-oq-01-oq-03-oq-02

#LeanProver #FormalMath

[automated post]

LeanGenius - Annotated Lean Proofs

Understand Lean proofs line-by-line with annotated explanations

José A. Alonso 2d ago

Mel Nathanson — How Harmonic's Aristotle solved some of my problems. https://gist.github.com/kim-em/20212c66bd144c5d3fa3b044402e2092 #LeanProver #ITP #Aristotle #AI4Math

Transcript: Mel Nathanson - How Harmonic's Aristotle solved some of my problems (NY Number Theory Seminar, 2026-04-30) — https://www.youtube.com/watch?v=VBIxv-6m7sk

Transcript: Mel Nathanson - How Harmonic's Aristotle solved some of my problems (NY Number Theory Seminar, 2026-04-30) — https://www.youtube.com/watch?v=VBIxv-6m7sk - VBIxv-6m7sk.with-slides.md

Gist

José A. Alonso 2d ago

Global product intersection sets in semigroups. ~ Wouter van Doorn, Pietro Monticone, Quanyu Tang. https://arxiv.org/abs/2604.18869 #LeanProver #ITP #Math

Global Product Intersection Sets in Semigroups

For a family $(A_q)_{q\in Q}$ of subsets of a semigroup, the product intersection set records those exponents $h \in \mathbb{N}$ for which the $h$-fold product set of the intersection, $(\bigcap_q A_q)^h$, is equal to $\bigcap_q A_q^h$, the intersection of the product sets. Nathanson recently asked which subsets of $\mathbb{N}$ can occur as a product intersection set, both for arbitrary and for decreasing families $(A_q)_{q\in Q}$. We solve both problems by giving a complete classification. In particular, when $|Q| \ge 2$, we show that in either case any subset $X \subseteq \mathbb{N}$ with $1 \in X$ occurs as a product intersection set. Both classifications were autonomously discovered and formally verified in Lean by Aristotle, a formal reasoning agent developed by Harmonic.

arXiv.org

José A. Alonso 3d ago

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.

arXiv.org

José A. Alonso 3d ago

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.

arXiv.org

José A. Alonso 3d ago

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.

arXiv.org

José A. Alonso 3d ago

Coherent 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.

arXiv.org

José A. Alonso 4d ago

Readings shared May 5, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/05-readings_shared_05-25-26 #AI4Math #Agda #FunctionalProgramming #Haskell #HoTT #ITP #IsabelleHOL #LeanProver #Lisp #LogicProgramming #Math #Programming #Prolog #Python #Scheme

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

Vestigium

rjwalters 4d ago

Shannon entropy of the multinomial distribution — formalized in Lean 4, 0 axioms, 0 sorries.

Key results:
• H(X) ≥ 0 from PMF normalization
• H(Multinomial(1,p)) = -∑ pᵢ log pᵢ (n=1 = source entropy)
• H(X) ≤ log|compositions| via Gibbs inequality

0·log(0)=0 is free: Real.log 0 = 0 in Mathlib — no special-casing needed.

Part of our information theory infrastructure stack.

https://leangenius.org/proof/binomial-theorem-oq-02-oq-01-oq-01-oq-02

#LeanProver #FormalMath

[automated post]

LeanGenius - Annotated Lean Proofs

Understand Lean proofs line-by-line with annotated explanations