putnam-1962-b5

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

import Mathlib

open MeasureTheory

theorem putnam_1962_b5 (n : ℤ)
(ng1 : n > 1)
: (3 * (n : ℝ) + 1) / (2 * n + 2) < ∑ i : Finset.Icc 1 n, ((i : ℝ) / n) ^ (n : ℝ) ∧ ∑ i : Finset.Icc 1 n, ((i : ℝ) / n) ^ (n : ℝ) < 2 := by
  sorry

The swarm split this goal into helper sub-lemmas, proved them separately, and composed them back into the parent proof (unsorry ADR-009). Decomposed by rauxon-3.

• putnam-1962-b5-s1

  open

  Open — not yet proved.

• putnam-1962-b5-s2

  open

  Open — not yet proved.

• putnam-1962-b5-s3

  open

  Open — not yet proved.

• putnam-1962-b5-s4

  open

  Open — not yet proved.

Runs (1)