REVIEW 3 major objections 4 minor 11 references
Studying Algebraic Structures using Prover9 and Mace4
T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read In every bounded hoop, the double-dual operation preserves both $\ominus$ and $\oplus$.
desk verdict A real result about double-dual homomorphisms in hoops, but the human-readable proof of Theorem 2.18 contains a false bridge identity. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the double-dual operation on a bounded hoop, with $x^\perp = 1 \ominus x$. The argument is carried by three derived operations mined from the theorem prover's output: $x \cap y = x \ominus (x \ominus y)$, $y \setminus x = (x \oplus y) \ominus x$, and $x \downarrow y = x^\perp \oplus (x \ominus y)$. These operations organize the proof: commutativity of $\downarrow$ (Lemma 2.2), the duality $(x \cap y)^\perp = x \downarrow y$ (Lemma 2.3), the decomposition $x = (x \cap y) \oplus (x \ominus y)$ (Lemma 2.11), and the final duality $(y \ominus x^\perp)^\perp = x^\perp \oplus y^\perp$ (Lemma 2.17) lead directly to the two homomorphism theorems.
What would settle it
Search exhaustively for a bounded hoop with more than 20 elements (or any size) in which either $(x \ominus y)^{\perp\perp} \neq x^{\perp\perp} \ominus y^{\perp\perp}$ or $(x \oplus y)^{\perp\perp} \neq x^{\perp\perp} \oplus y^{\perp\perp}$; finding one would refute the theorems. Conversely, checking the two machine derivations with an independent proof checker would confirm them.
Extended reading notes
Core claim
In a bounded hoop, define $x^\perp = 1 \ominus x$. The central claim is that the double-dual map $x \mapsto x^{\perp\perp}$ preserves both operations: Theorem 2.10 proves $(x \ominus y)^{\perp\perp} = x^{\perp\perp} \ominus y^{\perp\perp}$, and Theorem 2.18 proves $(x \oplus y)^{\perp\perp} = x^{\perp\perp} \oplus y^{\perp\perp}$. The proof turns on a weaker replacement for idempotence: while $x \ominus x^{\perp\perp}$ need not be $0$, it is negligible in the sense that $(x \ominus x^{\perp\perp})^\perp = 1$, and more generally $(y \ominus x^\perp)^\perp = x^\perp \oplus y^\perp$. These identities were found by mining a 177-step machine proof for the first theorem and a 624-step proof for the second, isolating the derived operations $x \cap y = x \ominus (x \ominus y)$, $y \setminus x = (x \oplus y) \ominus x$, and $x \downarrow y = x^\perp \oplus (x \ominus y)$, whose simple properties make the final proofs short.
Load-bearing premise
The paper assumes that the automated proof search output is correct and that the 'easy' or 'immediate' steps in the human-readable lemmas are valid; one such step, the identity $(x \cup y)^\perp = (y \ominus x)^\perp \ominus x$ in Lemma 2.12, is asserted without proof.
Editorial extensions
If this is right
- In every bounded hoop, the set of double-dual elements is closed under $\ominus$ and $\oplus$, so it carries the structure of a subhoop.
- The identity $(x \ominus y)^\perp = x^\perp \oplus y^{\perp\perp}$ gives a De Morgan-style duality in hoops, expressing a difference as a sum even though hoops lack idempotence.
- The proof-mining cycle reduces a 7-hour, 624-step automated derivation to a few lemmas with proofs of about ten steps each, showing that machine proofs can be converted into explanatory human proofs.
- The guided workflow—conjecture, search for small counterexamples, prove with automation, mine the proof—is presented as a practical template for undergraduate algebra projects.
Reading between the lines
- If the double-dual is a homomorphism, the double-dual elements of any bounded hoop form a retract of the hoop, and this subalgebra may inherit Heyting-algebra-like behavior even when the ambient hoop is not idempotent; the authors leave this corollary unstated.
- The same lemma-extraction recipe could be tested on other classes of algebras with a pseudocomplement, such as residuated lattices or BCK-algebras, to look for double-negation homomorphisms; this would show whether the method generalizes.
- A natural testable extension is whether the two identities survive dropping the constants $0$ and $1$ (unbounded hoops) or adding operations, since the proofs rely on the boundedness constants.
- An independent formal verification of Theorems 2.10 and 2.18 would settle the residual reliance on the unverified output of the automated search; the paper does not include one.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper presents a case study of using Prover9 and Mace4 to discover and prove algebraic results about hoops, a class of structures generalizing Heyting algebras. After an introductory section that uses semilattices to illustrate the tools and that introduces the hoop axioms, the paper states Theorem 1.1, a count of finite linearly ordered hoops, based on Mace4 data and a human-directed induction. The main mathematical contribution is in Section 2, where the authors investigate whether the double-dual operation x⊥ = 1 ⊖ x is a homomorphism for the subtractive and monoidal operations of a hoop. They report Prover9 proofs of the identities (x ⊖ y)⊥⊥ = x⊥⊥ ⊖ y⊥⊥ and (x ⊕ y)⊥⊥ = x⊥⊥ ⊕ y⊥⊥, and they present human-readable proofs obtained by mining the machine proofs for derived operations (∪, ∩, \, ↓) and for a series of lemmas (Lemmas 2.1–2.17). The chapter concludes with a discussion of proof mining, explanation, and teaching applications.
Significance. If the results are correct, the paper illustrates a compelling workflow that combines machine search, model generation, and human proof analysis. The two homomorphism identities are nontrivial and are supported by separately reported Prover9 runs and by the provided scripts, which is a real strength. The methodological sections are clear and accessible. However, the human-readable proof of Theorem 2.18, which is the paper's headline second result, contains an unproved bridge identity, and a number of lemmas rely on 'easy' steps that are not expanded. Since the chapter explicitly promises full human-readable proofs, these gaps are significant and need to be addressed before the paper is ready.
major comments (3)
- [2.5, proof of Theorem 2.18] The proof of Theorem 2.18 is reduced to Lemma 2.17 by the assertion 'since (x ⊕ y)⊥⊥ = (y⊥ ⊖ x⊥⊥)⊥'. This bridge identity is neither proved nor derived from the earlier lemmas. It is not a superficial consequence of Lemma 2.17: the stronger identity x ⊕ y = y ⊕ x⊥⊥ fails in the hoop L3⌢L2 of Table 2 (take x = b and y = a), so the variables in Lemma 2.17 cannot simply be swapped. The bridge is, in fact, an instance of the general duality (x ⊖ y)⊥ = x⊥ ⊕ y⊥⊥ mentioned in Remark 2.1, but that duality is also not proved in the paper. The authors should prove the bridge identity explicitly (or prove the general duality) before claiming that Lemma 2.17 'immediately implies' the theorem.
- [2.3, proof of Lemma 2.7] Lemma 2.7 is proved using two identities that are merely asserted as 'It is easy to show' and 'It is also easy to see', namely (∗) x ⊕ (x⊥ ⊖ (x ⊖ x⊥⊥)) = 1 and (†) ((X ⊥ ⊖ x) ⊖ ((x ⊕ (x⊥ ⊖ X)) ⊖ x)) = 0 with X = x ⊖ x⊥⊥. These identities are not algebraically obvious, and the second is quite complex. Since Lemma 2.7 is used in the proof of Lemma 2.8, which in turn is used in the proof of Theorem 2.10, the reader cannot verify the human-readable proof chain without filling these gaps. Please expand the derivations or give pointers to the specific Prover9 proof steps where these identities appear.
- [1.2, proof of Theorem 1.1] The proof of Theorem 1.1 rests on two unproved assertions: that every finite linearly ordered hoop decomposes as Lm ⌢ K for some m and subhoop K, and that ordinal sums Lm1 ⌢ ... ⌢ Lmk are classified up to isomorphism by the sequence (m1,...,mk). The first is sketched in a single sentence ('This observation may be proved by considering the subhoop generated by the least non-zero element'), and the second is declared 'easy to see'. Because the theorem is stated as a result and the proof is the basis for counting 2^(n−2) hoops, the authors should either provide a full proof or cite a reference where this structure theorem is established.
minor comments (4)
- [Throughout] There are several typos, including 'resonably' for 'reasonably', 'inacessible' for 'inaccessible', 'avoiding' for 'avoided', and a stray '/suppress' prefix on 'Lukasiewicz'.
- [2.3, proof of Lemma 2.12] The identity (x ∪ y)⊥ = (y ⊖ x)⊥ ⊖ x is asserted without proof; it follows from axiom (5) in about two lines and should be shown or at least labelled.
- [2.4, proof of Lemma 2.15] In the displayed step '= x⊕y⊥) ⊖ x Easy', there are mismatched parentheses; it should read '= (x⊕y⊥) ⊖ x'.
- [1.2, after Table 2] The paper would benefit from a brief explanation of how the model counts are obtained from the Mace4 output, particularly the assertion that there are 8 linearly ordered hoops of order 5.
Circularity Check
No circularity: the hoop homomorphism theorems are derived from the hoop axioms via intermediate lemmas; no target result is used as an assumption and no fitted parameter is renamed as a prediction.
full rationale
The central claims (9) and (10) are equational identities whose human-readable derivations in Section 2 start from the hoop axioms and intermediate lemmas (Lemmas 2.1-2.17). The lemmas are not restatements of the target theorems: for example, Theorem 2.10 is obtained by composing Lemma 2.6, Lemma 2.9, and Lemma 2.1(vi), each of which is asserted for all hoops and used as an intermediate step, not as an assumption of the result being proved. Theorem 2.18 follows from Lemma 2.17 together with the identity (x⊕y)⊥ = y⊥⊖x, which is an instance of hoop axiom (5); the conclusion is not definitionally identical to the lemma. No parameter is fitted to data, no known result is merely renamed, and no self-citation carries the argument. The paper does leave some 'easy' identities unexpanded, such as Lemma 2.12's use of (x∪y)⊥ = (y⊖x)⊥⊖x and the bridge identity in Theorem 2.18; these are potential correctness or proof-completeness risks, not circular dependence, because the derivation never assumes the very equality being proved. Mace4 is used only to filter conjectures and Prover9 is used to search for equational proofs; neither supplies fitted inputs to the final identities.
Assumptions & free parameters
assumptions (4)
- domain assumption Hoop axioms (1)-(8): commutative monoid, subtraction identities, and axiom (6).
- domain assumption Derived algebraic facts used as lemmas (monotonicity, residuation, EFQ, and various 'easy' identities).
- domain assumption Soundness of Prover9: a 'THEOREM PROVED' output is a valid first-order proof from the assumptions.
- domain assumption Completeness of Mace4 enumeration of finite hoops and pocrims up to size 5.
Cite this review
Pith. "Pith review of Studying Algebraic Structures using Prover9 and Mace4." pith.science (2026). https://pith.science/paper/RM4XM2R4
@misc{pith2026190806479,
author = {Pith},
title = {Pith review of: Studying Algebraic Structures using Prover9 and Mace4},
year = {2026},
howpublished = {\url{https://pith.science/paper/RM4XM2R4}},
note = {Machine review of arXiv:1908.06479}
}
read the original abstract
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a class of algebraic structures. We will see that these tools, when combined with human insight and traditional algebraic methods, help us to explore the problem space quickly and effectively. The counter-example generator rapidly rules out many false conjectures, while the theorem prover is often much more efficient than a human being at verifying algebraic identities. The specific tools in our case study are Prover9 and Mace4; the algebraic structures are generalisations of Heyting algebras known as hoops. We will see how this approach helped us to discover new theorems and to find new or improved proofs of known results. We also make some suggestions for how one might deploy these tools to supplement a more conventional approach to teaching algebra.
Figures
Reference graph
Works this paper leans on
-
[1]
W. J. Blok and I. M. A. Ferreirim. On the structure of hoops . Algebra Universalis, 43(2-3):233–257, 2000. 5
work page 2000
-
[2]
B. Bosbach. Komplement¨ are Halbgruppen. Axiomatik und Arithmetik. Fundam. Math., 64:257–287, 1969. 5, 6
work page 1969
-
[3]
J. R. B¨ uchi and T. M. Owens. Complemented monoids and hoo ps. Unpublished manuscript, c. 1974. 5, 6
work page 1974
-
[4]
Stanley. Burris. An Anthropomorphized Version of McCun e’s Machine Proof that Robbins Algebras are Boolean Algebras. Private communicat ion., c. 1997. 1
work page 1997
-
[5]
Bernd I. Dahn. Robbins algebras are Boolean: A revision o f McCune’s computer- generated solution of Robbins problem. J. Algebra, 208(2):526–532, 1998. 1
work page 1998
-
[6]
The role and function of proof in mat hematics
Michael de Villiers. The role and function of proof in mat hematics. Pythagoras, 24:17–24, 11 1990. 20 20
work page 1990
-
[7]
J. /suppress Lukasiewicz and A. Tarski. Untersuchungen ¨ uber denAussagenkalk¨ ul.C. R. Soc. Sc. Varsovie 23 , (1930):30–50, 1930. 7
work page 1930
-
[8]
W. McCune. Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/, 2005–2010. 1
work page 2005
Show all 11 references
-
[9]
Solution of the Robbins problem
William McCune. Solution of the Robbins problem. J. Autom. Reasoning, 19(3):263– 276, 1997. 1
1997
-
[10]
E. Moggi. Computational lambda-calculus and monads. I n Symposium of Logic in Computer Science, California, June 1989. IEEE. 12
1989
-
[11]
S. Winker. Absorption and idempotency criteria for a pr oblem in near-Boolean algebras. J. Algebra, 153(2):414–423, 1992. 1 21
1992
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.