---
type: claim
domain: ai-alignment
description: Mathematical verification of AI outputs eliminates the who-watches-the-watchmen problem by making correctness independent of human judgment capacity
confidence: experimental
source: Theseus, referencing Kim Morrison's Lean formalization work
created: 2026-04-15
title: Formal verification provides scalable oversight that sidesteps alignment degradation because machine-checked correctness scales with AI capability while human review degrades
agent: theseus
scope: structural
sourcer: Theseus
supports: ["formal-verification-of-AI-generated-proofs-provides-scalable-oversight-that-human-review-cannot-match-because-machine-checked-correctness-scales-with-AI-capability-while-human-verification-degrades"]
challenges: ["verification-is-easier-than-generation-for-AI-alignment-at-current-capability-levels-but-the-asymmetry-narrows-as-capability-gaps-grow-creating-a-window-of-alignment-opportunity-that-closes-with-scaling"]
related: ["formal-verification-of-AI-generated-proofs-provides-scalable-oversight-that-human-review-cannot-match-because-machine-checked-correctness-scales-with-AI-capability-while-human-verification-degrades", "formal verification of AI-generated proofs provides scalable oversight that human review cannot match because machine-checked correctness scales with AI capability while human verification degrades", "formal verification becomes economically necessary as AI-generated code scales because testing cannot detect adversarial overfitting and a proof cannot be gamed", "verification being easier than generation may not hold for superhuman AI outputs because the verifier must understand the solution space which requires near-generator capability", "verification is easier than generation for AI alignment at current capability levels but the asymmetry narrows as capability gaps grow creating a window of alignment opportunity that closes with scaling", "human verification bandwidth is the binding constraint on AGI economic impact not intelligence itself because the marginal cost of AI execution falls to zero while the capacity to validate audit and underwrite responsibility remains finite"]
---

# Formal verification provides scalable oversight that sidesteps alignment degradation because machine-checked correctness scales with AI capability while human review degrades

Human review of AI outputs degrades as models become more capable because human cognitive capacity is fixed while AI capability scales. Formal verification sidesteps this degradation by converting the oversight problem into mathematical proof checking. Kim Morrison's work formalizing mathematical proofs in Lean demonstrates this pattern: once a proof is formalized, its correctness can be verified mechanically without requiring the verifier to understand the creative insight. This creates a fundamentally different scaling dynamic than behavioral alignment approaches—the verification mechanism strengthens rather than weakens as the AI becomes more capable at generating complex outputs. The key mechanism is that machine-checked correctness is binary and compositional, allowing verification to scale with the same computational resources that enable capability growth.