implement problem extraction

.github/workflows/push-main.yaml

@@ -52,6 +52,7 @@ jobs:
         run: |
           set -o pipefail
           echo "Starting build at $(date +'%T')"
+          export GITHUB_PAGES_BASEURL="https://dwrensha.github.io/math-puzzles-in-lean4/"
           build/bin/buildWebpage
           result_run1=$?
           echo "Complete at $(date +'%T'); return value $result_run1"

MathPuzzles/Bulgaria1998Q1.lean

@@ -8,6 +8,8 @@ import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.IntervalCases
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 Bulgarian Mathematical Olympiad 1998, Problem 1
 
@@ -19,12 +21,14 @@ the same color.
 
 namespace Bulgaria1998Q1
 
+@[problem_setup]
 def coloring_has_desired_points (m : ℕ) (color : Set.Icc 1 m → Fin 2) : Prop :=
   ∃ i j : Set.Icc 1 m,
     i < j ∧
     ∃ h3 : 2 * j.val - i ∈ Set.Icc 1 m,
     color i = color j ∧ color i = color ⟨2 * j - i, h3⟩
 
+@[solution_data]
 def n := 9
 
 def coloring_of_eight : Set.Icc 1 8 → Fin 2
@@ -38,6 +42,7 @@ def coloring_of_eight : Set.Icc 1 8 → Fin 2
 | ⟨8, _⟩ => 0
 | _ => 0 -- unreachable
 
+@[problem_statement]
 theorem bulgaria1998_q1a :
     ∃ f: Set.Icc 1 (n - 1) → Fin 2, ¬coloring_has_desired_points (n - 1) f := by
   use coloring_of_eight
@@ -48,6 +53,7 @@ theorem bulgaria1998_q1a :
   dsimp[coloring_of_eight] at *
   interval_cases i <;> interval_cases j <;> aesop
 
+@[problem_statement]
 theorem bulgaria1998_q1b (color : Set.Icc 1 n → Fin 2) : coloring_has_desired_points n f := by
   sorry
 

MathPuzzles/Bulgaria1998Q11.lean

@@ -9,7 +9,10 @@ import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.ModCases
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Zify
-/-
+
+import MathPuzzles.Meta.Attributes
+
+/-!
 Bulgarian Mathematical Olympiad 1998, Problem 11
 
 Let m,n be natural numbers such that
@@ -36,6 +39,7 @@ lemma foo1 (m n : ℕ) (ho : Odd m) : (m + 3) ^ n.succ % 2 = 0 := by
   rw[hw, Nat.pow_succ, show 2 * w + 1 + 3 = 2 * (w + 2) by ring, Nat.mul_mod,
      Nat.mul_mod_right, mul_zero, Nat.zero_mod]
 
+@[problem_statement]
 theorem bulgaria1998_q11
     (m n A : ℕ)
     (h : 3 * m * A = (m + 3)^n + 1) : Odd A := by

MathPuzzles/Bulgaria1998Q2.lean

@@ -9,6 +9,8 @@ import Mathlib.LinearAlgebra.AffineSpace.Midpoint
 import Mathlib.Geometry.Euclidean.Basic
 import Mathlib.Geometry.Euclidean.Triangle
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 Bulgarian Mathematical Olympiad 1998, Problem 2
 
@@ -23,6 +25,7 @@ namespace Bulgaria1998Q2
 
 open EuclideanGeometry
 
+@[problem_statement]
 theorem bulgaria1998_q2
     (A B C D E M: EuclideanSpace ℝ (Fin 2))
     (H1 : dist D A = dist D C)

MathPuzzles/Bulgaria1998Q3.lean

@@ -9,6 +9,8 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Analysis.SpecificLimits.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-
 Bulgarian Mathematical Olympiad 1998, Problem 3
 
@@ -30,6 +32,7 @@ lemma geom_sum_bound (n : ℕ) : ∑ i in Finset.range n, (1:ℝ) / (2^i) < 3 :=
         _ ≤ 2 := sum_geometric_two_le n
         _ < 3 := by norm_num
 
+@[problem_statement]
 theorem bulgaria1998_q3
     (f : ℝ → ℝ)
     (hpos : ∀ x : ℝ, 0 < x → 0 < f x)

MathPuzzles/Bulgaria1998Q6.lean

@@ -10,6 +10,8 @@ import Mathlib.Order.WellFounded
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Ring
 
+import MathPuzzles.Meta.Attributes
+
 /-
 Bulgarian Mathematical Olympiad 1998, Problem 6
 
@@ -61,6 +63,7 @@ lemma lemma_1
   rw [←hs'] at h
   sorry
 
+@[problem_statement]
 theorem bulgaria1998_q6
     (x y z : ℤ)
     (hx : 0 < x)

MathPuzzles/Bulgaria1998Q8.lean

@@ -8,7 +8,9 @@ import Mathlib.Algebra.Ring.Basic
 import Mathlib.Data.Rat.Basic
 import Mathlib.Tactic.Ring
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 Bulgarian Mathematical Olympiad 1998, Problem 8
 The polynomials Pₙ(x,y) for n = 1, 2, ... are defined by P₁(x,y) = 1 and
   Pₙ₊₁(x,y) = (x + y - 1)(y + 1)Pₙ(x,y+2) + (y - y²)Pₙ(x,y)
@@ -19,6 +21,7 @@ namespace Bulgaria1998Q8
 
 variable {R : Type} [CommRing R]
 
+@[problem_setup]
 def P : ℕ → R → R → R
 | 0, _, _ => 1
 | n+1, x, y => (x + y - 1) * (y + 1) * P n x (y + 2) + (y - y^2) * P n x y
@@ -43,6 +46,7 @@ def U : ℕ → R → R → R
 | n, x, y => (x + y - 1) *((y + 1)*(x - x^2) * P n (y + 2) x
                            + (x + 1) * (y - y^2) * P n y (x + 2))
 
+@[problem_statement]
 theorem bulgaria1998_q8 (n : ℕ) (x y : R) : P n x y = P n y x := by
   -- We induct on n. For n = 1,2 the result is evident.
   -- So we take n > 1 and suppose that the result is true for

MathPuzzles/Canada1998Q3.lean

@@ -7,13 +7,14 @@ Authors: David Renshaw
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Data.Real.Basic
-import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Positivity
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 Canadian Mathematical Olympiad 1998, Problem 3
 
 Let n be a natural number such that n ≥ 2. Show that
@@ -25,6 +26,7 @@ namespace Canada1998Q3
 
 open BigOperators
 
+@[problem_statement]
 theorem canada1998_q3 (n : ℕ) (hn : 2 ≤ n) :
     (1/((n:ℝ) + 1)) * ∑ i in Finset.range n, (1/(2 * (i:ℝ) + 1)) >
     (1/(n:ℝ)) * ∑ i in Finset.range n, (1/(2 * (i:ℝ) + 2)) := by

MathPuzzles/Canada1998Q5.lean

@@ -6,7 +6,9 @@ Authors: David Renshaw
 
 import Mathlib.Data.Int.Basic
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 Canadian Mathematical Olympiad 1998, Problem 5
 
 Let m be a positive integer. Define the sequence {aₙ} by a₀ = 0,
@@ -20,11 +22,13 @@ if an only if (a,b) = (aₙ,aₙ₊₁) for some n ≥ 0.
 
 namespace Canada1998Q5
 
+@[problem_setup]
 def A (m : ℕ) (hm : 0 < m) : ℕ → ℤ
 | 0 => 0
 | 1 => (↑m)
 | n + 2 => (m : ℤ)^2 * A m hm (n + 1) - A m hm n
 
+@[problem_statement]
 theorem canada1998_q5 (m : ℕ) (hm : 0 < m) (a b : ℕ) (hab : a ≤ b) :
     a^2 + b^2 = m^2 * (a * b + 1) ↔
      ∃ n : ℕ, (a:ℤ) = A m hm n ∧ (b:ℤ) = A m hm (n + 1) := by

MathPuzzles/Hungary1998Q6.lean

@@ -11,7 +11,9 @@ import Mathlib.Algebra.Associated
 import Mathlib.Data.Int.Basic
 import Mathlib.Tactic.Ring
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 Hungarian Mathematical Olympiad 1998, Problem 6
 
 Let x, y, z be integers with z > 1. Show that
@@ -39,6 +41,7 @@ lemma cast_sum_square (n : ℕ) :
   ∑i in Finset.range n, ((i:ℤ)+1)^2 =
    (((∑i in Finset.range n, (i+1)^2):ℕ) :ℤ) := by norm_cast
 
+@[problem_statement]
 theorem hungary1998_q6 (x y : ℤ) (z : ℕ) (hz : 1 < z) :
     (∑ i in Finset.range 99, (x + i + 1)^2) ≠ y^z := by
   -- Suppose (x + 1)² + (x + 2)² + ... + (x + 99)² = yᶻ.

MathPuzzles/Imo1959Q1.lean

@@ -8,6 +8,8 @@ import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Tactic.Ring
 import Mathlib.Data.Nat.Prime
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 1959 Q1
 Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every
@@ -28,6 +30,7 @@ lemma calculation
   have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1 := by ring
   exact (Nat.dvd_add_right h3).mp (h5 ▸ h4)
 
+@[problem_statement]
 theorem imo1959_q1 : ∀ n : ℕ, Nat.coprime (21 * n + 4) (14 * n + 3) :=
 fun n => Nat.coprime_of_dvd' <| λ k _ h1 h2 => calculation n k h1 h2
 

MathPuzzles/Imo1964Q1B.lean

@@ -8,6 +8,8 @@ import Mathlib.Data.Nat.Basic
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Tactic.Linarith
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # International Mathematical Olympiad 1964, Problem 1b
 
@@ -24,6 +26,7 @@ Informal proof (credit to twitch.tv viewer int_fast64_t):
     2^n mod 7 = (2^3 mod 7)^k * 2^j mod 7 = 1 mod 7 * 2^j mod 7,
   but 2^j < 5
 -/
+@[problem_statement]
 theorem imo_1964_q1b (n : ℕ) : ¬ 7 ∣ (2^n + 1) := by
   intro h
   replace h := Nat.mod_eq_zero_of_dvd h

MathPuzzles/Imo1964Q4.lean

@@ -8,6 +8,8 @@ import Aesop
 import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Tactic.Linarith
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # International Mathematical Olympiad 1964, Problem 4
 
@@ -107,6 +109,7 @@ theorem lemma1
       have h9 := ht3 t3'
       rw[←h9]
 
+@[problem_statement]
 theorem imo1964_q4
     (Person Topic : Type)
     [Fintype Person] [DecidableEq Person]

MathPuzzles/Imo1986Q1.lean

@@ -10,6 +10,8 @@ import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Tactic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 1986 Q1
 
@@ -90,7 +92,7 @@ theorem imo1986_q1' (d : ℤ):
     exact ⟨w * v, hnm'⟩
   exact Int.even_iff_not_odd.mp hdeven hdodd
 
-
+@[problem_statement]
 theorem imo1986_q1 (d : ℤ) (_hdpos : 1 ≤ d) (h2 : d ≠ 2) (h5 : d ≠ 5) (h13 : d ≠ 13) :
     ∃ a b :({2, 5, 13, d} : Finset ℤ), (a ≠ b) ∧ ¬ ∃ z, z^2 = (a * (b : ℤ) - 1) := by
   by_contra h

MathPuzzles/Imo1987Q4.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2023 Moritz Firsching. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Renshaw
+-/
+
 import Aesop
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Interval
@@ -6,6 +12,8 @@ import Mathlib.Data.Fintype.Card
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Ring
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # International Mathematical Olympiad 1987, Problem 4
 
@@ -105,6 +113,7 @@ theorem imo1987_q4_generalized (m : ℕ) :
   apply_fun (· % 2) at h2
   norm_num at h2
 
+@[problem_statement]
 theorem imo1987_q4 : (¬∃ f : ℕ → ℕ, ∀ n, f (f n) = n + 1987) := by
   rw[show 1987 = (2 * 993 + 1) by norm_num]
   exact imo1987_q4_generalized 993

MathPuzzles/Imo1989Q5.lean

@@ -4,6 +4,8 @@ import Mathlib.Data.Nat.Prime
 import Mathlib.Tactic.Common
 import Std.Data.List.Lemmas
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # International Mathematical Olympiad 1989, Problem 5
 
@@ -154,6 +156,7 @@ lemma lemma4 {a b : ℕ} (h : a ≡ b [MOD b]) : a ≡ 0 [MOD b] := by
   rw[h2] at h1
   exact h1
 
+@[problem_statement]
 theorem imo1989_q5 (n : ℕ) : ∃ m, ∀ j < n, ¬IsPrimePow (m + j) := by
   -- (informal solution from https://artofproblemsolving.com)
   -- Let p₁,p₂,...pₙ,q₁,q₂,...,qₙ be distinct primes.

MathPuzzles/Imo2011Q3.lean

@@ -1,5 +1,7 @@
 import Mathlib.Data.Real.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 2011 Q3
 
@@ -8,12 +10,15 @@ Let f : ℝ → ℝ be a function that satisfies
    f(x + y) ≤ y * f(x) + f(f(x))
 
 for all x and y. Prove that f(x) = 0 for all x ≤ 0.
+-/
 
+/-
 # Solution
 
 Direct translation of the solution found in https://www.imo-official.org/problems/IMO2011SL.pdf
 -/
 
+@[problem_statement]
 theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f x)) :
   ∀ x ≤ 0, f x = 0 := by
   -- reparameterize

MathPuzzles/Imo2013Q1.lean

@@ -9,6 +9,8 @@ import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FieldSimp
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 2013 Q1
 
@@ -17,6 +19,9 @@ m₁, m₂, ..., mₖ (not necessarily different) such that
 
   1 + (2ᵏ - 1)/ n = (1 + 1/m₁) * (1 + 1/m₂) * ... * (1 + 1/mₖ).
 
+-/
+
+/-
 # Solution
 
 Adaptation of the solution found in https://www.imo-official.org/problems/IMO2013SL.pdf
@@ -35,8 +40,10 @@ theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :
   intro i hi
   simp [Finset.mem_range.mp hi]
 
+@[problem_statement]
 theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
-    ∃ m : ℕ → ℕ+, (1 : ℚ) + (2 ^ k - 1) / n = ∏ i in Finset.range k, (1 + 1 / (m i : ℚ)) := by
+    ∃ m : ℕ → ℕ+,
+      (1 : ℚ) + (2 ^ k - 1) / n = ∏ i in Finset.range k, (1 + 1 / (m i : ℚ)) := by
   revert n
   induction' k with pk hpk
   · intro n; use fun (_ : ℕ) => (1 : ℕ+); simp