What is the difference between definitions and theorems?

In the current version of the Software Foundations, the relevant explanation is formulated with intentional leeway.

First, we've used the keyword Theorem instead of Example. This difference is mostly a matter of style; the keywords Example and Theorem (and a few others, including Lemma, Fact, and Remark) mean pretty much the same thing to Coq.

(I put the wording used to introduce uncertainty in bold.)

In an earlier version of, evidently, the same writing, it was put strongly:

The form of this theorem and proof are almost exactly the same as the examples above: the only differences are that we've added the quantifier ∀ n:nat and that we've used the keyword Theorem instead of Example. Indeed, the latter difference is purely a matter of style; the keywords Example and Theorem (and a few others, including Lemma, Fact, and Remark) mean exactly the same thing to Coq.

(I put words introducing strength in bold.)

Looking at the official documentation, all of these words, and more, belong to the same grammatical category «assertion keyword»:

assertion_keyword  ::=  Theorem | Lemma
                        Remark | Fact
                        Corollary | Property | Proposition
                        Definition | Example

There are further two sections explaining how these keywords work: «Definitions» and «Assertions and proofs». In short:

Definitions extend the environment with associations of names to terms.

— And:

An assertion states a proposition (or a type) of which the proof (or an inhabitant of the type) is interactively built using tactics.

But, as far as I see, a theorem also extends the environment, and an example can be built with tactics. So, I am not seeing where these things are different. But the Software Foundation is a clever book. If they chose to be uncertain, there must be a reason?

Solution

As of today the differences are minimal, and could be summarized as:

Theorem/Example/Definition/... do produce different entries in the documentation; this is the most relevant difference.
Some forms such as Theorem don't support the syntactical form Theorem foo := nat. for non-interactive mode, which is supported by Definition for example.

Another non-trivial difference is whether you use the interactive mode or not. That is to say:

Definition foo : Type := nat.

and

Definition foo : Type. Proof. apply nat. Qed.

will take slightly different code paths due to the second creating an interactive proof; the codepath when the definition gets sent to the kernel is a bit different, but Coq 8.12 should unify them for all practical purposes, just marking the second proof as opaque.