• Tarski's name and university are incorrect.
  It should have been written Alfred Tarski at UC Berkeley.
• The article incorrectly states: "Computers have found proofs of mathematical conjectures before, of course, but those conjectures were easy to prove". Many of those previous proofs were quite difficult. Look here for many examples.
• There are a few theoretical applications of the Robbins Theorem (on the size of axiom systems) but no practical ones that we know of.
• Wos is not McCune's supervisor :-) Both are staff members in the Mathematics and Computer Science Division; their supervisor is Rick Stevens.
• The correct name of our workplace is Argonne National Laboratory. We frown upon the name Argonne Labs.
• The automated deduction project is supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Computational and Technology Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.