Can an AI Prove That Its Own Reasoning Is Correct?

Chapter 1 — Why plausible answers are not proofs

A language model generates text that is statistically plausible given its training and prompt. That process can produce a correct final answer with an invalid derivation (lucky cancellation of two errors), or a flawless-sounding derivation of a false statement. ESTABLISHED distinction: factual accuracy (does the answer match the world?), logical validity (does each step follow?), and verified artifact (has a machine checked the steps against formal rules?). Confidence scores measure none of these — they measure the model's own output distribution. This article refuses to anthropomorphize: “the AI believes” is shorthand; the engineering reality is tokens, weights and a loss function.

Chapter 2 — Foundations of formal logic

A proposition is a statement that is true or false. Predicates are propositions with holes (P(x): “x is even”). Connectives combine them: AND (∧), OR (∨), NOT (¬), IMPLIES (→). Quantifiers range over domains: ∀ (for all), ∃ (there exists). An inference rule licenses a step — modus ponens: from P and P→Q, conclude Q. A proof is a chain of licensed steps from assumptions to conclusion. Soundness: a sound system never proves falsehoods from true premises. Completeness: every truth (in the system's semantics) is provable — first-order logic has both; sufficiently expressive arithmetic systems, by Gödel, cannot have consistency + completeness + effective axiomatization together (Chapter 7 scopes this carefully).

# Safe Boolean evaluation with a tiny parser-free evaluator (no eval on user input).
RULES = {
    'modus_ponens': lambda p, p_imp_q: (not (p and p_imp_q)) or True,  # form is valid; truth depends on premises
}

def modus_ponens_conclusion(p: bool, p_implies_q: bool) -> bool | None:
    """Return Q's established value, or None if not established."""
    if p and p_implies_q:
        return True
    return None

print(modus_ponens_conclusion(True, True))   # True  (executed)
print(modus_ponens_conclusion(False, True))  # None: valid form, untrue premise (executed)

Chapter 3 — How proof assistants work

In Lean-style systems, propositions are types and proofs are terms of those types. You state a theorem, then build its proof with tactics (interactive commands that construct the term). At the end, a small, conservative kernel re-checks the complete proof term from scratch. Trust concentrates in: the kernel, the axioms you admitted, and your definitions. Everything else — tactic magic, AI suggestions, pretty printers — is untrusted tooling. That asymmetry is the entire value proposition: a huge, fallible search process can propose, but only a tiny checker disposes [1][2].

-- ILLUSTRATIVE Lean 4 snippet (NOT compiled in this environment).
theorem add_zero_example (n : Nat) : n + 0 = n := by
  exact Nat.add_zero n
-- The kernel, not the tactic, is the final judge.

Chapter 4 — A practical AI-to-proof pipeline

Pipeline: natural-language question → formal specification → candidate generation (model, search, or human) → proof artifact → independent kernel checking → human interpretation → documented result. Error entry points: mistranslated specification (most dangerous — everything downstream verifies the wrong thing beautifully), unsound candidate steps (kernel catches), axiom smuggling (review catches), and interpretation drift (documentation catches). The Python pattern below enforces the architectural rule: generators are untrusted functions; only the verifier's verdict is used.

def mock_generator(claim: str) -> dict:
    """Local stand-in. No model API is configured or claimed."""
    return {'claim': claim, 'certificate': {'a': 2, 'b': 3, 'total': 5}}

def verifier(cert: dict) -> bool:
    return cert['a'] + cert['b'] == cert['total']

candidate = mock_generator('2 + 3 = 5')
print(verifier(candidate['certificate']))  # True (executed pattern)

Chapter 5 — Mini verification laboratory

The interactive Proof Inspector below the article body lets you toggle premises and watch validity versus truth diverge. In Python terms the same lab evaluates Boolean expressions with a hand-written evaluator (never eval on untrusted input), checks inference rules, tests arithmetic properties over bounded ranges (testing, not proof — labelled as such), and validates or rejects small certificates. Unit tests are evidence about the tested inputs; a proof is a guarantee about all inputs in the stated domain. Confusing the two is the beginner error this chapter exists to prevent.

Chapter 6 — Verification beyond mathematics

The same architecture verifies software specifications, program invariants (“this balance never goes negative”), protocol properties, and AI-generated code against formal specs. Mechanically checkable: anything stated precisely in a decidable-enough logic over a bounded-enough model. Assumption-dependent: inputs, environments, hardware behaviour, and whether the specification deserved your trust. Article 06 develops the security side fully.

Chapter 7 — Limitations and open questions

ESTABLISHED (Gödel, scoped): any consistent, effectively axiomatized formal system expressive enough for basic arithmetic is incomplete — it contains true statements it cannot prove. This does NOT say AI (or humans) cannot reason correctly, and it does not pick out any specific practical statement as unprovable. Open problems: scaling proof discovery, shrinking trusted bases, and formalizations that provably match intent.

Conclusion: verifying an AI-generated claim means producing a formal statement, a proof artifact, and a kernel acceptance — plus a human-audited bridge between the formal statement and the claim you actually cared about. The first three are engineering; the bridge is, and remains, research.