theorem
proved
term proof
primeCounting_three
show as:
view Lean formalization →
formal statement (Lean)
366theorem primeCounting_three : primeCounting 3 = 2 := by
proof body
Term-mode proof.
367 native_decide
368
369/-- π(5) = 3. -/