---

Claim. The theorem erdos_1164 of the Lean development linked above states that for every $\varepsilon>0$ there are $0<a\le b$ such that for all large $n$, $\mathbb P(\log R_n<a\sqrt{\log n})<\varepsilon$ and $\mathbb P(\log R_n>b\sqrt{\log n})<\varepsilon$. Here $R_n$ is the largest $r$ whose closed lattice disc $x_1^2+x_2^2\le r^2$ planar simple random walk started at the origin has visited by time $n$, and Lean's convention $\log0=0$ applies; the file's module comment says that its lower-tail theorem controls the event $R_n=0$ explicitly. This is the corrected Statement of Problem 1164, the order of $\log R_n$ in probability for the pathwise radius. The module comment says that the development proves the order and not the sharp limit law of Dembo, Peres, Rosen and Zeitouni. The file was added to Boris Alexeev's repository of Lean proofs of Erdős problems on 2026-08-26 and is linked at the commit that holds it.

Standing. The file and its documentation page name no author, and the repository's source list has no entry for it, so the claim is recorded under the name on the commit that added it (Boris Alexeev, 2026-08-26). A text scan of its modules finds no sorry, admit or axiom, but no outside reviewer has examined it and this corpus has not built or audited it, so it carries no formalized evidence and stays claimed. The site does not mention it, and the community database at teorth/erdosproblems lists the problem as not formalized.

Depends on. No page of this wiki.