diff --git a/.github/workflows/push-main.yaml b/.github/workflows/push-main.yaml
index 37cbd65a..e7ea93ad 100644
--- a/.github/workflows/push-main.yaml
+++ b/.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"
diff --git a/MathPuzzles/Bulgaria1998Q1.lean b/MathPuzzles/Bulgaria1998Q1.lean
index cd30e5b6..81812016 100644
--- a/MathPuzzles/Bulgaria1998Q1.lean
+++ b/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
 
diff --git a/MathPuzzles/Bulgaria1998Q11.lean b/MathPuzzles/Bulgaria1998Q11.lean
index 884d9207..8afda088 100644
--- a/MathPuzzles/Bulgaria1998Q11.lean
+++ b/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
diff --git a/MathPuzzles/Bulgaria1998Q2.lean b/MathPuzzles/Bulgaria1998Q2.lean
index 2fd3066a..f30e1309 100644
--- a/MathPuzzles/Bulgaria1998Q2.lean
+++ b/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)
diff --git a/MathPuzzles/Bulgaria1998Q3.lean b/MathPuzzles/Bulgaria1998Q3.lean
index 107d6993..e378184c 100644
--- a/MathPuzzles/Bulgaria1998Q3.lean
+++ b/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)
diff --git a/MathPuzzles/Bulgaria1998Q6.lean b/MathPuzzles/Bulgaria1998Q6.lean
index 1a692d0e..acd81106 100644
--- a/MathPuzzles/Bulgaria1998Q6.lean
+++ b/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)
diff --git a/MathPuzzles/Bulgaria1998Q8.lean b/MathPuzzles/Bulgaria1998Q8.lean
index 4eb598a2..c6c85eec 100644
--- a/MathPuzzles/Bulgaria1998Q8.lean
+++ b/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
diff --git a/MathPuzzles/Canada1998Q3.lean b/MathPuzzles/Canada1998Q3.lean
index 48d4a680..ff571191 100644
--- a/MathPuzzles/Canada1998Q3.lean
+++ b/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
diff --git a/MathPuzzles/Canada1998Q5.lean b/MathPuzzles/Canada1998Q5.lean
index 2db27082..d9137d81 100644
--- a/MathPuzzles/Canada1998Q5.lean
+++ b/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
diff --git a/MathPuzzles/Hungary1998Q6.lean b/MathPuzzles/Hungary1998Q6.lean
index 2498eb64..227b28c8 100644
--- a/MathPuzzles/Hungary1998Q6.lean
+++ b/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ᶻ.
diff --git a/MathPuzzles/Imo1959Q1.lean b/MathPuzzles/Imo1959Q1.lean
index ddf1ca9a..b385e127 100644
--- a/MathPuzzles/Imo1959Q1.lean
+++ b/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
 
diff --git a/MathPuzzles/Imo1964Q1B.lean b/MathPuzzles/Imo1964Q1B.lean
index e3a56b86..b9f9c34a 100644
--- a/MathPuzzles/Imo1964Q1B.lean
+++ b/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
diff --git a/MathPuzzles/Imo1964Q4.lean b/MathPuzzles/Imo1964Q4.lean
index 33e7e2eb..c1c959f7 100644
--- a/MathPuzzles/Imo1964Q4.lean
+++ b/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]
diff --git a/MathPuzzles/Imo1986Q1.lean b/MathPuzzles/Imo1986Q1.lean
index 6b861417..a155d25f 100644
--- a/MathPuzzles/Imo1986Q1.lean
+++ b/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
diff --git a/MathPuzzles/Imo1987Q4.lean b/MathPuzzles/Imo1987Q4.lean
index 8aa07eae..7031942f 100644
--- a/MathPuzzles/Imo1987Q4.lean
+++ b/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
diff --git a/MathPuzzles/Imo1989Q5.lean b/MathPuzzles/Imo1989Q5.lean
index 8d73a171..a0472d24 100644
--- a/MathPuzzles/Imo1989Q5.lean
+++ b/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.
diff --git a/MathPuzzles/Imo2011Q3.lean b/MathPuzzles/Imo2011Q3.lean
index 89a564e0..bfff1e2c 100644
--- a/MathPuzzles/Imo2011Q3.lean
+++ b/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
diff --git a/MathPuzzles/Imo2013Q1.lean b/MathPuzzles/Imo2013Q1.lean
index 8858e714..40e05ecb 100644
--- a/MathPuzzles/Imo2013Q1.lean
+++ b/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
diff --git a/MathPuzzles/Imo2013Q5.lean b/MathPuzzles/Imo2013Q5.lean
index ae309776..a79e1ead 100644
--- a/MathPuzzles/Imo2013Q5.lean
+++ b/MathPuzzles/Imo2013Q5.lean
@@ -6,6 +6,8 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.LinearCombination
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 2013 Q5
 
@@ -18,6 +20,9 @@ the conditions
 for all x,y ∈ ℚ>₀. Given that f(a) = a for some rational a > 1, prove that f(x) = x for
 all x ∈ ℚ>₀.
 
+-/
+
+/-
 # Solution
 
 We provide a direct translation of the solution found in
@@ -185,6 +190,7 @@ lemma fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
   have heq := h1.antisymm (by exact_mod_cast h2)
   linarith [H5 x hx, H5 _ h_big_enough]
 
+@[problem_statement]
 theorem imo2013_q5
     (f : ℚ → ℝ)
     (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
diff --git a/MathPuzzles/Imo2018Q3.lean b/MathPuzzles/Imo2018Q3.lean
index c2d4accf..8c925ebe 100644
--- a/MathPuzzles/Imo2018Q3.lean
+++ b/MathPuzzles/Imo2018Q3.lean
@@ -6,6 +6,8 @@ Authors: David Renshaw
 
 import Mathlib.Algebra.BigOperators.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 2018 Q3
 
@@ -23,26 +25,33 @@ which contains every integer from 1 to 10:
 Does there exist an anti-Pascal triangle with 2018 rows which contains every
 integer from 1 to 1 + 2 + ... + 2018?
 
+-/
+
+/-
+
 # Solution
 No.
-
 -/
 
 namespace Imo2018Q3
 open BigOperators
 
+@[problem_setup]
 structure Coords where
 (row : Nat) (col : Nat)
 
+@[problem_setup]
 def left_child (c : Coords) : Coords :=
  ⟨c.row.succ, c.col⟩
 
+@[problem_setup]
 def right_child (c : Coords) : Coords :=
   ⟨c.row.succ, c.col.succ⟩
 
 /--
 antipascal triangle with n rows
 -/
+@[problem_setup]
 structure antipascal_triangle (n : Nat) where
 (f : Coords → Nat)
 (antipascal : ∀ x: Coords, x.row.succ < n ∧ x.col ≤ x.row →
@@ -52,6 +61,7 @@ structure antipascal_triangle (n : Nat) where
 structure a_and_b where
 (a : Coords) (b : Coords)
 
+@[problem_statement]
 theorem imo2018_q3 (t : antipascal_triangle 2018)
     (h_contains_all : ∀ n, n ≤ ∑ i in Finset.range 2018, (i + 1) →
                       ∃ r, r ≤ 2018 ∧ ∃ c, c < r ∧ t.f ⟨r,c⟩ = n) :
diff --git a/MathPuzzles/Imo2019Q1.lean b/MathPuzzles/Imo2019Q1.lean
index 5211d6c1..53e3eac3 100644
--- a/MathPuzzles/Imo2019Q1.lean
+++ b/MathPuzzles/Imo2019Q1.lean
@@ -7,6 +7,8 @@ import Mathlib.Algebra.Module.LinearMap
 import Mathlib.Data.Int.Basic
 import Mathlib.Tactic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # IMO 2019 Q1
 Let ℤ be the set of integers. Determine all functions f : ℤ → ℤ such that,
@@ -27,6 +29,7 @@ lemma additive_to_int_linear (f : ℤ → ℤ) (h: ∀ (x y : ℤ), f (x + y) =
   change g a = g 1 * a
   rw [mul_comm, ← smul_eq_mul, ← LinearMap.map_smul, smul_eq_mul, mul_one]
 
+@[problem_statement]
 theorem imo2019_q1 (f : ℤ → ℤ) (hf : ∀ a b, f (2 * a) + 2 * (f b) = f (f (a + b))) :
   (∀ z,  f z = 0) ∨ (∃ c, ∀ z, f z = 2 * z + c) := by
   let g : ℤ → ℤ := fun z => f z - f 0
diff --git a/MathPuzzles/India1998Q1.lean b/MathPuzzles/India1998Q1.lean
index 46897f13..f4dc09eb 100644
--- a/MathPuzzles/India1998Q1.lean
+++ b/MathPuzzles/India1998Q1.lean
@@ -7,6 +7,8 @@ import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.NormNum.Prime
 
+import MathPuzzles.Meta.Attributes
+
 /-
 Indian Mathematical Olympiad 1998, problem 1
 
@@ -16,10 +18,12 @@ Indian Mathematical Olympiad 1998, problem 1
 
 namespace India1998Q1
 
+@[problem_statement]
 theorem india1998_q1a (a₁ a₂ b₁ b₂ : ℤ) :
     (∃ a₃ b₃, (a₁^2 + 3 * b₁^2) * (a₂^2 + 3 * b₂^2) = (a₃^2 + 3 * b₃^2)) :=
   ⟨a₁ * a₂ + 3 * b₁ * b₂, ⟨a₁ * b₂ - b₁ * a₂, by ring⟩⟩
 
+@[problem_statement]
 theorem india1998_q1b (n a b: ℤ) (hn : a^2 + 3 * b^2 = 7 * n) :
     (∃ a b : ℤ, a^2 + 3 * b^2 = n) := by
   let az : ZMod 7 := a
diff --git a/MathPuzzles/IntegersInACircle.lean b/MathPuzzles/IntegersInACircle.lean
index 955fc305..9e4ea6c6 100644
--- a/MathPuzzles/IntegersInACircle.lean
+++ b/MathPuzzles/IntegersInACircle.lean
@@ -14,6 +14,8 @@ import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.LinearCombination
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 There are 101 positive integers arranged in a circle.
 Suppose that the integers sum to 300.
@@ -56,6 +58,7 @@ lemma lemma2 {f : ZMod 101 → ℤ} (y : ZMod 101)
      · simp
   rw[h3]
 
+@[problem_statement]
 theorem integers_in_a_circle
     (a : ZMod 101 → ℤ)
     (ha : ∀ i, 1 ≤ a i)
diff --git a/MathPuzzles/Iran1998Q3.lean b/MathPuzzles/Iran1998Q3.lean
index d2657885..726f0724 100644
--- a/MathPuzzles/Iran1998Q3.lean
+++ b/MathPuzzles/Iran1998Q3.lean
@@ -1,7 +1,9 @@
 import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.MeanInequalities
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 Iranian Mathematical Olympiad 1998, problem 3
 
 Let x₁, x₂, x₃, x₄ be positive real numbers such that
@@ -37,6 +39,7 @@ lemma prod_pow' (S : Finset ℕ) (e : ℝ) (f : ℕ → ℝ) (hf : ∀ s ∈ S,
       exact mul_nonneg hs0 hsnn
     · exact (Real.mul_rpow hsnn hs0).symm
 
+@[problem_statement]
 theorem iran1998_q3
     (x : ℕ → ℝ)
     (x_positive : ∀ i, 0 < x i)
diff --git a/MathPuzzles/Iran1998Q9.lean b/MathPuzzles/Iran1998Q9.lean
index b94230a8..b5299e99 100644
--- a/MathPuzzles/Iran1998Q9.lean
+++ b/MathPuzzles/Iran1998Q9.lean
@@ -10,6 +10,8 @@ import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.NormedSpace.PiLp
 
+import MathPuzzles.Meta.Attributes
+
 /-
 Iranian Mathematical Olympiad 1998, Problem 9
 
@@ -31,6 +33,7 @@ lemma compute_norm (v : EuclideanSpace ℝ (Fin 3)) : ‖v‖ = Real.sqrt (∑i
   congr; ext
   rw [Real.norm_eq_abs, sq_abs]
 
+@[problem_statement]
 theorem iran1998_q9
     (x y z : ℝ)
     (hx : 1 < x)
diff --git a/MathPuzzles/KolmogorovStreams.lean b/MathPuzzles/KolmogorovStreams.lean
index 15c95ff9..36d1790d 100644
--- a/MathPuzzles/KolmogorovStreams.lean
+++ b/MathPuzzles/KolmogorovStreams.lean
@@ -9,7 +9,9 @@ import Mathlib.Data.Stream.Defs
 import Mathlib.Data.Stream.Init
 import Mathlib.Tactic.Ring
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 
 Puzzle referenced from this tweet: https://twitter.com/sigfpe/status/1474173467016589323
 
@@ -21,6 +23,10 @@ Problem: Suppose each (finite) word is either "decent" or "indecent". Given an i
 sequence of characters, can you always break it into finite words so that all of them
 except perhaps the first one belong to the same class?
 
+-/
+
+/-
+
 Answer: yes.
 
 -/
@@ -31,6 +37,7 @@ open Stream' BigOperators
 
 variable {α : Type}
 
+@[problem_setup]
 def break_into_words :
    (Stream' ℕ) → -- word lengths
    (Stream' α) → -- original sequence
@@ -79,6 +86,7 @@ lemma break_into_words_closed_form
           drop_drop, Finset.sum_range_succ']
       congr
 
+@[problem_statement]
 def all_same_class
     (is_decent : List α → Prop)
     (b : Stream' (List α))
@@ -213,6 +221,7 @@ lemma check_indecent_words
   intro j
   exact ((choose_indecent_words is_decent a h).nth j).h
 
+@[problem_statement]
 theorem kolmogorov_streams
     (is_decent : List α → Prop)
     (a : Stream' α)
diff --git a/MathPuzzles/Meta/Attributes.lean b/MathPuzzles/Meta/Attributes.lean
new file mode 100644
index 00000000..307ffa3b
--- /dev/null
+++ b/MathPuzzles/Meta/Attributes.lean
@@ -0,0 +1,38 @@
+import Lean.Elab.Command
+import Lean.Meta.Basic
+import Mathlib.Tactic.LabelAttr
+
+/-!
+Attributes to aid in "problem extraction".
+
+For the math problems that we archive, we aim to include proofs in-line.
+That presents a problem, however, if someone wants to try solving the
+problems without seeing the solutions.
+Therefore, we have "problem extraction" -- a means of stripping solutions.
+
+During problem extraction, all declarations are removed
+except those that have been tagged with one of the below attributes.
+-/
+
+open Lean Elab
+
+/--
+Indicates that a theorem is a problem statement. During problem extraction,
+the proof is replaced by a `sorry`.
+-/
+register_label_attr problem_statement
+
+/--
+Indicates that a declaration is required to set up a problem statement.
+During problem extraction, the declaration is kept completely intact.
+-/
+register_label_attr problem_setup
+
+/--
+Indicates that a declaration represents data that is intended to
+be filled in as part of a solution.
+During problem extraction, the body is replaced by a `sorry`.
+During judging, a human will inspect the filled-in body
+to see whether it is reasonable.
+-/
+register_label_attr solution_data
diff --git a/MathPuzzles/Meta/Frontend.lean b/MathPuzzles/Meta/Frontend.lean
new file mode 100644
index 00000000..b7df468d
--- /dev/null
+++ b/MathPuzzles/Meta/Frontend.lean
@@ -0,0 +1,238 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Lean.Elab.Frontend
+import Std.Util.TermUnsafe
+import Std.Data.MLList.Basic
+
+/-!
+# Compiling Lean sources to obtain `Environment`, `Message`s and `InfoTree`s.
+
+The main entry point is
+
+```
+def processInput (input : String) (env? : Option Environment := none)
+    (opts : Options := {}) (fileName : Option String := none) (info : Bool := true) :
+    IO (Environment × List Message × List InfoTree) :=
+  ...
+```
+
+which attempts to compile Lean source code, returning an `Environment`,
+along with any generated `Message`s and `InfoTree`s.
+
+The optional argument `env?` allows specifying an existing `Environment`, for partial compilation.
+If this is non-empty, then the source code may not contain any `import` statements.
+
+You may suppress the generation of `InfoTree`s using `info := false`.
+
+For finer-grained control of compilation, we define a `CompilationStep` structure
+which contains information about the results of each command.
+
+You can use `processInput'` to obtain a monadic lazy list of `CompilationStep`s.
+
+The functions `compileModule : Name → IO (List CompilationStep)` and
+`moduleInfoTrees : Name → IO (List InfoTree)` are useful for compiling single modules from source.
+-/
+
+set_option autoImplicit true
+
+open Lean Elab Frontend
+
+namespace Lean.PersistentArray
+
+/--
+Drop the first `n` elements of a `PersistentArray`, returning the results as a `List`.
+-/
+-- We can't remove the `[Inhabited α]` hypotheses here until
+-- `PersistentArray`'s `GetElem` instance also does.
+def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :=
+  List.range (t.size - n) |>.map fun i => t.get! (n + i)
+
+end Lean.PersistentArray
+
+namespace MLList
+
+/-- Run a lazy list in a `ReaderT` monad on some fixed state. -/
+partial def runReaderT [Monad m] (L : MLList (ReaderT ρ m) α) (r : ρ) : MLList m α :=
+  squash fun _ =>
+    return match ← (uncons L).run r with
+    | none => nil
+    | some (a, L') => cons a (L'.runReaderT r)
+
+/-- Run a lazy list in a `StateRefT'` monad on some initial state. -/
+partial def runStateRefT [Monad m] [MonadLiftT (ST ω) m] (L : MLList (StateRefT' ω σ m) α) (s : σ) :
+    MLList m α :=
+  squash fun _ =>
+    return match ← (uncons L).run s with
+    | (none, _) => nil
+    | (some (a, L'), s') => cons a (L'.runStateRefT s')
+
+end MLList
+
+namespace Lean.Elab.IO
+
+/--
+Results from processing a command.
+
+Contains the `Environment` before and after,
+the `src : Substring` and `stx : Syntax` of the command,
+and any `Message`s and `InfoTree`s produced while processing.
+-/
+structure CompilationStep where
+  src : Substring
+  stx : Syntax
+  before : Environment
+  after : Environment
+  msgs : List Message
+  trees : List InfoTree
+
+namespace CompilationStep
+
+/--
+Process one command, returning a `CompilationStep` and
+`done : Bool`, indicating whether this was the last command.
+-/
+def one : FrontendM (CompilationStep × Bool) := do
+  let s := (← get).commandState
+  let beforePos := (← get).cmdPos
+  let before := s.env
+  let done ← processCommand
+  let stx := (← get).commands.back
+  let src := ⟨(← read).inputCtx.input, beforePos, (← get).cmdPos⟩ -- FIXME this is incorrect
+  let s' := (← get).commandState
+  let after := s'.env
+  let msgs := s'.messages.msgs.drop s.messages.msgs.size
+  let trees := s'.infoState.trees.drop s.infoState.trees.size
+  return ({ src, stx, before, after, msgs, trees }, done)
+
+/-- Process all commands in the input. -/
+partial def all : FrontendM (List CompilationStep) := do
+  let (cmd, done) ← CompilationStep.one
+  if done then
+    return [cmd]
+  else
+    return cmd :: (← all)
+
+/-- Return all new `ConstantInfo`s added during the processed command. -/
+def diff (cmd : CompilationStep) : List ConstantInfo :=
+  cmd.after.constants.map₂.toList.filterMap
+    fun (c, i) => if cmd.before.constants.map₂.contains c then none else some i
+
+end CompilationStep
+
+/--
+Returns a monadic lazy list of `CompilationStep`s.
+This needs to be provided with initial state, see `compilationSteps`.
+-/
+partial def compilationSteps_aux :  MLList FrontendM CompilationStep :=
+  .squash fun _ => aux
+where
+  /-- Implementation of `compilationSteps_aux`.  -/
+  aux := do
+    let (cmd, done) ← CompilationStep.one
+    if done then
+      return .ofList [cmd]
+    else
+      return .cons cmd (← aux)
+
+/-- Return the the `CompilationStep`s, as a monadic lazy list in `IO`. -/
+def compilationSteps (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
+    (commandState : Command.State) : MLList IO CompilationStep :=
+  compilationSteps_aux.runReaderT { inputCtx }
+    |>.runStateRefT { commandState, parserState, cmdPos := parserState.pos }
+
+/--
+Process some text input, with or without an existing environment.
+If there is no existing environment, we parse the input for headers (e.g. import statements),
+and create a new environment.
+Otherwise, we add to the existing environment.
+Returns a list containing data about each processed command.
+
+Be aware that Lean does not support compiling multiple files in the same sessions.
+Often it works, but if the compiled files do anything complicated with initializers then
+nothing is gauranteed.
+-/
+def processInput' (input : String) (env? : Option Environment := none)
+    (opts : Options := {}) (fileName : Option String := none) (info : Bool := true) :
+    MLList IO CompilationStep := unsafe do
+  let fileName   := fileName.getD "<input>"
+  let inputCtx   := Parser.mkInputContext input fileName
+  let (parserState, commandState) ← match env? with
+  | none => do
+    enableInitializersExecution
+    let (header, parserState, messages) ← Parser.parseHeader inputCtx
+    let (env, messages) ← processHeader header opts messages inputCtx
+    pure (parserState, (Command.mkState env messages opts))
+  | some env => do
+    pure ({ : Parser.ModuleParserState }, Command.mkState env {} opts)
+  compilationSteps inputCtx parserState { commandState with infoState.enabled := info }
+
+/--
+Process some text input, with or without an existing environment.
+If there is no existing environment, we parse the input for headers (e.g. import statements),
+and create a new environment.
+Otherwise, we add to the existing environment.
+Returns the resulting environment, along with a list of messages and info trees.
+-/
+def processInput (input : String) (env? : Option Environment := none)
+    (opts : Options := {}) (fileName : Option String := none) (info : Bool := true) :
+    IO (Environment × List Message × List InfoTree) := do
+  let steps ← processInput' input env? opts fileName info |>.force
+  match steps.getLast? with
+  | none => throw <| IO.userError "No commands found in input."
+  | some { after, .. } =>
+    return (after, steps.bind CompilationStep.msgs, steps.bind CompilationStep.trees)
+
+open System
+
+-- TODO allow finding Lean 4 sources from the toolchain.
+def findLean (mod : Name) : IO FilePath := do
+  return FilePath.mk ((← findOLean mod).toString.replace "build/lib/" "") |>.withExtension "lean"
+
+/-- Implementation of `moduleSource`, which is the cached version of this function. -/
+def moduleSource' (mod : Name) : IO String := do
+  IO.FS.readFile (← findLean mod)
+
+initialize sourceCache : IO.Ref <| HashMap Name String ←
+  IO.mkRef .empty
+
+/-- Read the source code of the named module. The results are cached. -/
+def moduleSource (mod : Name) : IO String := do
+  let m ← sourceCache.get
+  match m.find? mod with
+  | some r => return r
+  | none => do
+    let v ← moduleSource' mod
+    sourceCache.set (m.insert mod v)
+    return v
+
+/-- Implementation of `compileModule`, which is the cached version of this function. -/
+def compileModule' (mod : Name) : MLList IO CompilationStep := do
+  Lean.Elab.IO.processInput' (← moduleSource mod) none {} (← findLean mod).toString
+
+initialize compilationCache : IO.Ref <| HashMap Name (List CompilationStep) ←
+  IO.mkRef .empty
+
+/--
+Compile the source file for the named module, returning the
+resulting environment, any generated messages, and all info trees.
+
+The results are cached, although be aware that compiling multiple files in the same session
+is unsupported, and may lead to exciting results:
+you should check all compiled files for error messages if attempting this.
+-/
+def compileModule (mod : Name) : IO (List CompilationStep) := do
+  let m ← compilationCache.get
+  match m.find? mod with
+  | some r => return r
+  | none => do
+    let v ← compileModule' mod |>.force
+    compilationCache.set (m.insert mod v)
+    return v
+
+/-- Compile the source file for the named module, returning all info trees. -/
+def moduleInfoTrees (mod : Name) : IO (List InfoTree) := do
+  let steps ← compileModule mod
+  return steps.bind (fun c => c.trees)
diff --git a/MathPuzzles/Poland1998Q4.lean b/MathPuzzles/Poland1998Q4.lean
index 32af0fdb..2a1c2a04 100644
--- a/MathPuzzles/Poland1998Q4.lean
+++ b/MathPuzzles/Poland1998Q4.lean
@@ -10,7 +10,9 @@ import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NormNum.Prime
 import Mathlib.Tactic.LibrarySearch
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 Polish Mathematical Olympiad 1998, Problem 4
 
 Prove that the sequence {a_n} defined by a_1 = 1 and
@@ -23,6 +25,7 @@ contains infinitely many integers divisible by 7.
 
 namespace Poland1998Q4
 
+@[problem_setup]
 def a : ℕ → ℕ
 | 0 => 1 -- unused dummy value
 | 1 => 1
@@ -293,6 +296,7 @@ lemma strengthen
       rw [heq] at hmp
       exact h (pn.succ) hmp
 
+@[problem_statement]
 theorem poland1998_q4 : (∀ N : ℕ, ∃ M : ℕ, N < M ∧ 7 ∣ a M) := by
   have he: 7 ∣ a 5 := by rw [show a 5 = 7 by rfl]
   exact strengthen can_get_a_later_one ⟨5, he⟩
diff --git a/MathPuzzles/Romania1998Q12.lean b/MathPuzzles/Romania1998Q12.lean
index 2db06945..28193919 100644
--- a/MathPuzzles/Romania1998Q12.lean
+++ b/MathPuzzles/Romania1998Q12.lean
@@ -2,7 +2,9 @@ import Mathlib.Data.Rat.Basic
 import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
-/-
+import MathPuzzles.Meta.Attributes
+
+/-!
 # Romanian Mathematical Olympiad 1998, Problem 12
 
 Find all functions u : ℝ → ℝ for which there exists a strictly monotonic
@@ -554,6 +556,11 @@ lemma romania1998_q12_mpr (u : ℝ → ℝ) :
            _ = (Real.exp (k * x) - 1) * Real.exp (k * y) +
                   (Real.exp (k * y) - 1) := by ring
 
+-- TODO define solution_set
+-- def solution_set : Set (ℝ → ℝ) :=
+-- { u | ∃ k : ℝ, ∀ x : ℝ, u x = Real.exp (k * x) }
+
+@[problem_statement]
 theorem romania1998_q12 (u : ℝ → ℝ) :
     (∃ f : ℝ → ℝ, (StrictMono f ∨ StrictAnti f)
           ∧ ∀ x y : ℝ, f (x + y) = f x * u y + f y) ↔
diff --git a/MathPuzzles/Russia1998Q42.lean b/MathPuzzles/Russia1998Q42.lean
index 0fdac1ce..21f415ae 100644
--- a/MathPuzzles/Russia1998Q42.lean
+++ b/MathPuzzles/Russia1998Q42.lean
@@ -6,6 +6,8 @@ Authors: David Renshaw
 
 import Mathlib.Data.Real.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-
  Russian Mathematical Olympiad 1998, problem 42
 
@@ -19,8 +21,11 @@ import Mathlib.Data.Real.Basic
 namespace Russia1998Q42
 
 variable (star : ℝ → ℝ → ℝ)
+
+@[problem_setup]
 local infixl:80 " ⋆ " => star
 
+@[problem_statement]
 theorem russia1998_q42
   (stardef : ∀ a b c, a ⋆ b ⋆ c = a + b + c) :
   (∀ a b, a ⋆ b = a + b) :=
diff --git a/MathPuzzles/UpperLowerContinuous.lean b/MathPuzzles/UpperLowerContinuous.lean
index 3ba6594c..a5dd392c 100644
--- a/MathPuzzles/UpperLowerContinuous.lean
+++ b/MathPuzzles/UpperLowerContinuous.lean
@@ -12,9 +12,10 @@ import Mathlib.Topology.MetricSpace.Basic
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Bases
 
-import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Linarith
 
+import MathPuzzles.Meta.Attributes
+
 /-
 Suppose f : ℝ -> ℝ is continuous in both the upper topology (where
 the basic open sets are half-open intervals (a, b]) and lower topology
@@ -102,15 +103,18 @@ def lower_intervals : Set (Set ℝ) := {s : Set ℝ | ∃ a b : ℝ, Set.Ico a b
 def open_intervals : Set (Set ℝ) := {s : Set ℝ | ∃ a b : ℝ, Set.Ioo a b = s}
 
 /-- Generate the toplogy on ℝ by intervals of the form (a, b]. -/
+@[problem_setup]
 def tᵤ : TopologicalSpace ℝ := TopologicalSpace.generateFrom upper_intervals
 
 /-- Generate the toplogy on ℝ by intervals of the form [a, b). -/
+@[problem_setup]
 def tₗ : TopologicalSpace ℝ := TopologicalSpace.generateFrom lower_intervals
 
 /-- This should be equivalent to the default instance
 for `TopologicalSpace ℝ`, which goes through `UniformSpace`, but for
 now I don't want to bother with proving that equivalence.
 -/
+@[problem_setup]
 def tₛ : TopologicalSpace ℝ := TopologicalSpace.generateFrom open_intervals
 
 -- activate the Continuous[t1, t2] notation
@@ -408,6 +412,7 @@ theorem monotone_of_upper_lower_continuous
     real_induction L1 L2 (@Set.left_mem_Ici _ _ (f z))
   exact h0 hz
 
+@[problem_statement]
 theorem properties_of_upper_lower_continuous
     (f : ℝ → ℝ)
     (huc : Continuous[tᵤ, tᵤ] f)
diff --git a/MathPuzzles/Usa1996Q1.lean b/MathPuzzles/Usa1996Q1.lean
index 5edbcfa6..87861736 100644
--- a/MathPuzzles/Usa1996Q1.lean
+++ b/MathPuzzles/Usa1996Q1.lean
@@ -7,6 +7,8 @@ Authors: David Renshaw
 import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 1996, Problem 1
 
@@ -18,6 +20,7 @@ for n ∈ {2,4,6,…,180} is 1/tan(π/180).
 namespace Usa1996Q1
 open BigOperators
 
+@[problem_statement]
 theorem usa1996Q1 :
     (1 / (n:ℝ)) * ∑ n in Finset.range 90, (2 * (n+1)) * Real.sin ((2 * (n+1)) * Real.pi / 180)
     = 1 / Real.tan (Real.pi / 180) := by
diff --git a/MathPuzzles/Usa1998Q1.lean b/MathPuzzles/Usa1998Q1.lean
index 1eeb5e06..1e88ad64 100644
--- a/MathPuzzles/Usa1998Q1.lean
+++ b/MathPuzzles/Usa1998Q1.lean
@@ -10,6 +10,8 @@ import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Data.Int.ModEq
 import Mathlib.Data.Finset.Interval
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 1998, Problem 1
 
@@ -49,6 +51,7 @@ lemma lemma2
   have h2 := le_of_eq hc.symm
   exact Iff.mp (Finset.subset_iff_eq_of_card_le h2) habc
 
+@[problem_statement]
 theorem usa1998_q1
     (a b : ℕ → ℕ)
     (ha : Finset.image a (Finset.Icc 1 999) ⊆ Finset.Icc 1 1998)
diff --git a/MathPuzzles/Usa1998Q3.lean b/MathPuzzles/Usa1998Q3.lean
index 584b4beb..1aaecb94 100644
--- a/MathPuzzles/Usa1998Q3.lean
+++ b/MathPuzzles/Usa1998Q3.lean
@@ -8,6 +8,8 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
 import Mathlib.Analysis.MeanInequalities
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 1998, Problem 3
 
@@ -134,6 +136,7 @@ lemma lemma2 (f : ℕ → ℝ) :
     rw[h6]
     ring
 
+@[problem_statement]
 theorem usa1998_q3
     (n : ℕ)
     (a : ℕ → ℝ)
diff --git a/MathPuzzles/Usa1998Q4.lean b/MathPuzzles/Usa1998Q4.lean
index df3bde7c..f0c830d5 100644
--- a/MathPuzzles/Usa1998Q4.lean
+++ b/MathPuzzles/Usa1998Q4.lean
@@ -7,6 +7,8 @@ Authors: David Renshaw
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Order.Bounds.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 1998, Problem 4
 
@@ -20,19 +22,24 @@ chessboard all one color.
 
 namespace Usa1998Q4
 
+@[problem_setup]
 def chessboard : Type := Fin 98 × Fin 98
 
+@[problem_setup]
 def coloring := chessboard → ZMod 2
 
+@[problem_setup]
 def all_same_color (f : coloring) : Prop :=
   ∃ c : ZMod 2, ∀ s : chessboard, f s = c
 
+@[problem_setup]
 structure Rectangle where
   x : ℕ
   y : ℕ
   width : ℕ
   height : ℕ
 
+@[problem_setup]
 def recolor_rect (f : coloring) (r : Rectangle) : coloring :=
 fun ⟨x, y⟩ ↦ if r.x ≤ x.val ∧
                 r.y ≤ y.val ∧
@@ -43,16 +50,19 @@ fun ⟨x, y⟩ ↦ if r.x ≤ x.val ∧
              else
                 f ⟨x, y⟩
 
+@[problem_setup]
 def start_coloring : coloring := fun ⟨x, y⟩ ↦ x.val + y.val
 
+@[problem_setup]
 def possible_num_clicks : Set ℕ :=
  { n : ℕ | ∃ rs : List Rectangle,
     (all_same_color (rs.foldl recolor_rect start_coloring) ∧
      rs.length = n) }
 
--- @[solution_data]
+@[solution_data]
 def min_clicks : ℕ := 98
 
+@[problem_statement]
 theorem usa1998_q4 : IsLeast possible_num_clicks min_clicks := by
   constructor
   · use (List.range 49).map
diff --git a/MathPuzzles/Usa1998Q5.lean b/MathPuzzles/Usa1998Q5.lean
index 35eafe38..5c5fbf3c 100644
--- a/MathPuzzles/Usa1998Q5.lean
+++ b/MathPuzzles/Usa1998Q5.lean
@@ -12,6 +12,8 @@ import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Ring
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 1998, Problem 5
 
@@ -119,6 +121,7 @@ lemma usa1998_q5_stronger (n : ℕ) :
             rw[ha2, hb2, hab] at Lmod'
             exact Int.dvd_of_emod_eq_zero Lmod'
 
+@[problem_statement]
 theorem usa1998_q5 (n : ℕ) (_hn : 2 ≤ n) :
     ∃ S : Finset ℤ,
        S.card = n ∧
diff --git a/MathPuzzles/Usa1999Q1.lean b/MathPuzzles/Usa1999Q1.lean
index 90a463d3..be3eb650 100644
--- a/MathPuzzles/Usa1999Q1.lean
+++ b/MathPuzzles/Usa1999Q1.lean
@@ -8,6 +8,8 @@ import Std.Data.List.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 USA Mathematical Olympiad 1999, Problem 1
 
@@ -22,8 +24,10 @@ Prove that at least (n²-2)/3 checkers have been placed on the board.
 
 namespace Usa1999Q1
 
+@[problem_setup]
 def checkerboard (n : ℕ) := Fin n × Fin n
 
+@[problem_setup]
 def adjacent {n : ℕ} : checkerboard n → checkerboard n → Prop
 | ⟨a1, a2⟩, ⟨b1, b2⟩ =>
   (a1.val = b1.val ∧ a2.val = b2.val + 1) ∨
@@ -31,6 +35,7 @@ def adjacent {n : ℕ} : checkerboard n → checkerboard n → Prop
   (a2.val = b2.val ∧ a1.val = b1.val + 1) ∨
   (a2.val = b2.val ∧ a1.val + 1 = b1.val )
 
+@[problem_statement]
 theorem usa1999_q1 (n : ℕ) (c : Finset (checkerboard n))
     (ha : ∀ x : checkerboard n, x ∈ c ∨ (∃ y ∈ c, adjacent x y))
     (hb : ∀ x ∈ c, ∀ y ∈ c,
diff --git a/MathPuzzles/Usa2000Q1.lean b/MathPuzzles/Usa2000Q1.lean
index f0bbfe79..a14e7046 100644
--- a/MathPuzzles/Usa2000Q1.lean
+++ b/MathPuzzles/Usa2000Q1.lean
@@ -8,6 +8,8 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Algebra.GroupPower.Lemmas
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 USA Mathematical Olympiad 2000, Problem 1
 
@@ -20,6 +22,7 @@ Show that there exist no very convex functions.
 
 namespace Usa2000Q1
 
+@[problem_statement]
 theorem usa2000_q1 :
     ¬∃ f : ℝ → ℝ,
       ∀ x y : ℝ, f ((x + y) / 2) + |x - y| ≤ (f x + f y) / 2 := by
diff --git a/MathPuzzles/Usa2001Q1.lean b/MathPuzzles/Usa2001Q1.lean
index 287a2a5f..ba563439 100644
--- a/MathPuzzles/Usa2001Q1.lean
+++ b/MathPuzzles/Usa2001Q1.lean
@@ -7,6 +7,8 @@ Authors: David Renshaw
 import Mathlib.Data.Finset.Card
 import Mathlib.Order.Bounds.Basic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 2001, Problem 1
 
@@ -19,6 +21,7 @@ for which this is possible.
 
 namespace Usa2001Q1
 
+@[problem_setup]
 def possible_num_colors : Set ℕ :=
 { n : ℕ | ∃ f : Fin 8 → Finset (Fin n),
     (∀ i, (f i).card = 6) ∧
@@ -26,9 +29,10 @@ def possible_num_colors : Set ℕ :=
       i ≠ j → x ∈ f i → y ∈ f i →
         (¬ (x ∈ f j ∧ y ∈ f j))) }
 
--- @[solution_data]
+@[solution_data]
 def min_colors : ℕ := 23
 
+@[problem_statement]
 theorem usa2001_q1 : IsLeast possible_num_colors min_colors := by
   constructor
   · sorry
diff --git a/MathPuzzles/Usa2002Q1.lean b/MathPuzzles/Usa2002Q1.lean
index 3064db30..2028d3b5 100644
--- a/MathPuzzles/Usa2002Q1.lean
+++ b/MathPuzzles/Usa2002Q1.lean
@@ -11,6 +11,8 @@ import Mathlib.Data.Finite.Basic
 
 import Mathlib.Tactic.IntervalCases
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 2002, Problem 1
 
@@ -28,6 +30,7 @@ red so that the following conditions hold:
 
 namespace Usa2002Q1
 
+@[problem_setup]
 inductive Color : Type where
 | red : Color
 | blue : Color
@@ -100,6 +103,7 @@ lemma usa2002q1_generalized
       -- Thus the induction is complete.
       sorry
 
+@[problem_statement]
 theorem usa2002q1
     {α : Type} [DecidableEq α] [Fintype α] (hs : Fintype.card α = 2002)
     (N : ℕ) (hN : N ≤ 2 ^ 2002) :
diff --git a/MathPuzzles/Usa2003Q1.lean b/MathPuzzles/Usa2003Q1.lean
index ab151293..50beb774 100644
--- a/MathPuzzles/Usa2003Q1.lean
+++ b/MathPuzzles/Usa2003Q1.lean
@@ -9,6 +9,8 @@ import Mathlib.Data.Nat.Parity
 
 import Mathlib.Tactic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 2003, Problem 1
 
@@ -40,6 +42,7 @@ lemma lemma2 (a b c : ℕ) (hb : 0 < b) (h : Nat.coprime a b) : ∃ k, k < b ∧
 
 lemma prime_five : Nat.Prime 5 := by norm_num
 
+@[problem_statement]
 theorem usa2003Q1 (n : ℕ) :
     ∃ m, ((Nat.digits 10 m).length = n ∧
           5^n ∣ m ∧
diff --git a/MathPuzzles/Usa2019Q1.lean b/MathPuzzles/Usa2019Q1.lean
index 4f7f54ca..fa3bb454 100644
--- a/MathPuzzles/Usa2019Q1.lean
+++ b/MathPuzzles/Usa2019Q1.lean
@@ -9,6 +9,8 @@ import Mathlib.Data.Nat.Parity
 
 import Mathlib.Tactic
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 2019, Problem 1
 
@@ -113,10 +115,10 @@ lemma lemma_2
   sorry
 
 
--- @[solution_data]
+@[solution_data]
 def solution_set : Set ℕ+ := { x : ℕ+ | Even x }
 
--- @[problem_statement]
+@[problem_statement]
 theorem usa2019Q1 (m : ℕ+) :
    m ∈ solution_set ↔
     (∃ f : ℕ+ → ℕ+,
diff --git a/MathPuzzles/Usa2022Q1.lean b/MathPuzzles/Usa2022Q1.lean
index 73f276d5..aa64009d 100644
--- a/MathPuzzles/Usa2022Q1.lean
+++ b/MathPuzzles/Usa2022Q1.lean
@@ -4,6 +4,8 @@ import Mathlib.Data.Fintype.Prod
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Positivity
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 # USA Mathematical Olympiad 2022, Problem 1
 
@@ -16,6 +18,7 @@ of the a + b chosen cells lie in the same row or column.
 
 namespace Usa2022Q1
 
+@[problem_statement]
 theorem usa2022q1
     (a b : ℕ)
     (ha : 0 < a)
diff --git a/MathPuzzles/ZeroesOnesAndTwos.lean b/MathPuzzles/ZeroesOnesAndTwos.lean
index 8aa01f3e..212478ef 100644
--- a/MathPuzzles/ZeroesOnesAndTwos.lean
+++ b/MathPuzzles/ZeroesOnesAndTwos.lean
@@ -9,6 +9,8 @@ import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Nat.Digits
 
+import MathPuzzles.Meta.Attributes
+
 /-!
 (From Mathematical Puzzles: A Connoisseur's Collection by Peter Winkler.)
 
@@ -55,6 +57,7 @@ lemma one_le_ten : (1 : ℕ) ≤ 10 := tsub_eq_zero_iff_le.mp rfl
 --
 -- Prove that n has a positive multiple whose representation contains only zeroes and ones.
 --
+@[problem_statement]
 theorem zeroes_and_ones
     (n : ℕ) : ∃ k : ℕ+, ∀ e ∈ (Nat.digits 10 (n * k)), e = 0 ∨ e = 1 := by
   obtain (hn0 : n = 0 ) | (hn : n > 0) := Nat.eq_zero_or_pos n
@@ -100,11 +103,13 @@ theorem zeroes_and_ones
   rw [List.mem_append, List.mem_replicate, List.mem_replicate] at he
   aesop
 
+@[problem_setup]
 def is_one_or_two : ℕ → Prop
 | 1 => True
 | 2 => True
 | _ => False
 
+@[problem_setup]
 def all_one_or_two (l : List ℕ) : Prop := ∀ e ∈ l, is_one_or_two e
 
 def prepend_one (n : ℕ) := 10 ^ (List.length (Nat.digits 10 n)) + n
@@ -288,6 +293,7 @@ lemma ones_and_twos_aux (n : ℕ) :
 --
 -- Prove that 2^n has a positive multiple whose representation contains only ones and twos.
 --
+@[problem_statement]
 theorem ones_and_twos (n : ℕ) : ∃ k : ℕ+, all_one_or_two (Nat.digits 10 (2^n * k)) := by
   cases' n with n
   · use 1; simp[all_one_or_two]; norm_cast
diff --git a/scripts/buildWebpage.lean b/scripts/buildWebpage.lean
index 45cfe769..3ba6f3b7 100644
--- a/scripts/buildWebpage.lean
+++ b/scripts/buildWebpage.lean
@@ -2,12 +2,17 @@ import Std.Data.String.Basic
 import Std.Tactic.Lint
 import Lean.Environment
 import Mathlib.Data.String.Defs
+import Mathlib.Tactic.LabelAttr
+import MathPuzzles.Meta.Attributes
+import MathPuzzles.Meta.Frontend
+import Lean.Meta.Basic
 
 open Lean Core Elab Command Std.Tactic.Lint
 
 structure PuzzleInfo where
   name : String
-  url : String
+  solutionUrl : String
+  problemUrl : String
   proved : Bool
 
 
@@ -33,7 +38,52 @@ def HEADER : String :=
  "<title>Math Puzzles in Lean 4</title>" ++
  "</head>"
 
+def getStubDecl (name : Name) (ty : Expr) : MetaM String := do
+  let msg ← withoutModifyingEnv <| withoutModifyingState do
+    let sig ← addMessageContext <| MessageData.ofPPFormat { pp := fun
+                | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name
+                | none     => unreachable!
+              }
+    let cmd := if ← Meta.isProp ty then "theorem" else "def"
+    m!"{cmd} {sig} := sorry\n".toString
+  pure msg
+
+def matchDecl : Syntax → CoreM (String.Pos × String.Pos)
+| `(command| $_:declModifiers theorem%$thm $_:declId $_:declSig :=%$colEq $_:term) => do
+    let .some startPos := thm.getPos? | throwError "thm syntax has no pos"
+    let .some endPos := colEq.getTailPos? | throwError "colEq syntax has no pos"
+    pure ⟨startPos, endPos⟩
+| `(command| $_:declModifiers def%$df $_:declId $_:optDeclSig :=%$colEq $_:term) => do
+    let .some startPos := df.getPos? | throwError "df syntax has no pos"
+    let .some endPos := colEq.getTailPos? | throwError "colEq syntax has no pos"
+    pure ⟨startPos, endPos⟩
+| _ => throwError "no match"
+
+def matchProblemSetup (stx: Syntax) : CoreM (String.Pos × String.Pos) := do
+  let .some endPos := stx.getTailPos? | throwError "no end pos"
+  match stx with
+  | `(command| $_:declModifiers abbrev%$ab $_:ident $_:declVal) => do
+      let .some startPos := ab.getPos? | throwError "ab syntax has no pos"
+      pure ⟨startPos, endPos⟩
+  | `(command| $_:declModifiers def%$df $_:declId $_:optDeclSig $_:declVal) => do
+      let .some startPos := df.getPos? | throwError "df syntax has no pos"
+      pure ⟨startPos, endPos⟩
+  | `(command| $_:declModifiers structure%$st $_:declId $[$ids:bracketedBinder]* where
+               $[$_:structCtor]? $_:structFields) => do
+      let .some startPos := st.getPos? | throwError "st syntax has no pos"
+      pure ⟨startPos, endPos⟩
+  | `(command| $_:declModifiers inductive%$st $_:declId $_:optDeclSig where
+               $[$_:ctor]* $[$_:computedFields]? $_:optDeriving) => do
+      let .some startPos := st.getPos? | throwError "st syntax has no pos"
+      pure ⟨startPos, endPos⟩
+
+  | _ => throwError "no match"
+
+
 unsafe def main (_args : List String) : IO Unit := do
+  IO.FS.createDirAll "_site"
+  IO.FS.createDirAll "_site/problems"
+
   let module := `MathPuzzles
   searchPathRef.set compileTimeSearchPath
 
@@ -41,14 +91,74 @@ unsafe def main (_args : List String) : IO Unit := do
     let ctx := {fileName := "", fileMap := default}
     let state := {env}
     Prod.fst <$> (CoreM.toIO · ctx state) do
+      let ⟨problem_statements,_⟩ ←
+        Lean.Meta.MetaM.run (Mathlib.Tactic.LabelAttr.labelled `problem_statement)
+      IO.println f!"problem statements: {problem_statements}"
+      let ⟨problem_setups,_⟩ ←
+        Lean.Meta.MetaM.run (Mathlib.Tactic.LabelAttr.labelled `problem_setup)
+      IO.println f!"problem setups: {problem_setups}"
+      let ⟨solution_datas,_⟩ ←
+        Lean.Meta.MetaM.run (Mathlib.Tactic.LabelAttr.labelled `solution_data)
+      IO.println f!"solution_datas: {solution_datas}"
+
       let mut infos : List PuzzleInfo := []
       let pkg := `MathPuzzles
       let modules := env.header.moduleNames.filter (pkg.isPrefixOf ·)
+      let baseurl := ((← IO.getEnv "GITHUB_PAGES_BASEURL").getD "")
+
       for m in modules do
-        if m ≠ pkg then do
+        if m ≠ pkg && m ≠ `MathPuzzles.Meta.Attributes then do
           let p ← findOLean m
-          let url := olean_path_to_github_url p.toString
+          let src ← Lean.Elab.IO.moduleSource m
+          let solutionUrl := olean_path_to_github_url p.toString
           IO.println s!"MODULE: {m}"
+          let steps ← Lean.Elab.IO.compileModule m
+          IO.println f!"number of steps = {steps.length}"
+          let problem_file := s!"problems/{m}.lean"
+          let problemUrl := s!"{baseurl}{problem_file}"
+          let h ← IO.FS.Handle.mk ("_site/" ++ problem_file) IO.FS.Mode.write
+          match steps with
+          | s :: _ =>
+            for im in s.before.header.imports do
+              if im.module ≠ "Init" && im.module ≠ `MathPuzzles.Meta.Attributes
+              then h.putStrLn s!"import {im}"
+            h.putStrLn ""
+          | [] => pure ()
+          for s in steps do
+             let csrc : String ← match s.stx.getPos?, s.stx.getTailPos? with
+             | .some pos, .some tailPos =>
+                pure s!"{(Substring.mk src pos tailPos).toString}\n"
+             | _, _ => throwError "failed to get source positions"
+             if s.diff.length = 0
+             then
+               if "/-!".isPrefixOf csrc
+               then h.putStrLn csrc
+               else if "/-".isPrefixOf csrc || "--".isPrefixOf csrc
+                    then pure ()
+                    else
+                      -- this includes things like `variables` and `namespace`
+                      h.putStrLn csrc
+             else
+               for c in s.diff do
+                 let name := c.toConstantVal.name
+
+                 if problem_statements.contains name
+                 then -- keep the type and replace the body with `sorry`
+                      let ⟨startPos, endPos⟩ ← matchDecl s.stx
+                      let decl1 := s!"{(Substring.mk src startPos endPos)} sorry\n"
+                      h.putStrLn decl1
+                 else if problem_setups.contains name
+                 then -- keep everything, but strip the attribute
+                      let ⟨startPos, endPos⟩ ← matchProblemSetup s.stx
+                      let decl1 := s!"{(Substring.mk src startPos endPos)}\n"
+                      h.putStrLn decl1
+                 else if solution_datas.contains name
+                 then -- keep the type and replace the body with `sorry`
+                      let ⟨startPos, endPos⟩ ← matchDecl s.stx
+                      let decl1 := s!"{(Substring.mk src startPos endPos)} sorry\n"
+                      h.putStrLn s!"/- @[solution_data] -/\n{decl1}"
+                 pure ()
+          h.flush
           let mut proved := true
           let decls ← getDeclsInPackage m
           for d in decls do
@@ -57,14 +167,14 @@ unsafe def main (_args : List String) : IO Unit := do
             | none => pure ()
             | some v => do
                  if v.hasSorry then proved := false
-          infos := ⟨m.toString.stripPrefix "MathPuzzles.", url, proved⟩  :: infos
+          infos := ⟨m.toString.stripPrefix "MathPuzzles.",
+                    solutionUrl, problemUrl, proved⟩ :: infos
       -- now write the file
       let num_proved := (infos.filter (·.proved)).length
       let commit_sha := ((← IO.getEnv "GITHUB_SHA").getD "GITHUB_SHA_env_var_not_found")
       let commit_url :=
         s!"https://github.com/dwrensha/math-puzzles-in-lean4/commit/{commit_sha}"
 
-      IO.FS.createDirAll "_site"
       let h ← IO.FS.Handle.mk "_site/index.html" IO.FS.Mode.write
       h.putStr HEADER
       h.putStr "<body>"
@@ -76,11 +186,13 @@ unsafe def main (_args : List String) : IO Unit := do
       h.putStr "<ul>"
       for info in infos.reverse do
         h.putStr "<li>"
+        h.putStr s!"<a href=\"{info.solutionUrl}\">"
         if info.proved then
           h.putStr "✅  "
         else
           h.putStr "❌  "
-        h.putStr s!"<a href=\"{info.url}\">{info.name}</a>"
+        h.putStr "</a>"
+        h.putStr s!"<a href=\"{info.problemUrl}\">{info.name}</a>"
         h.putStr "</li>"
       h.putStr "</ul>"
       h.putStr "</body></html>"