---

Claim. Let $G(n,M)$ be uniform on the labeled simple graphs with $n$ vertices and $M$ edges, let $L_i$ be the number of vertices of its $i$-th largest component, and for an edge sequence $M_n$ put $\lambda_n=2M_n/n$ and $a(x)=x-1-\log x$. The development's principal theorem is a five-regime atlas of the sparse evolution. Fixed subcritical and supercritical: for $\lambda_n\to\lambda\in(0,\infty)\setminus\{1\}$, $L_2-(\log n-\tfrac52\log\log n)/a(\lambda_n)=O_{\mathbb P}(1)$, with an explicit lattice limit law along subsequences, and for $\lambda>1$ the largest component has $n(1-x(\lambda_n)/\lambda_n)+O_{\mathbb P}(\sqrt n)$ vertices, where $x(\lambda)\in(0,1)$ solves $xe^{-x}=\lambda e^{-\lambda}$, and is with high probability the only component of order at least $n^{2/3}$. Barely subcritical and supercritical: for $\lambda_n=1\mp\varepsilon_n$ with $\varepsilon_n\to0$ and $n\varepsilon_n^3\to\infty$, $L_2$ has an exact-rate threshold law with scale $1/a(\lambda_n)$ in place of the quadratic normalization, and in the supercritical case the giant component has $2n\varepsilon_n+O(n\varepsilon_n^2)+O_{\mathbb P}(\sqrt{n/\varepsilon_n})$ vertices, with one absolute constant in the deterministic error term. Critical: for every fixed real $\lambda$ and $(2M_n-n)/n^{2/3}\to\lambda$, the vector $n^{-2/3}(L_1,\ldots,L_k)$ converges in distribution, for each fixed $k$, to the ranked excursion lengths of $B(t)+\lambda t-t^2/2$ above its running minimum, Aldous's limit; the second length is finite and positive almost surely, so $L_2$ has order $n^{2/3}$ in probability in the critical window. The development states this for the uniform model; the problem Problem 745 fixes the binomial model with edge probability $1/n$, whose edge count is concentrated at $n/2$ within $O_{\mathbb P}(\sqrt n)$, inside the critical regime with $\lambda=0$, and Erdős's 1981 paper poses the question for the uniform model with $k$ edges as $k$ varies. The passage from the uniform model to the binomial one is not part of the development. The result describes the size of the second largest component at the asked parameter and throughout the sparse evolution, which is what the problem asks for, so the claim's value is solved; it agrees with Boris Alexeev's development on the claim page that Erdős's expectation of an order about $\log n$ holds away from the critical point and fails at it.

Claimant. The development was posted on the site's discussion thread on 4 October 2026 by an account of the SpringSense Innovation Institute, as a completed auto-formalization of the problem; its formalization.yaml and README, at the pinned commit, name Jingxuan Ding of the institute as the formalization's author and responsible maintainer. The post and the README say that the Lean proofs were produced by AI agents through MathMiner, an auto-formalization framework developed during the project, and the post names GPT-5.6 Sol with high thinking effort as the primary model; the formalization.yaml records the method as agent orchestration through MathMiner and says that the model identities of the proof runs are not established in its archive. The development lists Erdős and Rényi 1960 and Pittel 1990 as background and Łuczak 1990 and Aldous 1997 as sources it adapts; it declares itself a formalization of no single claimant's result, so it is an independent proof with its own page. Its principal theorem is Erdos745.Palomar.sparseEvolution in Solution.lean, a direct bridge to Erdos745.WrapUp.atlas; the public statement is Challenge.lean, which imports only Mathlib and carries one deliberate sorry as the statement placeholder, and the prose statement is docs/STATEMENT.md (FINAL-01 to FINAL-05). The development's own scope note says that the atlas is pointwise in the edge sequence, is no theorem about the whole graph process at once, and in the critical window claims finite-rank convergence at continuity points rather than the full $\ell^2$ limit; its formalization.yaml reports no sorry in the proof closure and the axioms propext, Classical.choice and Quot.sound, with the review status self-assessed and no independent human review claimed.

Depends on. Nothing in this wiki.

Standing. Claimed: this corpus has not built, audited or kernel-checked the development, so no evidence is listed; the development's own records claim no independent review or acceptance; 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 critical-window order $n^{2/3}$ agrees with Erdős and Rényi's 1960 statement for the largest component at $N\sim n/2$, with Alexeev's development and with the refereed limit law of Aldous 1997, the accepted full claim on which the problem's standing rests and the source the development cites for its critical window. This page would become accepted if the development were built and audited.