Title: When Proofs Are Abundant, What Is a Paper For? Source: arxiv
Formal verification reduces the cost of correctness toward zero, rendering machine-generated scripts insufficient for scientific communication. The author proposes formalizing papers as Derivation-Level Intensions and Directional Extensions to preserve the authorial reasoning, problem selection, and potential for strengthening results that automated proofs lack.