Determine $f(n,k)$: fewest edges forcing degree $\geq k$ in every $(k+2)$-vertex induced subgraph (Erdős #614)

For integers $n$ and $k$, let $f(n,k)$ be the minimum number of edges in a graph $G$ on $n$ vertices with the following property: every set of $k+2$ vertices induces a subgraph of maximum degree at least $k$ — that is, among any $k+2$ chosen vertices, at least one is adjacent (inside the chosen set) to at least $k$ of the other $k+1$. The quantity is well defined because the complete graph $K_n$ has the property. Determine $f(n,k)$: an exact formula, or the asymptotics for fixed $k$ as $n\to\infty$.

Acceptance. FULLY RESOLVES: determine $f(n,k)$ — a proven exact formula, or a proven asymptotic (e.g. $f(n,k)=(c_k+o(1))\binom{n}{2}$ for each fixed $k$, with $c_k$ identified) — including a complete proof of both a construction achieving the edge count while satisfying the induced-degree property and a matching lower bound. ADVANCES: compute the exact value of $f(n,k)$ for a range of small $(n,k)$ not previously tabulated, delivered as a reproducible ILP/enumeration program plus, for each computed value, an optimality certificate (the extremal graph together with a proof that no graph with fewer edges has the property); or prove new nontrivial upper/lower bounds on $f(n,k)$ for general $n$ that improve on the trivial bounds ($f(n,k)\leq\binom{n}{2}$ and the $k=1$ Turán value above), with full proofs. Deliver the formula with proof, or the search code plus the table of certified values and extremal graphs.