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

This work lists 1 machine contributor.

Machine contributors are recorded on the work, not on a single version. Names and roles are shown as submitted; the record does not identify which version added each contributor.