Theorem

A theorem is a statement in mathematics established by a mathematical proof: a deductive argument showing that it follows from accepted assumptions, definitions, and previously established results. Unlike an axiom, which is adopted as a starting point within a theory, a theorem requires justification. Its validity depends on the assumptions and rules under which it is proved, rather than on the number of examples that support it. In mathematical writing, “theorem” commonly designates a result considered important within the subject. (ocw.mit.edu)

Statements, assumptions, and conclusions

A theorem typically identifies a class of objects, specifies conditions on those objects, and asserts a conclusion. Many have the logical form “if $P$, then $Q$,” where $P$ expresses the hypotheses and $Q$ the conclusion. Definitions determine the precise meaning of the terms involved. Hypotheses may be stated explicitly or supplied by the surrounding context; applying a theorem requires checking that the relevant conditions hold. A proof connects those conditions to the conclusion through justified intermediate steps. (ocw.mit.edu)

For example, the extreme value theorem states that a continuous real-valued function on a closed, bounded interval attains both an absolute maximum and an absolute minimum. The conditions are essential to this formulation. The function $f(x)=x$ on the open interval $(0,1)$ attains neither, while $f(x)=1/x$ on that interval is unbounded above. These examples illustrate why a theorem cannot generally be separated from its hypotheses. (openstax.org)

The conclusion may assert existence, uniqueness, an equality, or a relationship between properties. An existence statement need not specify a procedure for finding the object concerned. For instance, the intermediate value theorem guarantees that a continuous function takes every value between its endpoint values, but its statement does not provide a numerical method for locating the corresponding input. (openstax.org)

Related terminology

Several labels describe proved results, principally according to their role in an exposition:

• A lemma is usually an auxiliary result used to prove another result.
• A corollary follows with relatively little additional argument from an established result.
• A proposition often denotes a proved result presented with less emphasis than a theorem, although usage varies.
• A conjecture is a statement proposed as true but not yet established by proof. (web.mit.edu)

These distinctions are not a formal ranking of logical certainty. A proved lemma and a proved theorem have the same requirement of justification. The label reflects organization, emphasis, or historical convention: a lemma can become more influential than the theorem it originally supported. Furthermore, “proposition” can mean any truth-valued statement in logic, not only a result already proved. (ocw.mit.edu)

Proof and mathematical reasoning

Theorems are established through deductive reasoning, rather than by accumulating confirming observations. A proof must cover the full scope of the statement. Testing particular cases can suggest a conjecture or expose an error, but does not establish a universal assertion unless those cases exhaust its domain. A single counterexample, by contrast, refutes a universal claim. (ocw.mit.edu)

Mathematical exposition normally presents proofs in ordinary language supplemented by symbols, equations, and references to earlier results. Authors need not reproduce every foundational inference, but the argument must make its dependencies and logical transitions sufficiently clear. Results already proved can serve as components of later proofs, creating chains of dependence rather than requiring each theorem to begin again from the axioms. (web.mit.edu)

A formal proof makes the permitted expressions and inferential steps explicit within a formal system. One familiar inference rule is modus ponens: from $P$ and $P\rightarrow Q$, infer $Q$. Formalization distinguishes the exact derivation from the more compressed presentation used for human readers. (ocw.mit.edu)

Provability, truth, and independence

In formal logic, $T\vdash\varphi$ expresses that the statement $\varphi$ is derivable from a theory $T$. This syntactic relationship differs from $T\models\varphi$, which expresses that $\varphi$ is true in every model satisfying $T$. Gödel’s completeness theorem connects these notions for first-order logic: semantic consequence from a theory coincides with derivability in a sound, complete deductive calculus. Truth in one particular intended model is a different matter from truth in every model of the axioms. (plato.stanford.edu)

The incompleteness theorems establish limitations on effectively axiomatized theories capable of expressing sufficient elementary arithmetic. Any such consistent theory contains sentences for which neither the sentence nor its negation is provable within the theory. Under the relevant standard conditions, it also cannot prove its own consistency. These results concern specific formal frameworks; they do not imply that established mathematical proofs are merely empirical guesses. (plato.stanford.edu)

Computer verification

A proof assistant supports the construction and checking of formal proofs. In systems such as Lean, theorem statements are represented as propositions, and proofs are represented by terms whose types express those propositions. Automated procedures can help construct these terms, while a checking kernel verifies that they conform to the underlying type theory. Finding a proof and checking a supplied proof are therefore distinct tasks. (docs.lean-lang.org)

Computer verification remains relative to the formal statement and its assumptions. A checked proof establishes the encoded proposition, so accurate definitions and faithful translation of the intended claim matter. Lean also records which axioms a declaration depends on, directly or through other results, allowing those dependencies to be inspected separately from the theorem’s surface statement. (lean-lang.org)