---

Claim. For the walk law of Problem 1166, discrete-time symmetric nearest-neighbor simple random walk on $\mathbb Z^2$ started at the origin, almost surely

$$\left|\bigcup_{k\le n}F(k)\right|=O((\log n)^2),$$

so the question has a positive answer with exponent $2$. The claim is the Lean development src/latest/ErdosProblems/Erdos1166.lean of Boris Alexeev's lean-proofs repository, added on 2026-08-23 and linked above, whose theorem erdos_1166 states that almost surely the cumulative favorite set through time $n$ has size at most $C(\log n)^2$ for all large $n$. Its docstring presents the file as the integration module for the problem. The development imports the repository's formalization of Problem 1165, linked on [[problems/analysis/E1165/claims/2024_09_02_hao_li_okada_zheng|the Hao–Li–Okada–Zheng claim page]], for the eventual bound of three on the number of favorite sites, and proves the Erdős–Taylor upper bound on the maximum local time internally; the deduction it formalizes is the one that [[problems/analysis/E1166/claims/2024_09_02_hao_li_okada_zheng|the claim page for that deduction]] records in prose.

Standing. The file names no author, informal or formal, and has no entry in the repository's list of sources, so it is recorded as an independent proof under the repository's owner rather than as a formalization of a named claimant's result; the authors key names that owner for this reason. No sorry appears in it; it has not been built or audited in this corpus, and there is no publication or outside review, so the claim stays claimed and no evidence is listed.

Depends on. Nothing in this wiki: the development carries its inputs itself.