Formal Proof

A formal proof is a mathematical proof expressed in a precisely defined language, with every inferential step justified by explicit rules. It establishes that a conclusion follows from specified assumptions within a formal system, rather than relying on a reader to supply unstated reasoning. Formal proofs are central to logic and the foundations of mathematics, and they underpin computer-assisted verification of mathematical results, software, and hardware. Their defining feature is explicit, rule-governed justification—not necessarily the use of a computer. (leanprover.github.io)

Structure and a simple example

A formal system specifies the symbols and formation rules of its language, its axioms, and its permitted rules of inference. A proof may be represented as a finite sequence or tree of formulas. Each step must be an axiom, an authorized assumption, or a consequence of earlier steps under a stated rule. Rules involving temporary assumptions also specify when those assumptions may be discharged. A theorem is a statement derivable in the system; a derivation from additional premises establishes a conditional consequence. (builds.openlogicproject.org)

For example, in propositional logic, modus ponens permits the inference of $Q$ from $P$ and $P\rightarrow Q$:

1. $P$ — premise.
2. $P\rightarrow Q$ — premise.
3. $Q$ — modus ponens applied to steps 1 and 2.

Writing $\Gamma\vdash Q$ records that $Q$ is derivable from the assumptions in $\Gamma$. The derivation does not independently establish its premises; it shows that the conclusion follows when they are accepted. In a suitable implication-introduction system, discharging the assumptions yields the theorem $P\rightarrow((P\rightarrow Q)\rightarrow Q)$. (builds.openlogicproject.org)

Formalization therefore requires more than replacing ordinary words with symbols. Definitions, domains of quantification, assumptions, and dependencies must be sufficiently precise for the chosen rules to apply. Previously proved results can serve as reusable components, provided their statements and supporting derivations are available within the formal framework. (leanprover.github.io)

Proof systems and ordinary mathematical writing

Different proof systems organize deductive reasoning differently. Hilbert-style systems typically use axiom schemes and relatively few inference rules. Natural deduction uses introduction and elimination rules for logical connectives, often with nested subproofs. Sequent calculi make collections of assumptions and conclusions explicit. Proof theory studies these systems and the structural properties of their derivations. (openlogicproject.org)

The underlying logic also matters. Classical reasoning allows principles that are not generally available in intuitionistic logic, such as unrestricted elimination of double negation. Consequently, a classical proof by contradiction may require an additional principle when translated into a constructive framework. “Formal” does not identify one particular logic or foundation. (docs.lean-lang.org)

Ordinary mathematical proofs combine prose, notation, diagrams, and omitted routine steps. Such proofs can be rigorous without being fully formalized: their intended audience supplies background definitions and recognizes standard arguments. A formal derivation instead makes the required dependencies explicit enough for rule-based checking. It may expose a missing hypothesis, but it does not automatically communicate why an argument is illuminating or which ideas motivated its discovery. (leanprover.github.io)

Derivability, truth, and limitations

Formal derivability concerns the manipulation of expressions according to rules. Semantics concerns their interpretation. In first-order logic, $\Gamma\models\varphi$ means that every interpretation satisfying the premises $\Gamma$ also satisfies $\varphi$. This semantic consequence relation is distinct from the syntactic relation $\Gamma\vdash\varphi$. (builds.openlogicproject.org)

A deductive system is sound when derivability preserves semantic consequence, and complete when every semantic consequence is derivable. Standard classical first-order calculi have both properties. Completeness here means capturing consequences across all interpretations of the premises, not proving every statement true in one intended mathematical structure. (builds.openlogicproject.org)

Gödel’s incompleteness theorems establish a different limitation. A consistent, effectively axiomatized theory sufficiently strong to express elementary arithmetic cannot decide every sentence in its language: some sentences are neither provable nor refutable within it. This does not contradict first-order logical completeness, because completeness of a calculus and completeness of a particular axiomatic theory are different properties. (builds.openlogicproject.org)

Computer checking and proof assistants

A proof assistant supports the construction and checking of formal derivations. In Lean, for example, propositions are represented by types and proofs by terms inhabiting those types. Under this propositions-as-types interpretation, associated with type theory, checking a proof becomes a form of type checking. Implication corresponds to a function that transforms evidence for its premise into evidence for its conclusion. (docs.lean-lang.org)

Users need not manually write every primitive step. Tactics can simplify expressions, introduce assumptions, or search for intermediate arguments. In Lean’s ordinary proof-term workflow, their output is checked by a small kernel independently of the tactics that generated it. Nevertheless, trust depends on the kernel and on any additional mechanisms used; proofs relying on native evaluation may introduce broader implementation dependencies. Explicit axioms and unfinished-proof placeholders must also be distinguished from proved results. (lean-lang.org)

Applications and the scope of verification

In formal verification, software or hardware behavior is represented mathematically, and proofs establish that the representation satisfies a specification. An algorithm may be proved to return a result meeting its stated conditions. This guarantees the formal property under the model’s assumptions; the correspondence between the model, specification, and actual system remains a separate concern. (leanprover.github.io)

Large mathematical formalizations also demonstrate the method’s scale. The Flyspeck project produced a formal proof of the Kepler conjecture using HOL Light and Isabelle; its published account appeared in 2017. Its verification covered both mathematical arguments and extensive computational components. Auditing such a development includes examining the formal statement, its definitions, its assumptions, and the mechanisms used to check the derivation—not merely observing that proof scripts execute successfully. (cambridge.org)