David Ledvinka - Formalization of Brownian Motion in Lean

Stream: Lean Together 2026

[Rémy Degenne]

Discussion about the talk.

[Kevin Buzzard]

Re proving $2^{-1}+2^{-1}=1$ in ENNReal: here's an example which isn't in mathlib plus a proof which one could imagine was automatable. @David Ledvinka it would be good if you had 5 other examples of where using ENNReal was painful so that tactic writers/norm_num extenders know what ENNReal users are actually looking for.

import Mathlib

example : (6 : ENNReal)⁻¹ + 3⁻¹ = 2⁻¹ := by
  suffices ((6⁻¹ : NNReal) : ENNReal) + ((3⁻¹ : NNReal) : ENNReal) = ((2⁻¹ : NNReal) : ENNReal) by
    convert this
    all_goals simp
  norm_cast
  norm_num