定理是数学中通过数学证明确立的陈述。数学证明是一种演绎论证，用来说明该陈述可由公认的假设、定义和此前已确立的结果推导出来。公理在理论中被采纳为出发点，而定理则需要证明其成立。定理的有效性取决于证明所依据的假设和规则，而不是支持它的例子有多少。在数学文献中，“定理”通常指在该领域内被认为较为重要的结果。(ocw.mit.edu)
陈述、假设与结论
定理通常会指明一类对象，规定这些对象应满足的条件，并断言某个结论。许多定理具有“若 (P)，则 (Q)”的逻辑形式，其中 (P) 表示假设，(Q) 表示结论。定义确定了所涉及术语的精确含义。假设可以明确写出，也可以由上下文给定；应用定理时，必须检查相关条件是否成立。证明则通过有充分依据的中间步骤，将这些条件与结论联系起来。(ocw.mit.edu)
例如，极值定理指出，定义在有界闭区间上的连续实值函数既能取到绝对最大值，也能取到绝对最小值。对这一表述而言，这些条件不可或缺。定义在开区间 ((0,1)) 上的函数 (f(x)=x) 既取不到最大值，也取不到最小值，而同一区间上的函数 (f(x)=1/x) 则没有上界。这些例子说明，定理通常不能脱离其假设。(openstax.org)
结论可以断言某个对象的存在性、唯一性、某个等式成立，或某些性质之间的关系。存在性陈述不一定会给出寻找相关对象的方法。例如，介值定理保证连续函数能够取到其两端点函数值之间的每一个值，但定理的陈述并未提供求出相应自变量值的数值方法。(openstax.org)
相关术语
已获证明的结果有多种称呼，主要取决于它们在论述中的作用：
- **引理**通常是用于证明另一结果的辅助性结果。
- **推论**是只需较少的额外论证，就能从已确立的结果中得出的结果。
- 命题通常指已获证明、但在表述中不如定理那样受到强调的结果，不过具体用法有所不同。
- **猜想**是被提出并认为可能为真，但尚未获得证明的陈述。(web.mit.edu)
这些区别并不是对逻辑确定性作出的正式分级。已获证明的引理和定理，都必须满足同样的论证要求。它们的称呼反映的是论述的组织方式、强调程度或历史惯例：一个引理的影响力可能超过它最初用来支持的定理。此外，在逻辑学中，“命题”可以指任何具有真值的陈述，而不只是已经证明的结果。(ocw.mit.edu)
证明与数学推理
定理通过演绎推理确立，而不是靠积累支持它的观察结果来确立。证明必须涵盖陈述的全部适用范围。检验个别情形可以启发猜想或揭示错误，但除非这些情形穷尽了陈述的适用范围，否则不能据此确立一个全称断言。反之，只需一个反例，就能驳倒一个全称断言。(ocw.mit.edu)
数学论述通常以自然语言呈现证明，并辅以符号、方程以及对先前结果的引用。作者不必重述每一步基础性推理，但论证必须足够清楚地交代其所依赖的前提和逻辑上的衔接。已经证明的结果可以作为后续证明的组成部分，由此形成依赖链，而不必让每个定理都重新从公理开始证明。(web.mit.edu)
形式证明在一个形式系统内，明确规定允许使用的表达式和推理步骤。一条常见的推理规则是肯定前件式：由 (P) 和 (P\rightarrow Q) 推出 (Q)。形式化将精确的推导过程与面向人类读者、较为简略的证明表述区分开来。(ocw.mit.edu)
可证明性、真与独立性
在形式逻辑中，(T\vdash\varphi) 表示陈述 (\varphi) 可以从理论 (T) 推导出来。这种句法关系不同于 (T\models\varphi)，后者表示 (\varphi) 在所有满足 (T) 的模型中都为真。哥德尔完备性定理在一阶逻辑中将这两个概念联系起来：一个陈述是某理论的语义后承，当且仅当它能在可靠且完备的演绎演算中从该理论推导出来。在某个特定的预期模型中为真，与在公理的每一个模型中都为真，是不同的事情。(plato.stanford.edu)
哥德尔不完备定理揭示了能够表达足够多初等算术内容的、可有效公理化的理论所受到的限制。任何满足这些条件且一致的理论，都包含某些语句，使得这些语句及其否定在该理论内均不可证明。在相关的标准条件下，这样的理论也无法证明自身的一致性。这些结果针对的是特定的形式框架，并不意味着已经确立的数学证明只是经验性的猜测。(plato.stanford.edu)
计算机验证
证明助手支持形式证明的构造与检查。在 Lean 等系统中，定理陈述被表示为命题，证明则被表示为项，而这些项的类型表达了相应命题。自动化程序可以帮助构造这些项，检查内核则验证它们是否符合底层类型论的规则。因此，寻找证明与检查给定的证明是两项不同的任务。(docs.lean-lang.org)
计算机验证仍然是相对于形式化陈述及其假设而言的。通过检查的证明确立的是编码后的命题，因此，定义的准确性以及对预期断言的忠实转写十分重要。Lean 还会记录一项声明直接或通过其他结果所依赖的公理，使人们能够在查看定理的表面陈述之外，单独检查这些依赖关系。(lean-lang.org)