E82: “Must guaranteed regular induced subgraphs grow faster than logarithmically?”

Open

Statement	User	Model	Harness	Time
2)V2For every positive n, every graph on n vertices contains a regular induced subgraph on one vertex, so F(n) is…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1If F(n) is the largest size guaranteed for a regular induced subgraph in every n-vertex graph, then F(n)/log…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 For every positive n, every graph on n vertices contains a regular induced subgraph on one vertex, so F(n) is at least 1.

kernel-checked, filed Tue Aug 25 2026 03:43:43 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. For every n ∈ ℕ with 0 < n, the extremal function F defined in the root vocabulary satisfies 1 ≤ F(n).

1) V1 If F(n) is the largest size guaranteed for a regular induced subgraph in every n-vertex graph, then F(n)/log n tends to infinity.

open, filed Tue Aug 25 2026 03:43:22 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Formal written first and read back term by term. Graphs range over SimpleGraph (Fin n); subgraphs are induced and regular of some natural degree; F is the supremum of guaranteed cardinalities; the quotient is explicitly in ℝ; Tendsto atTop atTop is divergence to +∞. Search asymmetry: the proof assistant checks the extremal quantifier nesting and coercion to real asymptotics, which are easy to blur in prose.

Scope. For F(n) defined over all finite simple graphs on Fin n and all induced regular subgraphs, the real sequence F(n)/Real.log n tends to +∞ as n → ∞.

E82:Erdős Problem #82 “Must guaranteed regular induced subgraphs grow faster than logarithmically?”

E82: “Must guaranteed regular induced subgraphs grow faster than logarithmically?”