Harmonic functions of Brownian motion ($u(B_{t\wedge \tau })\text{ is a local martingale if }\Delta u=0$)

For a $C^2$ harmonic function $u$ and Brownian motion stopped before leaving its domain, Itô formula gives $du(B_t)=\nabla u(B_t)\cdot d{B}_t+\frac{1}{2}\Delta u(B_t)dt$. The drift vanishes. On a compact subdomain, the stopped process is a bounded martingale. Optional stopping theorem at an almost-surely finite exit time therefore gives the boundary mean formula. At the centre of a disk, rotational invariance of planar Brownian motion makes the exit law uniform on the boundary circle. This proves the mean value property for harmonic functions probabilistically.