José A. AlonsoReadings shared April 9, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/10-readings_shared_04-09-26 #AI #AI4Math #ATP #Agda #FunctionalProgramming #ITP #IsabelleHOL #LeanProver #Math #Prover9
An optimal 14-symbol hybrid basis for BCH-algebras. ~ Mahesh Ramani, Shlok Kumar. https://arxiv.org/abs/2603.29137v1 #Prover9 #ATP #Math
An Optimal 14-Symbol Hybrid Basis for BCH-Algebras
We present an optimally minimal two-axiom basis for BCH-algebras. The standard presentation of a BCH-algebra relies on three axioms: two equations and one quasi-identity. Using automated theorem proving, we prove that the two standard equations can be entirely replaced by a 14-symbol equation, ((xy)z)((x(z0))y) = 0, while retaining the standard quasi-identity. We then provide a rigorous proof of strict minimality for this new equational companion. By employing an exhaustive, machine-assisted search space generation coupled with finite countermodel building, we demonstrate that no equation of 12 or fewer symbols can define the class of BCH-algebras when paired with the standard quasi-identity. Our literature searches have revealed no prior proof of this result, to the extent of our knowledge. All equivalence derivations were verified using Prover9, and all minimality countermodels were generated using Mace4.
Readings shared March 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/03/20-readings_shared_02-19-26 #ATP #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Physics #Prover9
In the mood for inference: Logic-based natural language inference with large language models. ~ Bill Noble, Rasmus Blanck, Gijs Wijnholds. https://scholarlypublications.universiteitleiden.nl/access/item%3A4294827/download #Prover9 #ATP #LLMs
Readings shared January 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/25-readings_shared_01-24-26 #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver
Elementary proofs of ring commutativity theorems. ~ Michael Kinyon, Desmond MacHale. https://arxiv.org/abs/2601.12599v1 #ATP #Prover9 #Math
Elementary proofs of ring commutativity theorems
Jacobson's commutativity theorem says that a ring is commutative if, for each $x$, $x^n = x$ for some $n > 1$. Herstein's generalization says that the condition can be weakened to $x^n-x$ being central. In both theorems, $n$ may depend on $x$. In this paper, in certain cases where $n$ is a fixed constant, we find equational proofs of each theorem. For the odd exponent cases $n = 2k+1$ of Jacobson's theorem, our main tool is a lemma stating that for each $x$, $x^k$ is central. For Herstein's theorem, we consider the cases $n=4$ and $n=8$, obtaining proofs with the assistance of the automated theorem prover Prover9.
Marginal subsemigroups and commutators in inverse semigroups. ~ Gonçalo Araújo, João Araújo, Michael Kinyon https://link.springer.com/article/10.1007/s00233-025-10548-9 #ATP #Prover9 #Math
Marginal subsemigroups and commutators in inverse semigroups - Semigroup Forum
Marginal subgroups, introduced by P. Hall, are characteristic subgroups induced by group words. The goal of this paper is to extend the notion to inverse semigroups. Our first main result establishes that these marginal subsemigroups are full inverse subsemigroups. We then examine the special case in which the word is the commutator, showing that the induced marginal inverse subsemigroup coincides with the metacenter, which is a normal inverse subsemigroup. In the process we prove some results about commutators in inverse semigroups and in Clifford semigroups. The paper concludes with several open problems.
Readings shared June 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/11-readings_shared_06-10-25 #AI #AIforMath #ATP #AlphaProof #Emacs #ITP #IsabelleHOL #LLMs #LeanProver #Math #Prover9
Are LLMs reliable translators of logical reasoning across lexically diversified contexts? ~ Qingchuan Li et als. https://arxiv.org/abs/2506.04575v1 #LLMs #Math #ATP #Prover9
Are LLMs Reliable Translators of Logical Reasoning Across Lexically Diversified Contexts?
Neuro-symbolic approaches combining large language models (LLMs) with solvers excels in logical reasoning problems need long reasoning chains. In this paradigm, LLMs serve as translators, converting natural language reasoning problems into formal logic formulas. Then reliable symbolic solvers return correct solutions. Despite their success, we find that LLMs, as translators, struggle to handle lexical diversification, a common linguistic phenomenon, indicating that LLMs as logic translators are unreliable in real-world scenarios. Moreover, existing logical reasoning benchmarks lack lexical diversity, failing to challenge LLMs' ability to translate such text and thus obscuring this issue. In this work, we propose SCALe, a benchmark designed to address this significant gap through **logic-invariant lexical diversification**. By using LLMs to transform original benchmark datasets into lexically diversified but logically equivalent versions, we evaluate LLMs' ability to consistently map diverse expressions to uniform logical symbols on these new datasets. Experiments using SCALe further confirm that current LLMs exhibit deficiencies in this capability. Building directly on the deficiencies identified through our benchmark, we propose a new method, MenTaL, to address this limitation. This method guides LLMs to first construct a table unifying diverse expressions before performing translation. Applying MenTaL through in-context learning and supervised fine-tuning (SFT) significantly improves the performance of LLM translators on lexically diversified text. Our code is now available at https://github.com/wufeiwuwoshihua/LexicalDiver.