---
id: F-008
title: Abel formula for the finite prime-reciprocal sum
tier: lean
polarity: positive
depends_on: []
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-008_prime-reciprocal-abel/lean/Research/PrimeReciprocalUpper.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/PrimeReciprocalUpper.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For every real `x≥2`, the finite reciprocal-prime sum satisfies the exact Abel
summation identity

\[
\sum_{p\le x}\frac1p
=\frac{\pi(\lfloor x\rfloor)}x
 +\int_2^x\frac{\pi(\lfloor t\rfloor)}{t^2}\,dt.
\]

Formal theorem:

```lean
theorem primeReciprocalSum_eq {x : ℝ} (hx : 2 ≤ x) :
  primeReciprocalSum x =
    (Nat.primeCounting ⌊x⌋₊ : ℝ) / x +
      ∫ t in 2..x, (Nat.primeCounting ⌊t⌋₊ : ℝ) / t ^ 2
```

## Proof / verification

Apply Mathlib's formal Abel summation formula to the prime indicator and
`f(t)=1/t`.  The cumulative indicator sum is the prime-counting function and
`f'(t)=-1/t²`; continuity away from zero discharges integrability.  Lean's
kernel accepts the proof with no `sorry`, `admit`, or axioms.  The frozen source
is `lean/Research/PrimeReciprocalUpper.lean`.
