Lean verification record
Checked Artifact: Taylor's Theorem with Lagrange Remainder (mathlib)
Proof Atlas collected build, no-sorry, axiom, and clean-source evidence directly from the pinned upstream declaration.
Verification result
The recorded Lean checks passed
- Build replaypassed with retained transcript
- Unfinished stepsNone found
- Source identityPinned commit and file recorded
- Dependency profileAxiom closure recorded
Reproducibility details
What the checker recorded
- Declaration checked
taylor_mean_remainder_lagrange- Module
Mathlib.Analysis.Calculus.Taylor- Source file checked
Mathlib/Analysis/Calculus/Taylor.lean- Package commit
5e932f97dd25535344f80f9dd8da3aab83df0fe6- Build transcript
- passed · retained with this record
- Unfinished proof steps
- None found by the recorded no-sorry scan
- Axiom closure
- Classical.choice, Quot.sound, propext
- Collection provenance
- Clean source state recorded
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Evidence boundary
Exact formal statement only
This page indexes Mathlib's selected Lagrange-remainder declaration for a real-valued function on ordered endpoints x₀ < x. Its exact assumptions are ContDiffOn ℝ n f (Icc x₀ x) together with DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x). It concludes that some x' strictly inside Ioo x₀ x realizes the exact finite Taylor remainder through iteratedDerivWithin (n + 1) on the same closed interval. It does not use the nearby corollary's single ContDiffOn ℝ (n + 1) hypothesis, assert uniqueness of x', handle reversed or equal endpoints, or state an analytic-series or convergence theorem.
This checker record does not establish novelty, transfer a historical acceptance decision, or authorize publication.