ChristianZ97/putnambench-satp-v4.27 huggingface dataset:
Problem: putnam_2025_b2
Category: analysis, geometry

Let $f: [0,1] \to [0, \infty)$ be strictly increasing and continuous.
Let $R$ be the region bounded by $x = 0$, $x = 1$, $y = 0$, and $y = f(x)$.
Let $x_1$ be the $x$-coordinate of the centroid of $R$.
Let $x_2$ be the $x$-coordinate of the centroid of the solid generated by rotating $R$ about the $x$-axis.
Prove that $x_1 < x_2$.


Lean 4 formalization:
import Mathlib

open Set Real MeasureTheory Interval

theorem putnam_2025_b2
    (f : ℝ → ℝ)
    (hf_cont : ContinuousOn f (Icc 0 1))
    (hf_mono : StrictMonoOn f (Icc 0 1))
    (hf_nonneg : ∀ x ∈ Icc (0 : ℝ) 1, 0 ≤ f x) :
    (∫ x in (0:ℝ)..1, x * f x) / (∫ x in (0:ℝ)..1, f x) <
    (∫ x in (0:ℝ)..1, x * (f x) ^ 2) / (∫ x in (0:ℝ)..1, (f x) ^ 2) := by
Problem: putnam_2025_b3
Category: number_theory

Suppose $S$ is a nonempty set of positive integers with the property that if $n$ is in $S$,
then every positive divisor of $2025^n - 15^n$ is in $S$. Must $S$ contain all positive integers?

Solution: Yes, $S$ must contain all positive integers.

Lean 4 formalization:
import Mathlib

open Finset

abbrev putnam_2025_b3_solution : Prop := sorry

theorem putnam_2025_b3 :
    putnam_2025_b3_solution ↔
    ∀ S : Set ℕ,
      S.Nonempty →
      (∀ n ∈ S, 0 < n) →
      (∀ n ∈ S, ∀ d : ℕ, 0 < d → d ∣ (2025 ^ n - 15 ^ n) → d ∈ S) →
      S = {n : ℕ | 0 < n} := by
Problem: putnam_2025_b4
Category: linear_algebra, combinatorics

For $n \geq 2$, let $A = [a_{i,j}]_{i,j=1}^n$ be an $n$-by-$n$ matrix of nonnegative integers such that:
(a) $a_{i,j} = 0$ when $i + j \leq n$;
(b) $a_{i+1,j} \in \{a_{i,j}, a_{i,j} + 1\}$ when $1 \leq i \leq n-1$ and $1 \leq j \leq n$; and
(c) $a_{i,j+1} \in \{a_{i,j}, a_{i,j} + 1\}$ when $1 \leq i \leq n$ and $1 \leq j \leq n-1$.

Let $S$ be the sum of the entries of $A$, and let $N$ be the number of nonzero entries of $A$.
Prove that $S \leq \frac{(n+2)N}{3}$.


Lean 4 formalization:
import Mathlib

open BigOperators Finset Matrix

theorem putnam_2025_b4
    (m : ℕ)
    (A : Matrix (Fin (m + 2)) (Fin (m + 2)) ℕ)
    (ha : ∀ (i j : Fin (m + 2)), (i : ℕ) + (j : ℕ) ≤ m → A i j = 0)
    (hb : ∀ (i : Fin (m + 1)) (j : Fin (m + 2)),
      A (Fin.succ i) j = A (Fin.castSucc i) j ∨
      A (Fin.succ i) j = A (Fin.castSucc i) j + 1)
    (hc : ∀ (i : Fin (m + 2)) (j : Fin (m + 1)),
      A i (Fin.succ j) = A i (Fin.castSucc j) ∨
      A i (Fin.succ j) = A i (Fin.castSucc j) + 1)
    (S : ℕ)
    (hS : S = ∑ i : Fin (m + 2), ∑ j : Fin (m + 2), A i j)
    (N : ℕ)
    (hN : N = #{p : Fin (m + 2) × Fin (m + 2) | A p.1 p.2 ≠ 0}) :
    3 * S ≤ (m + 4) * N := by
Problem: putnam_2025_b5
Category: number_theory

Let $p$ be a prime number greater than 3. For each $k \in \{1, \ldots, p-1\}$,
let $I(k) \in \{1, 2, \ldots, p-1\}$ be such that $k \cdot I(k) \equiv 1 \pmod{p}$.
Prove that the number of integers $k \in \{1, \ldots, p-2\}$ such that
$I(k+1) < I(k)$ is greater than $p/4 - 1$.


Lean 4 formalization:
import Mathlib

open Finset BigOperators

def modInv (p : ℕ) (k : ℕ) : ℕ := ZMod.val ((k : ZMod p)⁻¹)

def descentCount (p : ℕ) : ℕ :=
  #{k ∈ Finset.Icc 1 (p - 2) | modInv p (k + 1) < modInv p k}

theorem putnam_2025_b5
    (p : ℕ)
    (hp_prime : p.Prime)
    (hp_gt : 3 < p) :
    (p : ℚ) / 4 - 1 < descentCount p := by
Problem: putnam_2025_b6
Category: analysis, number_theory

Let $\mathbb{N} = \{1, 2, 3, \ldots\}$. Find the largest real constant $r$ such that
there exists a function $g: \mathbb{N} \to \mathbb{N}$ such that
$$g(n+1) - g(n) \geq (g(g(n)))^r$$
for all $n \in \mathbb{N}$.

Solution: Show that the largest possible value of $r$ is $1/4$.

Lean 4 formalization:
import Mathlib

open Real

noncomputable abbrev putnam_2025_b6_solution : ℝ := sorry

theorem putnam_2025_b6 :
    IsGreatest
      {r : ℝ | ∃ g : ℕ → ℕ, (∀ n : ℕ, 0 < n → 0 < g n) ∧
        ∀ n : ℕ, 0 < n → ((g (g n) : ℝ) ^ r) ≤ (g (n + 1) : ℝ) - (g n : ℝ)}
      putnam_2025_b6_solution := by