feat: add Novikov unsolvable word problem eval problem

LeanEval/GroupTheory/NovikovUnsolvable.lean

@@ -0,0 +1,44 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace GroupTheory
+namespace NovikovUnsolvableProblem
+
+/-!
+# Novikov's theorem: undecidability of the word problem
+
+There exists a finitely presented group whose word problem is
+undecidable. P.S. Novikov 1955 / W.W. Boone 1958. §122 in Knill's
+*Some Fundamental Theorems in Mathematics*.
+
+The standard encoding: a word in the generators `g₁, …, gₙ` and their
+inverses is `List (Fin n × Bool)`, which is `Primcodable`. The word
+problem of a finite presentation `φ : FreeGroup (Fin n) →* G` is the
+predicate "`w` represents the identity of `G`", and solvability is
+`ComputablePred` of that predicate. Novikov's theorem asserts the
+existence of `n` and a finite relator set `rels ⊆ FreeGroup (Fin n)`
+for which the canonical surjection
+`PresentedGroup.mk rels : FreeGroup (Fin n) →* PresentedGroup rels`
+has *no* such algorithm.
+-/
+
+/-- The word problem of a finite presentation `φ` is **solvable** when
+the predicate "the word `w` represents the identity of `G`" is
+decidable by an algorithm. -/
+def WordProblemSolvable {G : Type*} [Group G] {n : ℕ}
+    (φ : FreeGroup (Fin n) →* G) : Prop :=
+  ComputablePred (fun w : List (Fin n × Bool) => φ (FreeGroup.mk w) = 1)
+
+/-- **Novikov's theorem** (P.S. Novikov 1955; independently W.W. Boone
+1958). There exists a finite presentation with undecidable word
+problem. -/
+@[eval_problem]
+theorem novikov_unsolvable :
+    ∃ (n : ℕ) (rels : Set (FreeGroup (Fin n))),
+      rels.Finite ∧ ¬ WordProblemSolvable (PresentedGroup.mk rels) := by
+  sorry
+
+end NovikovUnsolvableProblem
+end GroupTheory
+end LeanEval

manifests/problems/novikov_unsolvable.toml

@@ -0,0 +1,9 @@
+id = "novikov_unsolvable"
+title = "Novikov's theorem: the word problem is undecidable for finitely presented groups"
+test = false
+module = "LeanEval.GroupTheory.NovikovUnsolvable"
+holes = ["novikov_unsolvable"]
+submitter = "Kim Morrison"
+notes = "There exists a finitely presented group with undecidable word problem. Concretely: some n and a finite relator set rels ⊆ FreeGroup (Fin n) for which the canonical surjection `PresentedGroup.mk rels` admits no `ComputablePred` decision procedure for `w ↦ φ (FreeGroup.mk w) = 1`. Pure existence of a pathological finite presentation; the negation (every finite presentation has solvable word problem) was disproved by Novikov 1955 and independently by Boone 1958. §122 of Knill's *Some Fundamental Theorems in Mathematics*."
+source = "P.S. Novikov, 'On the algorithmic unsolvability of the word problem in group theory', Trudy Mat. Inst. Steklov. 44 (1955) 1–143 (Russian); W.W. Boone, 'The word problem', Ann. of Math. (2) 70 (1959) 207–265 (announced 1958). §122 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "Novikov and Boone construct a finite presentation of a group whose word problem encodes the halting problem of a universal Turing machine. (1) Encode a Turing machine M whose halting problem is undecidable as a finitely presented **semigroup**: a fixed list of rewriting rules whose word problem mirrors halting. (2) Lift the semigroup presentation to a finitely presented **group** by Boone's machinery using HNN extensions and Britton's lemma, preserving the equivalence: the question 'does M halt on input x' becomes 'does the word w_x equal 1 in the constructed group G'. (3) Since the halting problem is undecidable, so is the word problem of G; G is finitely presented by construction. Mathlib v4.30 has `FreeGroup`, `PresentedGroup`, `Group.IsFinitelyPresented`, HNN extensions (`Mathlib/GroupTheory/HNNExtension.lean`, including Britton's lemma as `HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range`), and the full `ComputablePred` / `Computable` / `Partrec` / `Nat.Partrec.Code` stack, but no Turing-machine-to-finitely-presented-group simulation and no Novikov / Boone unsolvability result."