The tag has no wiki summary.

learn more… | top users | synonyms

5
votes
3answers
314 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 ...
38
votes
6answers
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 ...
15
votes
1answer
295 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 ...
15
votes
6answers
750 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 ...
4
votes
2answers
60 views

When is de-Skolemizing statements appropriate?

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 ...