Merge branch 'main' of https://github.com/trishullab/PutnamBench into…

… george

.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: |

README.md

@@ -8,7 +8,7 @@
 
 PutnamBench is a benchmark for evaluation of theorem-proving algorithms on competition mathematics problems sourced from the William Lowell Putnam Mathematical Competition years 1962 - 2023. Our formalizations currently support three formal languages : Lean 4 $\land$ Isabelle $\land$ Coq. PutnamBench comprises of 1697 manually-crafted formalizations, aggregated over all languages.
 
-PutnamBench aims to support research in automated mathematical reasoning by providing a multilingual benchmark for evaluating theorem-proving algorithms. It is released under permissive licenses (Apache 2.0 for Lean 4 and Isabelle, MIT for Coq). The informal statements are also available with permission from the MAA.
+PutnamBench aims to support research in automated mathematical reasoning by providing a multilingual benchmark for evaluating theorem-proving algorithms. It is released under permissive licenses (Apache 2.0 for Lean 4 and Isabelle, MIT for Coq). The [informal statements](informal/README.md) are also available with permission from the MAA.
 
 PutnamBench includes factored solutions for problems which require exhibiting a numerical answer in addition to its proof of correctness. For these problems, one can attempt two tasks: proving the problem with the numerical answer written into the theorem statement, or additionally producing the answer along with the proof.
 

informal/README.md

@@ -1 +1,10 @@
-The informal statement information is encapsulated in json files indicating batches of problems.
+The informal statements can be found in `putnam.json`.
+
+Remember that when writing $\LaTeX$ within a JSON string, you must escape backslashes;
+that is, you must write:
+```json
+"informal_statement": "What is the cardinality of $\\frac{1}{2} \\pm 1 \\pm 2$"
+```
+
+These statements are also present in the docstrings of some of the formal statements.
+Github CI will automatically catch if these are out of sync, but if you update them in one place you will have to update them in the other.

isabelle/putnam_1969_b2.thy

@@ -6,11 +6,10 @@ begin
 definition putnam_1969_b2_solution :: bool where "putnam_1969_b2_solution \<equiv> undefined"
 (* False *)
 theorem putnam_1969_b2:
-  fixes G (structure)
-  and h :: "nat \<Rightarrow> bool"
-  assumes hG: "group G \<and> finite (carrier G)"
-  defines "h \<equiv> (\<lambda>n::nat. (\<exists>H::nat\<Rightarrow>('a set). (\<forall>i::nat\<in>{0..(n-1)}. subgroup (H i) G \<and> H i \<noteq> carrier G) \<and> (carrier G = (\<Union>i::nat\<in>{0..(n-1)}. H i))))"
-  shows "\<not>(h 2) \<and> ((\<not>(h 3)) \<longleftrightarrow> putnam_1969_b2_solution)"
+  fixes P :: "nat \<Rightarrow> bool"
+  defines "P \<equiv> \<lambda> n. \<forall> G. group G \<and> finite (carrier G) \<longrightarrow>
+    (\<forall> H. (\<forall> i\<in>{0..<n}. subgroup (H i) G \<and> (H i) \<noteq> carrier G) \<longrightarrow> (carrier G \<noteq> (\<Union>i::nat\<in>{0..<n}. H i)))"
+  shows "P 2 \<and> (P 3 \<longleftrightarrow> putnam_1969_b2_solution)"
   sorry
 
 end

lean4/README.md

@@ -0,0 +1,17 @@
+# Lean formalizations
+
+The formalizations in this folder are of the form
+```lean
+import Mathlib
+
+abbrev putnam_easy_solution : ℕ := sorry
+-- 2
+
+/-- What is 1 + 1 -/
+theorem putnam_easy : 1 + 1 = putnam_easy_solution := sorry
+```
+
+To generate versions with the solution inlined into the question, you can use `python scripts/rewrite_solutions.py`.
+
+The docstring on the theorem must stay in sync with `informal/putnam.json` (this is checked by GitHub's CI),
+and should not be changed unless the informal problem text is wrong!

lean4/check_docstrings.lean

@@ -0,0 +1,108 @@
+import Mathlib.Lean.CoreM
+import Mathlib.Util.GetAllModules
+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
+
+/-- Emit a github error that will appear as an annotation in the diff view.
+
+This is adapted from `mathlib3/scripts/detect_errors.py`. -/
+def emitGithubError (msg : String) (file : Option System.FilePath) (pos : Option Position) :
+    IO Unit := do
+  let mut parts := #[]
+  if let .some file := file then
+    parts := parts.push s!"file={file}"
+  if let .some pos := pos then
+    parts := parts.push s!"line={pos.line}"
+    parts := parts.push s!"col={pos.column}"
+  IO.eprintln s!"::error {",".intercalate parts.toList}::{encodeMsg msg}"
+where
+  encodeMsg (msg : String) : String :=
+    msg.replace "%" "%25" |>.replace "\r" "%0D" |>.replace "\n" "%0A"
+
+def getSource (n : Name) : CoreM <| Option (Name × DeclarationRange) := do
+  let .some ranges ← Lean.findDeclarationRanges? n | return none
+  let .some mod ← Lean.findModuleOf? n | return none
+  return some (mod, ranges.range)
+
+/-- 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
+    let srcInfo ← getSource entry.problem_name
+    emitGithubError
+      s!"The docstring for {entry.problem_name} is not in sync with the version in `informal/putnam.json`.\
+      \nPlease either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON.\
+      \nThe JSON file currently contains:\
+      \n\
+      \n{entry.informal_statement.trim}\
+      \n\
+      \nWhile the docstring contains:
+      \n\
+      \n{doc}\n"
+      -- github paths have to be absolute, so include the lean4
+      (some <| "lean4" / "src" / s!"{entry.problem_name}.lean")
+      (srcInfo.map (·.2.pos))
+
+    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/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
+   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,20 +55,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "543725b3bfed792097fc134adca628406f6145f5",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
+   "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "putnam",

lean4/lakefile.lean

@@ -6,11 +6,15 @@ package «putnam» where
   leanOptions := #[
     ⟨`autoImplicit, false⟩
   ]
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.10.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.12.0"
 
 @[default_target]
 lean_lib «putnam» where
   globs := #[.submodules `src]
 
 lean_lib «putnam_with_solutions» where
   globs := #[.submodules `solutions_replaced_new]
+
+lean_exe «check_docstrings» where
+  root := `check_docstrings
+  supportInterpreter := true

lean4/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.12.0

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,9 +5,12 @@ 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 ↔ ∀ x ∈ s, ⨍ t in Ico 0 x, f t = √(f 0 * f x)) :
+    (P_def : ∀ s f, P s f ↔ 0 ≤ f ∧ ∀ x ∈ s, ⨍ t in Ico 0 x, f t = √(f 0 * f x)) :
     (∀ f,
       (P (Ioi 0) f → ∃ g ∈ putnam_1962_a2_solution, EqOn f g (Ici 0)) ∧
       (∀ e > 0, P (Ioo 0 e) f → ∃ g ∈ putnam_1962_a2_solution, EqOn f g (Ico 0 e))) ∧

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

@@ -1,6 +1,11 @@
 import Mathlib
 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 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)