Beweis einer – in der Regel in einer elementaren Sprache formulierten – mathematischen Aussage allein mit Hilfe von fixierten formalen Schlußregeln.

Zur Präzisierung des mathematischen Beweisbegriffs benötigt man eine formale Sprache L (elementare Sprache), ein in der Sprache formuliertes System logischer Axiome Ax (logisches Axiom), die als logische Voraussetzungen bei jedem Beweis uneingeschränkt benutzt werden dürfen und ein für die beabsichtigten Anwendungen geeignetes System logischer Schlußregeln (:= Beweisregeln; logische Ableitungsregeln). Ist Σ eine beliebige Menge von Ausdrücken oder Aussagen aus L und φ ein Ausdruck, dann ist φ aus Σ formal beweisbar (oder ableitbar), wenn es eine endliche Folge (φ₁,…,φ_n) von Ausdrücken aus L so gibt, daß φ_n = φ, und für jedes φ_i mit i = 1,…, n eine der folgenden Bedingungen erfüllt ist:

1. φ_i ∈ Ax (φ ist ein logisches Axiom), oder
2. φ_i, ∈ Σ (φ_i gehört zur Menge der Voraussetzungen, aus denen φ bewiesen werden soll), oder
3. φ_i, ist eine direkte Konsequenz aus vorhergehenden Folgegliedern, entsprechend der zulässigen Beweisregeln.

(φ₁,…, φ_i) heißt dann Ableitungsfolge oder formaler Beweis von φ aus Σ. In der klassischen zweiwertigen Logik sind (bei geeignetem Axiomensystem Ax) die folgenden beiden Beweisregeln ausreichend:

Vernünftige Beweisregeln sind so zu wählen, daß sie von wahren Voraussetzungen zu wahren Behauptungen führen. Das Axiomensystem Ax und die Beweisregeln sollten nach Möglichkeit so gestaltet sein, daß alle Aussagen, die aus Σ inhaltlich folgen, auch formal beweisbar sind (Beweismethoden).