MAReason: Adaptive Retrieval and Deep Proof Planning for Mathematical Analysis in Lean 4

Formal theorem proving in mathematical analysis requires finding relevant results in Mathlib, Lean's mathematical library, and connecting them into a complete argument. Language-model provers can invoke unavailable library facts or fail to turn relevant premises into a complete proof. We present MAReason, which uses Lean verification to trigger escalation around a fixed OProver-8B. It first strengthens the premise context for whole-proof generation. Persistent verification failure triggers a change in proof granularity to independently grounded and verified obligations, followed by final composition and Lean verification. MAReason-Corpus provides domain-specific, Lean-verified supervision with benchmark-overlap removal. We evaluate on MA-ProofBench's 200 problems, comprising undergraduate analysis (Level I) and Ph.D.-qualifying analysis (Level II). With eight candidates per retrieval stage and eight Deep search trajectories, MAReason raises Pass@8 from 4% to 19% on Level I and from 1% to 4% on Level II relative to direct OProver-8B, using additional staged search. Mathlib hallucination fractions among failed candidates fall from 54.6% to 49.9% on Level I and from 39.0% to 35.9% on Level II. In a separate study, domain adaptation with MAReason-Corpus improves Level I performance on the base model but solves no Level II problems. These results support domain adaptation for easier analysis proofs and verified proof planning for harder obligations.