$\theta(p_c)=0$ for Bernoulli bond percolation on $\mathbb{Z}^d$ in all dimensions $d\ge 2$: a guide to the Lean formalization

Every version keeps its own PDF, citation, and review record — endorsements are bound to the version they examined and never carry forward silently.