Add the docstrings to the Lean files.

Also includes a CI step to verify the docstrings are right.

.github/workflows/lean.yml

@@ -38,6 +38,11 @@ jobs:
       run: |
         lake exe cache pack
 
+    - name: Validate docstrings
+      working-directory: lean4
+      run: |
+        lake exe check_docstrings
+
     - name: Insert solutions
       working-directory: lean4
       run: |

lean4/check_docstrings.lean

@@ -0,0 +1,78 @@
+import Mathlib.Lean.CoreM
+import Mathlib.Util.GetAllModules
+import Batteries.Lean.Util.Path
+import Lean.Elab.Frontend
+import Batteries.Data.String.Matcher
+
+
+open Lean Elab Command Frontend
+
+def allModules : IO (Array Name) := do
+  let mut ret := #[]
+  for p in ← System.FilePath.walkDir "src" do
+    ret := ret.push (← moduleNameOfFileName p none)
+  return ret
+
+structure InformalJsonEntry where
+  problem_name : Name
+  informal_statement : String
+  informal_solution : Option String
+  tags : List String
+deriving Lean.ToJson, Lean.FromJson
+
+def getModuleNameFor? (env : Environment) (nm : Name) : Option Name :=
+  env.getModuleIdxFor? nm >>= fun i => env.header.moduleNames[i.toNat]?
+
+inductive EntryResult
+  | docMatching
+  | docMismatching
+  | docMissing
+  | missing
+
+/-- Return true if the entry is ok -/
+def checkEntry (entry : InformalJsonEntry) : CoreM EntryResult := do
+  let doc? := (← Lean.findDocString? (← getEnv) entry.problem_name).map String.trim
+  if doc? = some entry.informal_statement.trim then
+    return .docMatching
+  else if let .some doc := doc? then
+    IO.eprintln <|
+      f!"Doc for {entry.problem_name}:\
+      \n{doc}\
+      \ndoesn't match the content of `informal/putnam.json`:\
+      \n{entry.informal_statement.trim}"
+    return .docMismatching
+  else
+    try
+      discard <| getConstInfo entry.problem_name
+    catch _ =>
+      IO.eprintln <| s!"No formalization of {entry.problem_name}"
+      return .missing
+    IO.eprintln <|
+      s!"Doc for {entry.problem_name} is missing, adding one. Please rerun `lake build`."
+    addDocstring
+    return .docMissing
+where
+  addDocstring : CoreM Unit := do
+    -- hack, but good enough
+    let fname : System.FilePath := "src" / s!"{entry.problem_name.toString}.lean"
+    let mut raw ← IO.FS.readFile fname
+    let .some thm := raw.findSubstr? "\ntheorem" | throwError "Cannot find theorem command"
+    raw :=
+      raw.extract 0 thm.startPos
+      ++ "\n/--\n" ++ entry.informal_statement.trim ++ "\n-/"
+      ++ raw.extract thm.startPos raw.endPos
+    IO.FS.writeFile fname raw
+
+def main : IO UInt32 := do
+  searchPathRef.set compile_time_search_path%
+  let json ← IO.ofExcept <| Lean.Json.parse <| ← IO.FS.readFile (".." / "informal" / "putnam.json")
+  let data : Array InformalJsonEntry ← IO.ofExcept <| fromJson? json
+  CoreM.withImportModules (← allModules) do
+    let mut any_errors := false
+    for entry in data do
+      match ← checkEntry entry with
+      | .docMissing | .docMismatching =>
+        any_errors := true
+      | .missing | .docMatching =>
+        pure ()
+    return bif any_errors then 1 else 0

lean4/lakefile.lean

@@ -14,3 +14,7 @@ lean_lib «putnam» where
 
 lean_lib «putnam_with_solutions» where
   globs := #[.submodules `solutions_replaced_new]
+
+lean_exe «check_docstrings» where
+  root := `check_docstrings
+  supportInterpreter := true

lean4/src/putnam_1962_a1.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open MeasureTheory
 
+/--
+Given five points in a plane, no three of which lie on a straight line, show that some four of these points form the vertices of a convex quadrilateral.
+-/
 theorem putnam_1962_a1
 (S : Set (ℝ × ℝ))
 (hS : S.ncard = 5)

lean4/src/putnam_1962_a2.lean

@@ -5,6 +5,9 @@ open MeasureTheory Set
 
 abbrev putnam_1962_a2_solution : Set (ℝ → ℝ) := sorry
 -- {f : ℝ → ℝ | ∃ a c : ℝ, a ≥ 0 ∧ f = fun x ↦ a / (1 - c * x) ^ 2}
+/--
+Find every real-valued function $f$ whose domain is an interval $I$ (finite or infinite) having 0 as a left-hand endpoint, such that for every positive member $x$ of $I$ the average of $f$ over the closed interval $[0, x]$ is equal to the geometric mean of the numbers $f(0)$ and $f(x)$.
+-/
 theorem putnam_1962_a2
     (P : Set ℝ → (ℝ → ℝ) → Prop)
     (P_def : ∀ s f, P s f ↔ 0 ≤ f ∧ ∀ x ∈ s, ⨍ t in Ico 0 x, f t = √(f 0 * f x)) :

lean4/src/putnam_1962_a3.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open MeasureTheory
 
+/--
+Let $\triangle ABC$ be a triangle in the Euclidean plane, with points $P$, $Q$, and $R$ lying on segments $\overline{BC}$, $\overline{CA}$, $\overline{AB}$ respectively such that $$\frac{AQ}{QC} = \frac{BR}{RA} = \frac{CP}{PB} = k$$ for some positive constant $k$. If $\triangle UVW$ is the triangle formed by parts of segments $\overline{AP}$, $\overline{BQ}$, and $\overline{CR}$, prove that $$\frac{[\triangle UVW]}{[\triangle ABC]} = \frac{(k - 1)^2}{k^2 + k + 1},$$ where $[\triangle]$ denotes the area of the triangle $\triangle$.
+-/
 theorem putnam_1962_a3
 (A B C A' B' C' P Q R : EuclideanSpace ℝ (Fin 2))
 (k : ℝ)

lean4/src/putnam_1962_a4.lean

@@ -1,6 +1,9 @@
 import Mathlib
 open BigOperators
 
+/--
+Assume that $\lvert f(x) \rvert \le 1$ and $\lvert f''(x) \rvert \le 1$ for all $x$ on an interval of length at least 2. Show that $\lvert f'(x) \rvert \le 2$ on the interval.
+-/
 theorem putnam_1962_a4
 (f : ℝ → ℝ)
 (a b : ℝ)

lean4/src/putnam_1962_a5.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 abbrev putnam_1962_a5_solution : ℕ → ℕ := sorry
 -- fun n : ℕ => n * (n + 1) * 2^(n - 2)
+/--
+Evaluate in closed form \[ \sum_{k=1}^n {n \choose k} k^2. \]
+-/
 theorem putnam_1962_a5
 : ∀ n ≥ 2, putnam_1962_a5_solution n = ∑ k in Finset.Icc 1 n, Nat.choose n k * k^2 :=
 sorry

lean4/src/putnam_1962_a6.lean

@@ -1,6 +1,9 @@
 import Mathlib
 open BigOperators
 
+/--
+Let $S$ be a set of rational numbers such that whenever $a$ and $b$ are members of $S$, so are $a+b$ and $ab$, and having the property that for every rational number $r$ exactly one of the following three statements is true: \[ r \in S, -r \in S, r = 0. \] Prove that $S$ is the set of all positive rational numbers.
+-/
 theorem putnam_1962_a6
 (S : Set ℚ)
 (hSadd : ∀ a ∈ S, ∀ b ∈ S, a + b ∈ S)

lean4/src/putnam_1962_b1.lean

@@ -1,6 +1,9 @@
 import Mathlib
 open BigOperators
 
+/--
+Let $x^{(n)} = x(x-1)\cdots(x-n+1)$ for $n$ a positive integer and let $x^{(0)} = 1.$ Prove that \[ (x+y)^{(n)} = \sum_{k=0}^n {n \choose k} x^{(k)} y^{(n-k)}. \]
+-/
 theorem putnam_1962_b1
 (p : ℕ → ℝ → ℝ)
 (x y : ℝ)

lean4/src/putnam_1962_b2.lean

@@ -4,6 +4,9 @@ open BigOperators
 open MeasureTheory
 
 --Note: The original problem requires a function to be exhibited, but in the official archives the solution depends on an enumeration of the rationals, so we modify the problem to be an existential statement.
+/--
+Let $\mathbb{S}$ be the set of all subsets of the natural numbers. Prove the existence of a function $f : \mathbb{R} \to \mathbb{S}$ such that $f(a) \subset f(b)$ whenever $a < b$.
+-/
 theorem putnam_1962_b2
 : ∃ f : ℝ → Set ℕ+, ∀ a b : ℝ, a < b → f a ⊂ f b :=
 sorry

lean4/src/putnam_1962_b3.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open MeasureTheory
 
+/--
+Let $S$ be a convex region in the Euclidean plane, containing the origin, for which every ray from the origin has at least one point outside $S$. Assuming that either the origin is an interior point of $S$ or $S$ is topologically closed, prove that $S$ is bounded.
+-/
 theorem putnam_1962_b3
 (S : Set (EuclideanSpace ℝ (Fin 2)))
 (hS : Convex ℝ S ∧ 0 ∈ S)

lean4/src/putnam_1962_b5.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open MeasureTheory
 
+/--
+Prove that for every integer $n$ greater than 1: \[ \frac{3n+1}{2n+2} < \left( \frac{1}{n} \right)^n + \left(\frac{2}{n} \right)^n + \cdots + \left(\frac{n}{n} \right)^n < 2. \]
+-/
 theorem putnam_1962_b5
 (n : ℤ)
 (ng1 : n > 1)

lean4/src/putnam_1962_b6.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open MeasureTheory Real
 
+/--
+Let \[ f(x) = \sum_{k=0}^n a_k \sin kx + b_k \cos kx, \] where $a_k$ and $b_k$ are constants. Show that, if $\lvert f(x) \rvert \le 1$ for $0 \le x \le 2 \pi$ and $\lvert f(x_i) \rvert = 1$ for $0 \le x_1 < x_2 < \cdots < x_{2n} < 2 \pi$, then $f(x) = \cos (nx + a)$ for some constant $a$.
+-/
 theorem putnam_1962_b6
 (n : ℕ)
 (a b : ℕ → ℝ)

lean4/src/putnam_1963_a2.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Topology Filter
 
+/--
+Let $\{f(n)\}$ be a strictly increasing sequence of positive integers such that $f(2)=2$ and $f(mn)=f(m)f(n)$ for every relatively prime pair of positive integers $m$ and $n$ (the greatest common divisor of $m$ and $n$ is equal to $1$). Prove that $f(n)=n$ for every positive integer $n$.
+-/
 theorem putnam_1963_a2
 (f : ℕ → ℕ)
 (hfpos : ∀ n, f n > 0)

lean4/src/putnam_1963_a3.lean

@@ -5,6 +5,9 @@ open Nat Set Topology Filter
 
 noncomputable abbrev putnam_1963_a3_solution : (ℝ → ℝ) → ℕ → ℝ → ℝ → ℝ := sorry
 -- fun (f : ℝ → ℝ) (n : ℕ) (x : ℝ) (t : ℝ) ↦ (x - t) ^ (n - 1) * (f t) / ((n - 1)! * t ^ n)
+/--
+Find an integral formula (i.e., a function $z$ such that $y(x) = \int_{1}^{x} z(t) dt$) for the solution of the differential equation $$\delta (\delta - 1) (\delta - 2) \cdots (\delta - n + 1) y = f(x)$$ with the initial conditions $y(1) = y'(1) = \cdots = y^{(n-1)}(1) = 0$, where $n \in \mathbb{N}$, $f$ is continuous for all $x \ge 1$, and $\delta$ denotes $x\frac{d}{dx}$.
+-/
 theorem putnam_1963_a3
     (P : ℕ → (ℝ → ℝ) → (ℝ → ℝ))
     (hP : P 0 = id ∧ ∀ i y, P (i + 1) y = P i (fun x ↦ x * deriv y x - i * y x))

lean4/src/putnam_1963_a4.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Filter Set
 
+/--
+Let $\{a_n\}$ be a sequence of positive real numbers. Show that $\limsup_{n \to \infty} n\left(\frac{1+a_{n+1}}{a_n}-1\right) \geq 1$. Show that the number $1$ on the right-hand side of this inequality cannot be replaced by any larger number. (The symbol $\limsup$ is sometimes written $\overline{\lim}$.)
+-/
 theorem putnam_1963_a4
     (T : (ℕ → ℝ) → (ℕ → ℝ))
     (T_def : ∀ a n, T a n = n * ((1 + a (n + 1)) / a n - 1))

lean4/src/putnam_1963_a6.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Topology Filter
 
+/--
+Let $U$ and $V$ be distinct points on an ellipse, with $M$ the midpoint of chord $\overline{UV}$, and let $\overline{AB}$ and $\overline{CD}$ be any two other chords through $M$. If line $UV$ intersects line $AC$ at $P$ and line $BD$ at $Q$, prove that $M$ is the midpoint of segment $\overline{PQ}$.
+-/
 theorem putnam_1963_a6
 (F1 F2 U V A B C D P Q : EuclideanSpace ℝ (Fin 2))
 (r : ℝ)

lean4/src/putnam_1963_b1.lean

@@ -5,6 +5,9 @@ open Topology Filter Polynomial
 
 abbrev putnam_1963_b1_solution : ℤ := sorry
 -- 2
+/--
+For what integer $a$ does $x^2-x+a$ divide $x^{13}+x+90$?
+-/
 theorem putnam_1963_b1
 : ∀ a : ℤ, (X^2 - X + (C a)) ∣ (X ^ 13 + X + (C 90)) ↔ a = putnam_1963_b1_solution :=
 sorry

lean4/src/putnam_1963_b2.lean

@@ -5,6 +5,9 @@ open Topology Filter Polynomial
 
 abbrev putnam_1963_b2_solution : Prop := sorry
 -- True
+/--
+Let $S$ be the set of all numbers of the form $2^m3^n$, where $m$ and $n$ are integers, and let $P$ be the set of all positive real numbers. Is $S$ dense in $P$?
+-/
 theorem putnam_1963_b2
 (S : Set ℝ)
 (hS : S = {2 ^ m * 3 ^ n | (m : ℤ) (n : ℤ)})

lean4/src/putnam_1963_b3.lean

@@ -5,6 +5,9 @@ open Topology Filter Polynomial
 
 abbrev putnam_1963_b3_solution : Set (ℝ → ℝ) := sorry
 -- {(fun u : ℝ => A * Real.sinh (k * u)) | (A : ℝ) (k : ℝ)} ∪ {(fun u : ℝ => A * u) | A : ℝ} ∪ {(fun u : ℝ => A * Real.sin (k * u)) | (A : ℝ) (k : ℝ)}
+/--
+Find every twice-differentiable real-valued function $f$ with domain the set of all real numbers and satisfying the functional equation $(f(x))^2-(f(y))^2=f(x+y)f(x-y)$ for all real numbers $x$ and $y$.
+-/
 theorem putnam_1963_b3
 (f : ℝ → ℝ)
 (fdiff : Prop)

lean4/src/putnam_1963_b5.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Topology Filter Polynomial
 
+/--
+Let $\{a_n\}$ be a sequence of real numbers satisfying the inequalities $0 \leq a_k \leq 100a_n$ for $n \leq k \leq 2n$ and $n=1,2,\dots$, and such that the series $\sum_{n=0}^\infty a_n$ converges. Prove that $\lim_{n \to \infty}na_n=0$.
+-/
 theorem putnam_1963_b5
 (a : ℤ → ℝ)
 (haineq : ∀ n ≥ 1, ∀ k : ℤ, (n ≤ k ∧ k ≤ 2 * n) → (0 ≤ a k ∧ a k ≤ 100 * a n))

lean4/src/putnam_1963_b6.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Topology Filter Polynomial
 
+/--
+Let $E$ be a Euclidean space of at most three dimensions. If $A$ is a nonempty subset of $E$, define $S(A)$ to be the set of all points that lie on closed segments joining pairs of points of $A$. For a given nonempty set $A_0$, define $A_n=S(A_{n-1})$ for $n=1,2,\dots$. Prove that $A_2=A_3=\cdots$. (A one-point set should be considered to be a special case of a closed segment.)
+-/
 theorem putnam_1963_b6
 (d : ℕ)
 (S : Set (Fin d → ℝ) → Set (Fin d → ℝ))

lean4/src/putnam_1964_a1.lean

@@ -1,6 +1,9 @@
 import Mathlib
 open BigOperators
 
+/--
+Let $A_1, A_2, A_3, A_4, A_5, A_6$ be distinct points in the plane. Let $D$ be the longest distance between any pair, and let $d$ the shortest distance. Show that $\frac{D}{d} \geq \sqrt 3$.
+-/
 theorem putnam_1964_a1
 (A : Finset (EuclideanSpace ℝ (Fin 2)))
 (hAcard : A.card = 6)

lean4/src/putnam_1964_a2.lean

@@ -6,6 +6,14 @@ open Set
 -- Note: uses (ℝ → ℝ) instead of (Icc 0 1 → ℝ)
 abbrev putnam_1964_a2_solution : ℝ → Set (ℝ → ℝ) := sorry
 -- fun _ ↦ ∅
+/--
+Let $\alpha$ be a real number. Find all continuous real-valued functions $f : [0, 1] \to (0, \infty)$ such that 
+\begin{align*}
+\int_0^1 f(x) dx &= 1, \\
+\int_0^1 x f(x) dx &= \alpha, \\
+\int_0^1 x^2 f(x) dx &= \alpha^2. \\
+\end{align*}
+-/
 theorem putnam_1964_a2
 (α : ℝ)
 : (putnam_1964_a2_solution α = {f : ℝ → ℝ | (∀ x ∈ Icc 0 1, f x > 0) ∧ ContinuousOn f (Icc 0 1) ∧ ∫ x in (0)..1, f x = 1 ∧ ∫ x in (0)..1, x * f x = α ∧ ∫ x in (0)..1, x^2 * f x = α^2}) :=

lean4/src/putnam_1964_a3.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Set Function
 
+/--
+The distinct points $x_n$ are dense in the interval $(0, 1)$. For all $n \geq 1$, $x_1, x_2, \dots , x_{n-1}$ divide $(0, 1)$ into $n$ sub-intervals, one of which must contain $x_n$. This part is divided by $x_n$ into two sub-intervals, lengths $a_n$ and $b_n$. Prove that $\sum_{n=1}^{\infty} a_nb_n(a_n + b_n) = \frac{1}{3}$.
+-/
 theorem putnam_1964_a3
 (x a b : ℕ → ℝ)
 (hxdense : range x ⊆ Ioo 0 1 ∧ closure (range x) ⊇ Ioo 0 1)

lean4/src/putnam_1964_a4.lean

@@ -3,6 +3,13 @@ open BigOperators
 
 open Set Function
 
+/--
+The sequence of integers $u_n$ is bounded and satisfies 
+\[
+u_n = \frac{u_{n-1} + u_{n-2} + u_{n-3}u_{n-4}}{u_{n-1}u_{n-2} + u_{n-3} + u_{n-4}}.
+\] 
+Show that it is periodic for sufficiently large $n$.
+-/
 theorem putnam_1964_a4
 (u : ℕ → ℤ)
 (boundedu : ∃ B T : ℤ, ∀ n : ℕ, B ≤ u n ∧ u n ≤ T)

lean4/src/putnam_1964_a5.lean

@@ -3,6 +3,12 @@ open BigOperators
 
 open Set Function Filter Topology
 
+/--
+Prove that there exists a constant $k$ such that for any sequence $a_i$ of positive numbers, 
+\[
+\sum_{n=1}^{\infty} \frac{n}{a_1 + a_2 + \dots + a_n} \leq k \sum_{n=1}^{\infty}\frac{1}{a_n}.
+\]
+-/
 theorem putnam_1964_a5
 (pa : (ℕ → ℝ) → Prop)
 (hpa : pa = fun a ↦ (∀ n : ℕ, a n > 0) ∧ ∃ L : ℝ, Tendsto (fun N ↦ ∑ n in Finset.range N, 1 / a n) atTop (𝓝 L))

lean4/src/putnam_1964_a6.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Set Function Filter Topology
 
+/--
+Let $S$ be a finite set of collinear points. Let $k$ be the maximum distance between any two points of $S$. Given a pair of points of $S$ a distance $d < k$ apart, we can find another pair of points of $S$ also a distance $d$ apart. Prove that if two pairs of points of $S$ are distances $a$ and $b$ apart, then $rac{a}{b}$ is rational.
+-/
 theorem putnam_1964_a6
 (S : Finset ℝ)
 (pairs : Set (ℝ × ℝ))

lean4/src/putnam_1964_b1.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Set Function Filter Topology
 
+/--
+Let $a_n$ be a sequence of positive integers such that $\sum_{n=1}^{\infty} 1/a_n$ converges. For all $n$, let $b_n$ be the number of $a_n$ which are at most $n$. Prove that $\lim_{n \to \infty} b_n/n = 0$.
+-/
 theorem putnam_1964_b1
     (a b : ℕ → ℕ)
     (h₁ : ∀ n, 0 < a n)

lean4/src/putnam_1964_b2.lean

@@ -3,6 +3,9 @@ open BigOperators
 
 open Set Function Filter Topology
 
+/--
+Let $S$ be a finite set. A set $P$ of subsets of $S$ has the property that any two members of $P$ have at least one element in common and that $P$ cannot be extended (whilst keeping this property). Prove that $P$ contains exactly half of the subsets of $S$.
+-/
 theorem putnam_1964_b2
 (S : Type*) [Fintype S] [Nonempty S]
 (P : Finset (Set S))