José A. AlonsoReadings shared May 29, 2026. https://jaalonso.github.io/vestigium/posts/2026/05/30-readings_shared_05-29-26 #AI4Math #CoqProver #ITP #IsabelleHOL #LeanProver #Logic #Math
The classical Seifert–van Kampen theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos , David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Seifert-Van-Kampen.html #IsabelleHOL #ITP #Math
Diophantine equations over Z: Universal bounds and parallel formalization. ~ Jonas Bayer, Marco David, Malte Hassler, Yuri Matiyasevich, Dierk Schleicher. https://arxiv.org/abs/2506.20909 #IsabelleHOL #ITP #Math
Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization
This paper explores multiple closely related themes: bounding the complexity of Diophantine equations over the integers and developing mathematical proofs in parallel with formal theorem provers. Hilbert's Tenth Problem (H10) asks about the decidability of Diophantine equations and has been answered negatively by Davis, Putnam, Robinson and Matiyasevich. It is natural to ask for which subclasses of Diophantine equations H10 remains undecidable. Such subclasses can be defined in terms of universal pairs: bounds on the number of variables $ν$ and degree $δ$ such that all Diophantine equations can be rewritten in at most this complexity. Our work develops explicit universal pairs $(ν, δ)$ for integer unknowns, achieving new bounds that cannot be obtained by naive translations from known results over $\mathbb N$. In parallel, we have conducted a formal verification of our results using the proof assistant Isabelle. While formal proof verification has traditionally been applied a posteriori to known results, this project integrates formalization into the discovery and development process. In a final section, we describe key insights gained from this unusual approach and its implications for mathematical practice. Our work contributes both to the study of Diophantine equations and to the broader question of how mathematics is conducted in the 21st century.
The Mostowski collapse theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Mostowski_Collapse.html #IsabelleHOL #ITP #Math
Alon’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
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
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
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
