diff --git a/LeanEval.lean b/LeanEval.lean
index dc4a846e8..42d89caa0 100644
--- a/LeanEval.lean
+++ b/LeanEval.lean
@@ -16,3 +16,4 @@ import LeanEval.NumberTheory.Lagarias
 import LeanEval.NumberTheory.SmallHouse
 import LeanEval.Topology.CerfGammaFour
 import LeanEval.Topology.HomotopyGroups
+import LeanEval.Topology.SmaleConjecture
diff --git a/LeanEval/Topology/SmaleConjecture.lean b/LeanEval/Topology/SmaleConjecture.lean
new file mode 100644
index 000000000..1b0f6cd7f
--- /dev/null
+++ b/LeanEval/Topology/SmaleConjecture.lean
@@ -0,0 +1,89 @@
+import Mathlib.Geometry.Manifold.Diffeomorph
+import Mathlib.Geometry.Manifold.Instances.Sphere
+import Mathlib.Geometry.Manifold.Instances.Real
+import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
+import Mathlib.LinearAlgebra.UnitaryGroup
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+/-!
+# Smale conjecture (Hatcher, 1983), relative parameterized form
+
+Hatcher's theorem says the inclusion `O(4) ↪ Diff(S³)` (restriction of the linear action
+on ℝ⁴) is a homotopy equivalence of topological spaces. Stating it in that form would
+require mathlib to carry the C^∞ topology on `Diffeomorph S³ S³`, which it does not yet
+have.
+
+We state the equivalent **relative parameterized** form: for every compact smooth
+manifold-with-boundary X and every smooth family of self-diffeomorphisms
+`F : X × S³ → S³` whose restriction to `∂X × S³` already comes from a continuous map
+`ψ_bdry : ∂X → O(4)` (acting by the linear action), there is a continuous extension
+`ψ : X → O(4)` with `ψ|∂X = ψ_bdry` and a smooth isotopy rel `∂X` from `F` to the
+family induced by `ψ`.
+
+For `X = D^k`, `∂X = S^{k-1}`, this says `π_k(Diff(S³), O(4)) = 0` for all `k ≥ 0`,
+which (modulo smoothing theory translating between smooth families parameterized by X
+and continuous maps `X → Diff(S³)` with the C^∞ topology) is equivalent to
+`O(4) ↪ Diff(S³)` being a homotopy equivalence.
+
+The Cerf case `X = pt` (so `∂X = ∅`, the relative hypothesis is vacuous) is
+Cerf's theorem Γ₄ = 0 (see `CerfGammaFour.lean`).
+
+**Desired future improvement.** Once mathlib gains a C^∞ topology on `Diffeomorph M N`
+(making it a topological group, with smooth families ↔ continuous maps into it), this
+statement should be rewritten in the direct form: the continuous group homomorphism
+`O(4) ↪ Diff(S³)` is a homotopy equivalence of topological spaces. Until then, the
+relative parameterized form below is the most faithful statement available.
+-/
+
+/-- **Smale conjecture (Hatcher 1983), relative parameterized form.**
+For every compact smooth manifold-with-boundary `X` and every smooth family `F` of
+self-diffeomorphisms of `S³` parameterized by `X` whose boundary restriction already
+factors through the linear action of `O(4)`, there is a smooth isotopy of `F`, rel
+`∂X`, to a family fully factoring through `O(4)`. -/
+@[eval_problem]
+theorem smale_conjecture
+    {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  sorry
+
+end Topology
+end LeanEval
diff --git a/generated/index.json b/generated/index.json
index c987c1dec..55b4b6896 100644
--- a/generated/index.json
+++ b/generated/index.json
@@ -151,5 +151,104 @@
     "module": "LeanEval.Topology.HomotopyGroups",
     "theorem": "pi_succ_sphere_n_mulEquiv_zmod_two",
     "generated_path": "generated/pi_succ_sphere_n_mulEquiv_zmod_two"
+  },
+  {
+    "id": "substInv_X_sub_X_sq_eq_catalan",
+    "title": "Catalan generating function via compositional inversion",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Combinatorics.CatalanSubstInv",
+    "theorem": "substInv_X_sub_X_sq_eq_catalan",
+    "generated_path": "generated/substInv_X_sub_X_sq_eq_catalan"
+  },
+  {
+    "id": "isStarNormal_mul_of_commute",
+    "title": "Product of commuting normal elements is normal",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Algebra.NormalProduct",
+    "theorem": "isStarNormal_mul_of_commute",
+    "generated_path": "generated/isStarNormal_mul_of_commute"
+  },
+  {
+    "id": "posSemidef_map_exp",
+    "title": "Entrywise exponential of a PSD matrix is PSD",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.LinearAlgebra.EntrywiseExpPSD",
+    "theorem": "posSemidef_map_exp",
+    "generated_path": "generated/posSemidef_map_exp"
+  },
+  {
+    "id": "mulCayley_connected_iff_closure_eq_top",
+    "title": "Cayley graph connected iff generators generate the group",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Combinatorics.CayleyConnected",
+    "theorem": "mulCayley_connected_iff_closure_eq_top",
+    "generated_path": "generated/mulCayley_connected_iff_closure_eq_top"
+  },
+  {
+    "id": "oppenheim_inequality",
+    "title": "Oppenheim's inequality for Hadamard products",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.LinearAlgebra.Oppenheim",
+    "theorem": "oppenheim_inequality",
+    "generated_path": "generated/oppenheim_inequality"
+  },
+  {
+    "id": "symAction_range_eq_centralizer_glAction",
+    "title": "Schur-Weyl duality: S_k image equals centralizer of GL(V) image",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.SchurWeyl",
+    "theorem": "symAction_range_eq_centralizer_glAction",
+    "generated_path": "generated/symAction_range_eq_centralizer_glAction"
+  },
+  {
+    "id": "glAction_range_eq_centralizer_symAction",
+    "title": "Schur-Weyl duality: GL(V) image equals centralizer of S_k image",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.SchurWeyl",
+    "theorem": "glAction_range_eq_centralizer_symAction",
+    "generated_path": "generated/glAction_range_eq_centralizer_symAction"
+  },
+  {
+    "id": "g2_irrep_tensor_square_decomp",
+    "title": "Tensor square decomposition of a 64-dim irreducible g\u2082-representation",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.ExceptionalLieTensorSquare",
+    "theorem": "g2_irrep_tensor_square_decomp",
+    "generated_path": "generated/g2_irrep_tensor_square_decomp"
+  },
+  {
+    "id": "e8_irrep_tensor_square_decomp",
+    "title": "Tensor square decomposition of a 779247-dim irreducible e\u2088-representation",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.ExceptionalLieTensorSquare",
+    "theorem": "e8_irrep_tensor_square_decomp",
+    "generated_path": "generated/e8_irrep_tensor_square_decomp"
+  },
+  {
+    "id": "cerf_gamma_four",
+    "title": "Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Topology.CerfGammaFour",
+    "theorem": "cerf_gamma_four",
+    "generated_path": "generated/cerf_gamma_four"
+  },
+  {
+    "id": "smale_conjecture",
+    "title": "Smale conjecture (Hatcher) in relative parameterized form",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Topology.SmaleConjecture",
+    "theorem": "smale_conjecture",
+    "generated_path": "generated/smale_conjecture"
   }
 ]
diff --git a/generated/pi1_circle_mulEquiv_int/lakefile.toml b/generated/pi1_circle_mulEquiv_int/lakefile.toml
index 042fd1bca..f9944ea78 100644
--- a/generated/pi1_circle_mulEquiv_int/lakefile.toml
+++ b/generated/pi1_circle_mulEquiv_int/lakefile.toml
@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"
diff --git a/generated/pi3_sphere_two_mulEquiv_int/lakefile.toml b/generated/pi3_sphere_two_mulEquiv_int/lakefile.toml
index 72c279e1f..7198faed2 100644
--- a/generated/pi3_sphere_two_mulEquiv_int/lakefile.toml
+++ b/generated/pi3_sphere_two_mulEquiv_int/lakefile.toml
@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"
diff --git a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/lakefile.toml b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/lakefile.toml
index 6e1d24c89..e731a74e1 100644
--- a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/lakefile.toml
+++ b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/lakefile.toml
@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"
diff --git a/generated/pin_sphere_n_mulEquiv_int/lakefile.toml b/generated/pin_sphere_n_mulEquiv_int/lakefile.toml
index 8f8b25881..f1c2aadfa 100644
--- a/generated/pin_sphere_n_mulEquiv_int/lakefile.toml
+++ b/generated/pin_sphere_n_mulEquiv_int/lakefile.toml
@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"
diff --git a/generated/smale_conjecture/Challenge.lean b/generated/smale_conjecture/Challenge.lean
new file mode 100644
index 000000000..396ed8c73
--- /dev/null
+++ b/generated/smale_conjecture/Challenge.lean
@@ -0,0 +1,41 @@
+import Mathlib
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+theorem smale_conjecture {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  sorry
diff --git a/generated/smale_conjecture/README.md b/generated/smale_conjecture/README.md
new file mode 100644
index 000000000..386ac1e6e
--- /dev/null
+++ b/generated/smale_conjecture/README.md
@@ -0,0 +1,25 @@
+# `smale_conjecture`
+
+Smale conjecture (Hatcher) in relative parameterized form
+
+- Problem ID: `smale_conjecture`
+- Test Problem: no
+- Submitter: Kim Morrison
+- Notes: Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform rel boundary to a family fully factoring through O(4)). Mathlib does not yet carry the C-infinity topology on Diffeomorph, which would be needed for the direct homotopy-equivalence formulation.
+- Source: A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983).
+- Informal solution: Hatcher proves Diff(S3) is homotopy equivalent to O(4) by analyzing configurations of 2-spheres in S3 (the bigon criterion) and deducing by induction that every self-diffeomorphism is isotopic to a linear one, with all higher parameterized versions handled by the same incompressible-surface machinery.
+
+Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the
+trusted benchmark and fixed by the repository.
+
+Write your solution in `Submission.lean` and any additional local modules under
+`Submission/`.
+
+Participants may use Mathlib freely. Any helper code not already available in
+Mathlib must be inlined into the submission workspace.
+
+Multi-file submissions are allowed through `Submission.lean` and additional local
+modules under `Submission/`.
+
+`lake test` runs comparator for this problem. The command expects a comparator
+binary in `PATH`, or in the `COMPARATOR_BIN` environment variable.
diff --git a/generated/smale_conjecture/Solution.lean b/generated/smale_conjecture/Solution.lean
new file mode 100644
index 000000000..f100700fa
--- /dev/null
+++ b/generated/smale_conjecture/Solution.lean
@@ -0,0 +1,42 @@
+import Mathlib
+import Submission
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+theorem smale_conjecture {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  exact Submission.smale_conjecture X F F' hF hF' hFinv₁ hFinv₂ ψ_bdry hψ_bdry_cont hF_bdry
diff --git a/generated/smale_conjecture/Submission.lean b/generated/smale_conjecture/Submission.lean
new file mode 100644
index 000000000..2cb8f5d1d
--- /dev/null
+++ b/generated/smale_conjecture/Submission.lean
@@ -0,0 +1,46 @@
+import Mathlib
+import Submission.Helpers
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+namespace Submission
+
+theorem smale_conjecture {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  sorry
+
+end Submission
diff --git a/generated/smale_conjecture/Submission/Helpers.lean b/generated/smale_conjecture/Submission/Helpers.lean
new file mode 100644
index 000000000..1561e7c8a
--- /dev/null
+++ b/generated/smale_conjecture/Submission/Helpers.lean
@@ -0,0 +1,3 @@
+namespace Submission.Helpers
+
+end Submission.Helpers
diff --git a/generated/smale_conjecture/WorkspaceTest.lean b/generated/smale_conjecture/WorkspaceTest.lean
new file mode 100644
index 000000000..ecb65777d
--- /dev/null
+++ b/generated/smale_conjecture/WorkspaceTest.lean
@@ -0,0 +1,38 @@
+import Lean
+
+open Lean
+
+def comparatorExists (comparatorBin : String) : IO Bool := do
+  if comparatorBin.contains '/' then
+    return (← System.FilePath.pathExists comparatorBin)
+  try
+    let child ← IO.Process.spawn {
+      cmd := "sh"
+      args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin]
+    }
+    let exitCode ← child.wait
+    return exitCode == 0
+  catch _ =>
+    return false
+
+def main : IO UInt32 := do
+  let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
+  if !(← comparatorExists comparatorBin) then
+    IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
+    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
+    pure 1
+  else
+    try
+      let child ← IO.Process.spawn {
+        cmd := "lake"
+        args := #["env", comparatorBin, "config.json"]
+      }
+      let exitCode ← child.wait
+      pure exitCode
+    catch err =>
+      IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
+      IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+      IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export."
+      IO.eprintln s!"Original error: {err}"
+      pure 1
diff --git a/generated/smale_conjecture/config.json b/generated/smale_conjecture/config.json
new file mode 100644
index 000000000..956e55b54
--- /dev/null
+++ b/generated/smale_conjecture/config.json
@@ -0,0 +1,13 @@
+{
+  "challenge_module": "Challenge",
+  "solution_module": "Solution",
+  "theorem_names": [
+    "smale_conjecture"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ],
+  "enable_nanoda": false
+}
diff --git a/generated/smale_conjecture/lakefile.toml b/generated/smale_conjecture/lakefile.toml
new file mode 100644
index 000000000..f511865a0
--- /dev/null
+++ b/generated/smale_conjecture/lakefile.toml
@@ -0,0 +1,24 @@
+name = "smale_conjecture"
+testDriver = "workspace_test"
+defaultTargets = ["Challenge", "Solution", "Submission"]
+
+[leanOptions]
+autoImplicit = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "50d5513e83c"
+
+[[lean_lib]]
+name = "Challenge"
+
+[[lean_lib]]
+name = "Solution"
+
+[[lean_lib]]
+name = "Submission"
+
+[[lean_exe]]
+name = "workspace_test"
+root = "WorkspaceTest"
diff --git a/generated/smale_conjecture/lean-toolchain b/generated/smale_conjecture/lean-toolchain
new file mode 100644
index 000000000..e7e267fe4
--- /dev/null
+++ b/generated/smale_conjecture/lean-toolchain
@@ -0,0 +1,2 @@
+leanprover/lean4:v4.30.0-rc1
+
diff --git a/manifests/problems.toml b/manifests/problems.toml
index 6f1056815..99955c2a0 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -296,3 +296,14 @@ submitter = "Kim Morrison"
 notes = "Cerf's 1968 theorem, the X = point (unparameterized) case of the Smale conjecture. Stated as the existence of a smooth isotopy [0,1] x S3 -> S3 from f to a linear isometry, witnessed by a smooth slice-inverse to encode the diffeomorphism property of each slice without needing a topology on Diffeomorph."
 source = "J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968)."
 informal_solution = "Cerf's original proof uses pseudo-isotopy theory: a self-diffeomorphism of S3 extends to a pseudo-isotopy of D4, and Cerf's theorem on the triviality of pi_0 of the pseudo-isotopy space in dimension 4 implies the extension is isotopic to a genuine isotopy. Hatcher (1983) reproved this as a corollary of the full Smale conjecture using configurations of 2-spheres."
+
+[[problem]]
+id = "smale_conjecture"
+title = "Smale conjecture (Hatcher) in relative parameterized form"
+test = false
+module = "LeanEval.Topology.SmaleConjecture"
+theorem = "smale_conjecture"
+submitter = "Kim Morrison"
+notes = "Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform rel boundary to a family fully factoring through O(4)). Mathlib does not yet carry the C-infinity topology on Diffeomorph, which would be needed for the direct homotopy-equivalence formulation."
+source = "A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983)."
+informal_solution = "Hatcher proves Diff(S3) is homotopy equivalent to O(4) by analyzing configurations of 2-spheres in S3 (the bigon criterion) and deducing by induction that every self-diffeomorphism is isotopic to a linear one, with all higher parameterized versions handled by the same incompressible-surface machinery."