Balanced prime conjecture

References:

• Wikipedia
• OEIS A6562

theorem BalancedPrimes.balanced_primes : sorry ↔ {n : ℕ | Prime ((Nat.nth Prime n + Nat.nth Prime (n + 2)) / 2)}.Infinite

Let $p_k$ be the $k$-th prime number. Are there infinitely many $n$ such that $(p_n + p_{n+2}) / 2$ is prime?

theorem BalancedPrimes.balanced_primes_order : sorry ↔ ∀ k > 0, {n : ℕ | k ≤ n ∧ 2 * k * Nat.nth Prime n = ∑ i ∈ Finset.Ioc 0 k, (Nat.nth Prime (n - i) + Nat.nth Prime (n + i))}.Infinite

Let $p_k$ be the $k$-th prime number. Are there infinitely many $n$ such that $p_n = \dfrac{\sum_{i = 1} ^ k p_{n - i} + p_{n + i}}{2*k}$?