---

Claim. Let each edge of a graph on $n$ vertices be present independently with probability $\lambda/n$ for a fixed $\lambda>0$, and let $L_2$ be the number of vertices of its second largest component. At $\lambda=1$, the parameter of Problem 745, $L_2=\Theta_{\mathbb P}(n^{2/3})$: for every $\varepsilon>0$ there are $0<c<C$ and $N$ such that $cn^{2/3}\le L_2\le Cn^{2/3}$ with probability at least $1-\varepsilon$ for all $n\ge N$. For every fixed $\lambda\ne1$, $L_2$ has logarithmic order with high probability, and $L_2/\log n\to(\lambda-1-\log\lambda)^{-1}$ in probability. This is a description of the size of the second largest component at $p=1/n$, which is what the problem asks for, so the claim's value is solved; it also says that Erdős's expectation of an order about $\log n$ holds for fixed $\lambda\ne1$ and fails at $\lambda=1$.

Claimant. Boris Alexeev posted the result on the site's discussion thread on 25 August 2026, writing that they had formalized it, that the source [KSS80] the site credits assumes $\lambda>1$ strictly, and that the problem should perhaps say disproved. The Lean development in their repository of formalized Erdős problems, linked above at a pinned commit, was committed to the repository's main branch on 26 August 2026 (UTC) and strengthened on 27 August 2026. The file src/latest/ErdosProblems/Erdos745.lean, at the pinned commit, has no authors block and names no informal author and no AI system; its note ErdosProblems/Erdos745.md calls it a formalized proof of Erdős Problem 745 for Mathlib v4.33.0. Its theorems are erdos745_supercritical (the upper bound $A\log n$ with high probability for $1<\lambda$ and $A>1/(\lambda-1-\log\lambda)$, which its docstring calls the corrected KSS logarithmic upper bound), erdos745_critical (the $n^{2/3}$ order at $\lambda=1$), erdos745_noncritical_asymptotic (the limit of $L_2/\log n$ for fixed $\lambda\ne1$) and erdos745, the conjunction of the supercritical and critical statements; the module folder Erdos745/ holds thirteen files (Model, Components, Moments, PairRatio, EdgeLaw, TreeComponents, Prufer, TreeCounting, TreeMoments, CriticalLower, CriticalUpper, MacroscopicUniqueness, Noncritical). The file has no #print axioms line and contains no sorry. It names no claimant whose result it formalizes, so it is an independent proof with its own page, not a link on the page of [KSS80].

Depends on. Nothing in this wiki.

Standing. Claimed: this corpus has not built, audited or kernel-checked the development, so no evidence is listed; at the search recorded on the problem page, the site's label PROVED, which credits [KSS80], was unchanged, and neither the site's page nor the community database cited the development; the claim is not refereed. The order $n^{2/3}$ at $\lambda=1$ agrees with Erdős and Rényi's 1960 statement for the largest component at $N\sim n/2$ and with the refereed limit law of Aldous 1997, the accepted full claim on which the problem's standing rests. This page would become accepted if the development were built and audited.