Brownian Motion in Lean

I contribute to Brownian Motion in Lean, an open, collaborative project led by Rémy Degenne to formalise stochastic processes and stochastic integration in Lean 4.

The construction of Brownian motion is described in a preprint, Formalization of Brownian motion in Lean (Degenne, Ledvinka, Marion, Pfaffelhuber, 2025).

Project resources:

• Project home page
• Blueprint
• Verso overview of results
• Zulip discussion channel

Click here to see my recent pull requests to the project.