Random networks hide a real shortcut in their structure
- What it is
- The paper claims a quantified gap between two ways of grouping a random network, with a linked formalization of one consequence.
- Who did it
- Samuil Petkov
- What it could mean
- Let groups be fully connected or fully disconnected, and a random network can be organized more economically. This claim would put a precise lower bound on how large that advantage becomes.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A Full-Sequence Quantitative Gap Between the Chromatic and Cochromatic Numbers of a Random Graph ↗See the proposed checks
Clone the pinned formal commit; rebuild under its pinned Lean/Mathlib toolchain; inspect the theorem statement and axiom examination; then separately map the manuscript's signed-overlap/second-moment derivation to the formal theorem hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The manuscript claims to resolve Erdős and Gimbel's question by showing, along the full sequence for (Gn ∼ G(n,1/2)), that (χ(Gn)-ζ(Gn)) exceeds an explicit positive multiple of (n/(log n)³) with probability tending to one. It is unusually timely because the author supplies a Lean 4 formalization of the explicit full-sequence lower-bound consequence and a public replay archive, while disclosing AI-assisted development.
- Why this could matter
- Random networks hide a real shortcut in their structure A random network can be grouped more efficiently when groups may be either fully connected or fully disconnected than when only independent groups are allowed. The paper quantifies that advantage at scale.
- If it holds up
- Foundational: it resolves an Erdős–Gimbel question and gives researchers a sharper baseline for random-graph partitioning and average-case combinatorial optimization.
- If it does not
- The claimed full-sequence gap is not established; the failure would identify where a probabilistic or formally encoded bound overreaches.
- Impact horizon
- Foundational · Random networks · Graph partitioning · Probability
- Version
- submitted 2026-08-31 11:18:17 UTC
- Why we tracked it
- a current claimed resolution of Erdős–Gimbel Problem 625 with a narrowly scoped, version-pinned Lean 4 statement and public clean-replay record. The source lock and formal-artifact scope are sufficient to prepare a docket; neither settles the manuscript-only phase-refinement claims.
- Highest-risk dependency
- Kernel checking establishes only the encoded formal statement relative to the stated Lean trust base. The load-bearing issue for the paper is whether the formal statement faithfully captures all hypotheses and whether the manuscript-only phase-resolved refinement follows from the written probability argument.
- Available artifacts
- The source cites the exact Lean/replay archive revision, whose recorded formal-source commit is 824e4b609466d2e26b216a76ecf103184dac2663. The archive exposes Lean sources, axiom examination, checksums, logs, and a clean-environment replay. The manuscript explicitly limits the formalization to the stated full-sequence coefficient, not its phase-resolved refinement.
- Current boundary
- Intake record only; examination not started.