FOM: Are machines better in math?

[charles silver]

    I previously posted the question whether chess is as interesting 
as mathematics, intending to stimulate discussion on the role of 
mathematical insight in obtaining results.   However, immediately 
after posting the earlier question, I happened to stumble upon
a short account documenting the success of theorem provers in 
"discovering" new theorems. 
*****************************************
[This was posted 1996.   Probably many new results 
have been obtained since then.]

A Summary of New Results in Mathematics Obtained with Argonne's Automated
Deduction Software

  1.. Algebraic Geometry
    a.. Cancellative Semigroups on a Cubic Curve
    b.. Uniqueness of the 5-ary Steiner Law
  2.. Cancellative Semigroups
  3.. Lattice Theory
    a.. A Simpler Absorptive Basis for Lattice Theory
    b.. A New Schema for Single Axioms
    c.. A Shorter Single Axiom for Lattice Theory
    d.. A Single Axiom for Weakly Associative Lattices
  4.. Quasilattice Theory
  5.. Uniqueness of Operations in Lattice-like Algebras
  6.. Self-dual Bases for Boolean Algebra
  7.. Self-dual 2-Basis for Group Theory
  8.. Self-dual Bases for Group Varieties
  9.. Quasigroup Theory
  10.. Quasigroup Design Problems
  11.. Single Axioms for Ternary Boolean Algebra
  12.. Single Axioms for Groups
    a.. Ordinary Groups
    b.. Abelian Groups
    c.. Exponent Groups
    d.. Some Permutative Varieties
    e.. Ordinary Groups (Kunen)
    f.. Groups of Exponent 4 (Kunen)
    g.. Odd Exponent Groups (Hart and Kunen)
  13.. Simple Bases for Moufang Loops
  14.. Single Axioms for Inverse Loops and Subvarieties
  15.. Left Group and Right Group Calculi
  16.. Fixed Point Combinators
  17.. Semigroup Structure (F3B2)
  18.. Illative Combinatory Logic (Jech)
  19.. Robbins Algebra and Boolean Algebra
  20.. Equivalential Calculus Single Axioms
  21.. Semigroups, Antiautomorphisms, and Involutions
  22.. Independence of Ternary Boolean Algebra Axioms
  23.. Two-valued Sentential Calculus
  24.. Many-valued Sentential Calculus
  25.. Short Proofs in Various Logic Calculi
  26.. Pure Proofs in Equivalential Calculus