Budgeted Local Formal Verification for AI-Assisted PDE Research

English abstract A checked formal proof establishes a formal statement, but does not by itself establish that the statement matches its intended use in a PDE manuscript. Research-level analysis also contains external analytic inputs, parameter-sensitive claims, and proofs that change during revision. We study budgeted local formal verifi- cation: choosing where to verify and at what mathematical granularity so that independent researchers can determine what a result proves, assumes, and supports. Our method schedules verification units using their interfaces, downstream relevance, and measured formalization, semantic-review, and replay costs. Each unit binds a manuscript claim to a fixed Lean target, explicit external inputs, definitions, and versions. Checked evidence retains its unresolved premises; revisions trigger revalidation of affected uses while preserving unaf- fected alternative proofs. We design evaluations combining valid controls, documented research mismatches, and labeled interventions involving quantifiers, function spaces, comparison objects, and stale dependencies. All methods share the same trusted targets and final proof-checking safeguards. The central evaluation com- pares valid evidence retained, incorrect claims accepted, and independent verification cost across budgets. The contribution is not the use of Lean for short proofs, but a testable allocation mechanism for making partial formalization useful, reproducible, and explicit about its support boundaries in mathematical research.