Linked from

The 25 pages that link to Formal proof, each with the reason it gives.

• Mathematical proofRelated: Formalization makes every permitted proof step mechanically checkable.

• Sequent calculusNarrower topic: A sequent-calculus derivation is a formal proof built from rule applications.

• Principia MathematicaNarrower topic: The work presents mathematics as derivations governed by formal inference rules.

• Proof theoryBroader topic: Formal proofs are the central objects whose form and properties proof theory examines.

• SoundnessRelated: Soundness constrains what conclusions the system's proofs can establish.

• Peano arithmeticRelated: Theorems of Peano arithmetic are established by derivations from its axioms.

• Interpretation (logic)Compared with: Interpretation is semantic; proof is syntactic, though soundness links the two.

• Formal logicBroader topic: A proof makes an inference valid by exhibiting its permitted derivation.

• Foundations of mathematicsRelated: Its precise rules clarify what counts as a mathematical demonstration.

• Axiomatic methodRelated: Proofs make the derivation from axioms explicit and checkable.

• Computer-assisted proofNarrower topic: Formalization offers a route from complex machine-assisted arguments to mechanically checked derivations.

• DerivationRelated: A proof is a derivation whose final statement is the theorem being established.

• Gödel's completeness theoremRelated: The theorem guarantees a formal proof for every sentence valid in all models.

• CompletenessRelated: Provability in a deductive system is witnessed by a formal proof.

• Diagonal lemmaRelated: The conclusion is a provable equivalence, not merely an informal claim of matching meaning.

• Independence (mathematical logic)Narrower topic: Independence concerns the absence of proofs of both a sentence and its negation.

• Geometric proofRelated: Formalization makes geometric deductions precise enough for symbolic verification.

• Logical validityCompared with: Proof is a syntactic derivation; validity concerns truth preservation across interpretations.

• Axiom schemaRelated: A proof may use any permitted instance of an axiom schema as a starting statement.

• Gödel sentenceNarrower topic: Unprovability means that no such sequence ends with the Gödel sentence.

• Paris–Harrington theoremRelated: The theorem distinguishes mathematical truth from formal provability.

• Kepler conjectureRelated: The Flyspeck project used formal verification to check the proof’s full chain of reasoning.

• Lagrange inversion theoremRelated: The theorem's coefficient identity admits a purely algebraic proof.

• Deduction theoremNarrower topic: The theorem compares which conclusions have formal derivations under different premises.

• Löb's theoremBroader topic: The theorem turns a claim about the existence of such a proof into a proof of the sentence.