primeCounting_thirty
plain-language theorem explainer
The theorem states that the prime counting function evaluates to exactly 10 at input 30. Number theorists verifying explicit small values of π(n) in arithmetic function libraries would cite this result. Its proof is a direct native decision that evaluates the equality from the delegated definition without manual expansion.
Claim. $π(30) = 10$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The prime counting function is defined as π(n) = #{p ≤ n : p prime}, directly delegating to Nat.primeCounting. This sits in the NumberTheory.Primes.ArithmeticFunctions section, providing basic interfaces before deeper Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality.
why it matters
This concrete evaluation supports verification of the prime counting function within the arithmetic functions module. It fills the specific instance check for π(30) noted in the declaration comment. No downstream uses are recorded, leaving it as an isolated verification point in the number theory scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.