The nth Harmonic number is not an integer. We formalize the proof using 2-adic valuations. This proof is due to Kürschák.

Reference: https://kconrad.math.uconn.edu/blurbs/gradnumthy/padicharmonicsum.pdf

theorem harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n

theorem padicValRat_two_harmonic (n : ℕ) : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)

The 2-adic valuation of the n-th harmonic number is the negative of the logarithm of n.

theorem padicNorm_two_harmonic {n : ℕ} (hn : n ≠ 0) : ‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n

The 2-adic norm of the n-th harmonic number is 2 raised to the logarithm of n in base 2.

theorem harmonic_not_int {n : ℕ} (h : 2 ≤ n) : ¬(harmonic n).isInt = true

The n-th harmonic number is not an integer for n ≥ 2.