Claims

../

2024_09_02_hao_li_okada_zheng: The eventual bound of three on planar favorite sites, with the Erdős–Taylor maximum-local-time estimate, gives almost surely O((log n)^2) sites ever favorite by time n; refereed inputs, the deduction itself unpublished.

2026_08_23_alexeev: A Lean development in Boris Alexeev's lean-proofs repository proves that almost surely the sites ever favorite by time n number O((log n)^2), from the repository's Problem 1165 formalization; unbuilt here, unreviewed.

---