Fixed statements for 15 problems.

[logical-ivan]

putnam_1963_a6:

• Renamed hypothesis: (hM : M = midpoint ℝ U V) → (hMuv : M = midpoint ℝ U V) - Avoids name shadowing with the later hypothesis hM : M ∈ segment ℝ A B ∧ M ∈ segment ℝ C D
• Added (hAC : A ≠ C) - Required for line AC to be well-defined (P is the intersection of lines AC and UV)
• Added (hBD : B ≠ D) - Required for line BD to be well-defined (Q is the intersection of lines BD and UV)
• Fixed typo in hQ: Collinear ℝ {P, B, D} → Collinear ℝ {Q, B, D} - The hypothesis should state that Q (not P) is collinear with B and D

putnam_1964_b4:

• Added (hCinj : Function.Injective C) - Ensures the n circles are distinct.
• The problem statement says "n great circles" which implicitly assumes n different circles, but the original formalization allowed duplicates.

putnam_1977_a2

• Repositioned nonzero hypotheses - Changed from ∀ a b c d, solution ↔ (a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → equations) to ∀ a b c d, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (solution ↔ equations).
• The original was logically incorrect: when variable a equals to 0, the implication becomes vacuously true (False → ...), making the statement claim that (0,b,c,d) satisfies the solution predicate.
• The corrected version properly restricts to the nonzero domain where divisions are well-defined.

putnam_1977_b6:

• Added [Finite H] constraint - The problem states "a subgroup of G with h elements" which implicitly assumes H is finite.
• Without this constraint, h = Nat.card H doesn't properly capture the cardinality (since Nat.card of infinite types is 0), and the bound 3*h^2 becomes meaningless.

putnam_1980_a4:

• Added negation: ¬(a = 0 ∧ b = 0 ∧ c = 0) - The problem requires integers "not all zero", but the original formalization said (a = 0 ∧ b = 0 ∧ c = 0) which is the opposite condition.

putnam_1989_b6:

• Fixed function evaluation in Riemann sum: f (i + 1) → f (x i.succ) - The problem defines the Riemann sum as $\sum_{i=0}^n (x_{i+1}-x_i)f(x_{i+1})$, where $f$ is evaluated at the partition point value $x_{i+1}$.
• The original formalization incorrectly evaluated f (i + 1), passing the index i+1 (a natural number) to a function f : ℝ → ℝ that expects a real number. This is mathematically nonsensical - the function should be evaluated at the actual partition point value x i.succ, not at the index.
• Without this fix, the Riemann sum definition doesn't match the problem.

putnam_1997_a5:

• Removed monotonicity constraint: (∀ i j : Fin n, i < j → t i <= t j) ∧ removed from the definition of N - The problem asks for the number of ordered n-tuples $(a_1, a_2, \ldots, a_n)$ such that $1/a_1 + 1/a_2 + \ldots + 1/a_n = 1$.
• The word "ordered" means we count each arrangement separately. The original formalization incorrectly added a constraint requiring the tuple to be sorted (non-decreasing), which would only count each set of values once in sorted order, not all possible orderings.

putnam_1999_b3:

• Added explicit type casts: 1/2 ≤ m/n → (1 : ℝ)/2 ≤ (m : ℝ)/n and m/n ≤ 2 → (m : ℝ)/n ≤ 2 - The problem requires checking if the ratio $m/n$ falls within $[1/2, 2]$ where $m, n$ are positive integers.
• Without explicit type annotations, Lean could interpret m/n as natural number division (which truncates), giving wrong results - e.g., 3/4 would equal 0 instead of 0.75. The explicit casts force division in the real numbers, ensuring the condition matches the mathematical meaning

putnam_2003_a5:

• Fixed typo in return condition: (∀ k ∈ Ioc i j, p i = -1) → (∀ k ∈ Ioc i j, p k = -1) - A return in a Dyck path is a maximal sequence of contiguous downsteps. The condition should check that each step p k in the interval (i, j] equals -1.
• The original incorrectly wrote p i = -1, checking the same fixed value for all indices k - nonsensical. The corrected version properly checks that each step in the interval is a downstep.

putnam_2003_a6:

• Fixed type error: A ∪ B = ℕ → A ∪ B = (Set.univ : Set ℕ) - The problem asks whether we can partition the nonnegative integers into two sets $A$ and $B$.
• The original wrote A ∪ B = ℕ, but in Lean 4's type theory, ℕ is the type of natural numbers, not a set. The union A ∪ B has type Set ℕ, so we need to compare it with Set.univ : Set ℕ (the universal set of all natural numbers) for the statement to be well-typed.

putnam_2003_b5:

• Added non-degeneracy constraint: ∧ dist A B ≠ 0 - The problem states "$A, B$, and $C$ be equidistant points on the circumference" which implicitly means three distinct points forming an equilateral triangle.
• Without this constraint, the original conditions dist A B = dist A C ∧ dist A B = dist B C are satisfied when A = B = C (all three points coincide at the same location on the circle).
• In this degenerate case, for any interior point P, the constructed triangle would have all three sides equal to dist P A. But dist P A depends on both the distance ‖P‖ from the origin and P's angular direction. For example, with A = (1, 0), the point P = (0.5, 0) has ‖P‖ = 0.5 and dist P A = 0.5, while P = (0, 0.5) also has ‖P‖ = 0.5 but dist P A ≈ 1.118. These give different triangle areas despite having the same dist 0 P, so no function f(dist 0 P) exists that works for all P. This makes the original statement false and unprovable

putnam_2019_a6:

• Added explicit type cast to WithTop ℝ in limsup: {x' ^ r * abs (...) | ...} → {(x' ^ r * abs (...) : WithTop ℝ) | ...} - The problem asks to prove that $\limsup_{x \to 0^+} x^r |g''(x)| = \infty$.
• In the original formalization, sSup operates on a set of real numbers, but in ℝ, an unbounded set has no supremum. To express "limsup = ∞", we need sSup to be computed in WithTop ℝ (reals with an additional ⊤ element for infinity), where an unbounded set has supremum ⊤.
• The modified version casts set elements to WithTop ℝ so that sSup produces ⊤ for unbounded sets, making Tendsto ... atTop well-formed to express divergence to infinity.

putnam_2019_a5:

• Changed polynomial specification: (hnpoly : ∀ n x, (npoly n).eval x = (x - 1) ^ n) → (hnpoly : ∀ n : ℕ, npoly n = (Polynomial.X - 1) ^ n) - The problem asks about divisibility of polynomials in $\mathbb{F}_p[x]$ (the finite field $\mathbb{F}_p = \text{ZMod } p$).
• The original formulation only specified the evaluation function: "for all n and x, evaluating npoly n at x gives (x-1)^n". In finite fields, this is ambiguous because two different polynomials can have identical evaluation functions. By Fermat's Little Theorem, $X^p$ and $X$ evaluate to the same value at every point in $\mathbb{F}_p$ (since $a^p = a$ for all $a \in \mathbb{F}_p$), yet they are distinct polynomials with different coefficients.
• The original condition allowed npoly n to be $(X-1)^n + (X^p - X) \cdot f(X)$ for any polynomial $f$, since adding terms that vanish on all field elements doesn't change evaluations. However, polynomial divisibility depends on actual coefficients, not evaluation behavior. The modified version directly defines npoly n as the polynomial $(X-1)^n$, unambiguously specifying the intended polynomial and making the divisibility condition well-defined.

putnam_2019_b5:

• Added positivity constraints: (P.eval 2019 = F j - F k) → (P.eval 2019 = F j - F k ∧ 1 ≤ j ∧ 1 ≤ k) - The problem defines the Fibonacci sequence starting at index 1: "$F_1 = F_2 = 1$ and $F_m = F_{m-1} + F_{m-2}$ for all $m \geq 3$".
• The formalization uses F : ℕ → ℤ, which includes F 0. However, the hypotheses only constrain F 1 = 1, F 2 = 1, and the recurrence for indices ≥ 1. The value F 0 is completely unconstrained and could be any integer.

putnam_2022_a4:

• The original used X l ω < X (l + 1) ω, characterizing an increasing sequence - the opposite of what's intended. Before reaching k, the sequence should be decreasing: $X_0 \geq X_1 \geq ... \geq X_{k-1} \geq X_k$, then $X_k &lt; X_{k+1}$ breaks this pattern. The modified version correctly uses X l ω > X (l + 1) ω to capture the decreasing portion.
• Fixed solution sign and type: 2Real.exp (-1/2) - 3 → 2Real.exp ((1 : ℝ) / 2) - 3 - The commented solution had a negative exponent, but the correct answer requires positive exp(1/2). Added explicit type cast (1 : ℝ) to ensure real division instead of natural number division, avoiding truncation (1/2 → 0.5, not 0).