pith. sign in

arxiv: 2606.15089 · v2 · pith:MGTTKFISnew · submitted 2026-06-13 · 💱 q-fin.MF · math.PR

A Machine-Checked It\^o Calculus for Brownian Motion

Raphael Coelho This is my paper

Pith reviewed 2026-06-30 11:31 UTC · model grok-4.3

classification 💱 q-fin.MF math.PR
keywords Itô integralItô's formulaBrownian motionLean 4machine-checked prooflocal martingalequadratic variationstochastic calculus
0
0 comments X

The pith

The Itô integral is realized inside Lean 4 as a continuous local martingale on the half-line together with Itô's formula for C3 functions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs the Itô integral for Brownian motion on a bounded interval as a Hilbert-space isometry that begins with simple adapted processes and yields a continuous L2 martingale. A single structural fact drives the argument: the value of the integral at each time equals the conditional expectation of its terminal value onto the filtration at that time, from which adaptedness, the martingale property, and both isometries follow at once. Itô's formula is obtained for C3 functions with bounded derivatives by passing from discrete quadratic variation to the continuous case with explicit L2 remainder estimates. The L2 object is then lifted to an almost-surely continuous modification that is a local martingale for the null-augmented filtration, and these pieces are glued to produce the integral on the entire non-negative line.

Core claim

On a bounded interval the Itô integral is realized as the continuous L2 martingale whose value at each time is the projection of its terminal value onto the filtration at that time; this identity yields the martingale property and both isometries as immediate consequences. Itô's formula for C3 functions follows from a discrete approximation argument with explicit L2 error bounds. The resulting process admits an almost-surely continuous modification that is a local martingale with respect to the null-augmented filtration, and these bounded-horizon pieces glue to give the integral on the half-line.

What carries the argument

The conditional-expectation projection identity that defines the integral process at each time t from its terminal value.

If this is right

  • Adaptedness and the martingale property follow directly from the projection identity.
  • The integral satisfies both the terminal and time-indexed Itô isometries.
  • Itô's formula holds in both time-independent and time-dependent forms with explicit remainder terms.
  • A continuous modification exists that is a local martingale on the positive reals.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The separation of the L2 theory from the pathwise theory may simplify formalizations of related stochastic objects.
  • Similar projection identities could be used to verify other classical results in stochastic calculus inside proof assistants.
  • The bounded-horizon construction suggests a modular route for extending the formalization to longer time intervals or different integrators.

Load-bearing premise

The development assumes the correctness of the supplied definitions and properties of Brownian motion and its filtration from the existing Lean packages.

What would settle it

If the Lean proof script fails to type-check or if an explicit counterexample to one of the stated theorems is found within the bounded interval and C3 class.

Figures

Figures reproduced from arXiv: 2606.15089 by Raphael Coelho.

Figure 1
Figure 1. Figure 1: Proof architecture. The isometry layer (top) builds the integral and the process; the [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗
read the original abstract

We develop the It\^o calculus of Brownian motion, machine-checked in Lean~4 over Mathlib and the \lean{BrownianMotion} package. On a bounded interval $[0,T]$ the It\^o integral is built as a Hilbert-space isometry, from a predictable-rectangle $\pi$-system through the density of simple adapted processes. Realized as a process, it is a continuous $L^2$ martingale. One structural identity drives this: the integral at time $t$ is the conditional-expectation projection of its terminal value onto $\F_t$, and from it adaptedness, the martingale property, the contraction bound, and both the terminal and time-indexed It\^o isometries follow as corollaries. On this integral we prove It\^o's formula for $C^3$ functions with bounded derivatives, including the time-dependent form $df = f_x\,dB + (f_t + \tfrac12 f_{xx})\,dt$, by a discrete-to-continuous argument through weighted quadratic variation with explicit $L^2$ remainder bounds. We then pass from the $L^2$ theory to the pathwise. The integral process has an almost-surely continuous modification, and its everywhere-continuous representative is a local martingale for the null-augmented Brownian filtration; gluing the bounded-horizon representatives along the half-line yields the It\^o integral as a continuous local martingale on all of $\R_{\ge 0}$, the form it takes in the classical theory. To our knowledge these are the first machine-checked constructions of the It\^o integral and of It\^o's formula in any proof assistant, and the first to reach a pathwise-continuous local martingale. The boundary is explicit. The $L^2$ integral and It\^o's formula are developed on $[0,T]$ with bounded-derivative integrands; the unrestricted $C^2$ formula, integrators beyond brownian motion, and right-continuity of the filtration lie outside the development.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper develops the Itô calculus for Brownian motion, machine-checked in Lean 4 over Mathlib and the BrownianMotion package. On [0,T] the Itô integral is constructed as an L² isometry from predictable rectangles via density of simple adapted processes, realized as a continuous L² martingale whose properties (adaptedness, martingale property, isometries) follow from a single structural projection identity. Itô's formula for C³ functions with bounded derivatives (including the time-dependent form) is proved via a discrete-to-continuous argument with explicit L² remainder bounds. The development then passes to the pathwise setting: an a.s. continuous modification exists, the everywhere-continuous version is a local martingale on the null-augmented filtration, and gluing yields the continuous local-martingale form on ℝ≥0.

Significance. If the result holds, this is a significant contribution as the first machine-checked constructions of the Itô integral and Itô's formula in any proof assistant, and the first to reach a pathwise-continuous local martingale. The fully machine-checked Lean proofs, the clean structural projection identity that yields multiple properties as corollaries, the explicit L² remainder bounds, and the explicit scope boundaries (bounded interval, bounded-derivative integrands, Brownian motion only) are notable strengths. Reliance on pre-existing definitions from Mathlib and the BrownianMotion package is standard and does not introduce unverified gaps.

minor comments (2)
  1. The abstract and introduction both state that these are 'the first' machine-checked constructions; a brief comparison paragraph citing the closest prior formalizations (even if they stop short of pathwise continuity) would strengthen the novelty claim.
  2. Notation for the filtration (ℱ_t) and the null-augmented version is introduced without an explicit forward reference to the package definitions; a one-sentence pointer in §2 would aid readers unfamiliar with the BrownianMotion library.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and positive evaluation of the manuscript. We are pleased that the contribution is viewed as significant and that the recommendation is to accept.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper constructs the Itô integral and Itô's formula as formal Lean 4 proofs over the pre-existing BrownianMotion package and Mathlib definitions of Brownian motion and filtration. All steps (Hilbert-space isometry via predictable rectangles and density, discrete-to-continuous argument with explicit remainder bounds, passage to pathwise continuous local martingale via modification and gluing) are derived inside the proof assistant from library primitives; no parameter fitting, self-referential equations, or load-bearing self-citations appear. Reliance on external library definitions is standard for formalizations and does not reduce the claimed results to the inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work is a formalization of classical results; it introduces no new free parameters, invented entities, or ad-hoc axioms beyond the standard mathematical axioms already present in Mathlib.

axioms (1)
  • standard math Standard axioms of real analysis, measure theory, and conditional expectation as formalized in Mathlib
    Invoked throughout the construction of the integral and the martingale properties.

pith-pipeline@v0.9.1-grok · 5913 in / 1214 out tokens · 43064 ms · 2026-06-30T11:31:10.249976+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. The Fundamental Theorem of Asset Pricing, Formalized in Lean 4

    q-fin.MF 2026-06 accept novelty 9.0 full

    First machine-checked formalization of the FTAP in Lean 4 across three settings, with explicit EMM construction via minimization of E[log(1+e<θ,Y>)] in the d-asset case.

  2. A Formally Verified Library of Mathematical Finance in Lean 4

    q-fin.MF 2026-05 accept novelty 8.0 full

    A Lean 4 library formalizes over 200 sorry-free theorems in mathematical finance, constructs the L² Itô integral as a bounded linear isometry, derives the risk-neutral pricing measure, and enforces an axiom-usage audit.

  3. A Formally Verified Library of Mathematical Finance in Lean 4

    q-fin.MF 2026-05 accept novelty 7.0 full

    A Lean 4 library with 200+ sorry-free theorems formalizes mathematical finance including the L2 Itô integral and derived risk-neutral measure, plus a faithfulness audit.

Reference graph

Works this paper leans on

10 extracted references · 3 canonical work pages · cited by 2 Pith papers · 1 internal anchor

  1. [1]

    Avigad, J

    J. Avigad, J. Hölzl, L. Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389–423, 2017

    2017

  2. [2]

    Degenne et al.brownian-motion: a Lean 4 development of Brownian motion

    R. Degenne et al.brownian-motion: a Lean 4 development of Brownian motion. https:// github.com/RemyDegenne/brownian-motion, 2024–2026. Consumed at commit eaa4391

    2024

  3. [3]

    Degenne, D

    R. Degenne, D. Ledvinka, E. Marion, P . Pfaffelhuber. Formalization of Brownian motion in Lean. arXiv:2511.20118, 2025

    work page arXiv 2025

  4. [4]

    Echenim, H

    M. Echenim, H. Guiol, N. Peltier. Formalizing the Cox–Ross–Rubinstein pricing of European derivatives in Isabelle/HOL.Journal of Automated Reasoning, 64:737–765, 2020

    2020

  5. [5]

    R. Coelho. A formally verified library of mathematical finance in Lean 4. arXiv:2606.01356, 2026

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  6. [6]

    K. Itô. Stochastic integral.Proceedings of the Imperial Academy, T okyo, 20(8):519–524, 1944

    1944

  7. [7]

    Karatzas, S

    I. Karatzas, S. E. Shreve.Brownian Motion and Stochastic Calculus, 2nd ed. Springer, 1991

    1991

  8. [8]

    A. Keskin. A formalization of martingales in Isabelle/HOL. arXiv:2311.06188, 2023

    work page arXiv 2023

  9. [9]

    de Moura, S

    L. de Moura, S. Ullrich. The Lean 4 theorem prover and programming language. In CADE 28, LNCS 12699, pp. 625–635, 2021. 15

    2021

  10. [10]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. InCPP 2020, pp. 367–381, 2020. 16

    2020