Italy February Round 2025 P5

On 100 lines of a notebook, Federico writes 100 numbers calculated as follows: on the $n$-th line, he writes the number of prime numbers less than or equal to $n$ if $n$ is even, and the number of positive integers less than or equal to $n$ that are not prime if $n$ is odd. Finally, he adds together all 100 numbers he has written. What result does he obtain?

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.29.0.

import Mathlib.NumberTheory.PrimeCounting

open Nat.Prime

def answer : ℤ := sorry

def f (n : ℕ) : ℤ := if Even n then π n else n - π n

theorem solution : ∑ i ∈ Finset.range 100, f i.succ = answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions

# User Time (UTC) Status
423 Iván Renison 2026-04-13T20:29 PASSED
399 nikd 2026-03-25T18:11 PASSED
396 fve5 2026-03-25T12:41 PASSED
381 FelixMP 2026-03-16T11:22 PASSED
292 kappa 2026-02-24T08:35 PASSED
291 Kitsune 2026-02-24T02:47 PASSED
290 Kitsune 2026-02-24T02:46 Compilation error
289 Kitsune 2026-02-24T02:45 Compilation error
View all