Because propositions are types whose inhabitants count as proofs, theorems and definitions are technically very similar. However, because their use cases are quite different, they differ in many details:

• The theorem statement must be a proposition. The types of definitions may inhabit any universe.

• A theorem's header (that is, the theorem statement) is completely elaborated before the body is elaborated. Section variables only become parameters to the theorem if they (or their dependents) are mentioned in the header. This prevents changes to a proof from unintentionally changing the the theorem statement.

• Theorems are irreducible by default. Because all proofs of the same proposition are definitionally equal, there few reasons to unfold a theorem.

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private`, `protected`, or `public`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      theorem `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig := termTermination hints are `termination_by` and `decreasing_by`, in that order.

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private`, `protected`, or `public`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      theorem `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig
        (| term => term)*Termination hints are `termination_by` and `decreasing_by`, in that order.

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private`, `protected`, or `public`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      theorem `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig where
        structInstField*