José A. AlonsoAlon’s Combinatorial Nullstellensatz (in Isabelle/HOL). ~ Arthur Freitas Ramos, Ruy Jose Guerra Barretto de Queiroz, David Barros Hulak. https://isa-afp.org/entries/Combinatorial_Nullstellensatz.html #IsabelleHOL #ITP #Math
An Arrow-theoretic impossibility theorem for the ordinal MVP aggregation problem. ~ Arjun Trivedi. https://www.researchgate.net/profile/Arjun-Trivedi-5/publication/404396065_An_Arrow-Theoretic_Impossibility_Theorem_for_the_Ordinal_MVP_Aggregation_Problem #LeanProver #ITP
Formalizing the prime-field Singer construction and Sidon set infrastructure in Lean 4. ~ David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz. https://arxiv.org/abs/2605.03274v1 #LeanProver #ITP #Math
Formalizing the Prime-Field Singer Construction and Sidon Set Infrastructure in Lean 4
Erdős Problem 30 asks for sharp asymptotics of the Sidon extremal function $h(N)$, and Singer's construction is the classical source of lower-bound examples matching the main term. We present a Lean 4 formalization of Singer's Sidon set construction for prime fields, together with reusable Sidon-set infrastructure for additive combinatorics. For every prime $p$, we prove the existence of a Sidon set modulo $p^2+p+1$ of cardinality $p+1$. The proof proceeds through a non-trivial algebraic chain: construction of the Galois field $\mathrm{GF}(p^3)$, analysis of the trace kernel as a 2-dimensional subspace, a geometric argument via subspace intersections establishing the multiplicative Sidon property in the quotient group, and a combinatorial bridge transferring this to modular integer arithmetic. Around this central result, we develop a reusable Sidon set library for additive combinatorics. It comprises interval Sidon sets, modular Sidon sets, the extremal function $h(N)$, Lindstrom's cross-difference inequality, a Johnson-route shift-incidence upper bound of the form $h(N) \leq \sqrt{N} + N^{1/4} + O(1)$, exact representation-function identities, and unconditional two-sided $h(N)=Θ(\sqrt{N})$ bounds with exact floor-rounded finite statements for $N \geq 5$. We further formalize a conditional reduction: subpolynomial prime gaps together with a full subpolynomial upper-error hypothesis for $h(N)$ imply the Erdős Problem 30 estimate $h(N)=\sqrt{N}+O_\varepsilon(N^\varepsilon)$ for every $\varepsilon>0$. The core Singer/Sidon and transfer development comprises 6,382 lines of Lean 4 with zero active uses of sorry. We describe the mathematical lessons learned, focusing on how formalization clarifies the precise scope of classical arguments and forces explicit treatment of the algebraic-combinatorial interface.
Generalization of Church-Rosser strategies for confluent abstract rewriting systems of the smallest uncountable cardinality. ~ Ievgen Ivanov. https://wrla2026.github.io/preproceedings/preproceedings.pdf#page=7 #IsabelleHOL #ITP
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
Nash equilibria for finite games in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Nash_Equilibrium.html #IsabelleHOL #ITP
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
A General Formalised Framework for Reasoning About Display Calculi - Studia Logica
We encode Belnap’s basic theory of display calculi in the proof assistant Coq/Rocq version 8.18.0 and formalise the proof that Belnap’s conditions C2–C8 imply the cut-elimination theorem. Our framework allows us to formally prove meta-theoretic results such as Hilbert-completeness and derivability of explicit rules, such as cut, but also others if required. What makes our formalisation powerful is that it works entirely with an abstraction that can be instantiated to many possible logics and display calculi, although we make no attempt to precisely characterise the logics that can be properly displayed in our formalisation. For this reason, our work can be seen as a formalisation of a display calculus framework and a cut-elimination theorem for a wide range of display calculi. As examples, we apply our work to classical propositional logic (CPL), tense logic (Kt), and non-commutative non-associative Lambek calculus to obtain complete display calculi as well as formally proved cut-elimination theorems, but we believe our formalisation to be also applicable to many others. We also encoded a proof of the decidability of CPL that relies only on the structure of proofs within an additive display calculus for CPL. To our knowledge, our work is the first formalisation of a decidability result in display calculus. Moreover, all of our formal proofs are constructive as they never require the addition of the law of excluded middle in Coq’s environment (which is constructive by default), which means we were also able to extract computer programs from our proof of cut-elimination able to convert CPL/Kt/Lambek derivation trees into cut-free ones. As formal proofs are known to be significantly longer to write than usual pen-and-paper proofs, our work led to the development of a multitude of files of Coq code comprising more than 15,000 lines.
The Banach–Tarski paradox in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Banach_Tarski.html #IsabelleHOL #ITP #Math
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