# Tagged Questions

For questions regarding the different ways to generate and verify theorems via specialized computer languages, algorithms, and other computer-aided tools.

339 views

### In a monoid, does $x \cdot y=e$ imply $y \cdot x=e$?

A monoid is a set $S$ together with a binary operation $\cdot:S \times S \rightarrow S$ such that: The binary operation $\cdot$ is associative, that is, $(a\cdot b) \cdot c=a\cdot (b \cdot c)$ for ...
2k views

### Has any previously unknown result been proven by an automated theorem prover?

The Wikipedia page on automated theorem proving states: Despite these theoretical limits, in practice, theorem provers can solve many hard problems... However it is not clear whether these 'hard ...
444 views

### Rings with $a^5=a$ are commutative

Let $R$ be a ring such that $a^5=a$ for all $a \in R$. Then it follows that $R$ is commutative. This is part of a more general well-known theorem by Jacobson for arbitrary exponents ($a^n=a$), which ...
907 views

### What are the theorems of mathematics proved by a computer so far?

By theorems, I mean the ones you can find in an undergraduate course of mathematics, not the ones you can find in a textbook of automated proofs. I mean by "proved by a computer" that an existing ...
In first order logic we often convert prenex normal form statements to Skolem normal form statements to eliminate the existential quantifier: $\exists$x$\forall$y$\exists$z$\phi$(x,y,z) becomes \$\...