feat: add Novikov unsolvable word problem eval problem#383
Merged
Hidden character warning
The head ref may contain hidden characters: "knill-\u00a7122-novikov-unsolvable"
Conversation
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Codex review of PR #383 confirmed faithfulness of the formal statement (PresentedGroup.mk is mathlib's canonical quotient; rels.Finite correctly encodes finite presentation; degenerate trivial-group rels cannot witness the existential since trivial groups have computable word problem) and caught a real factual error: my manifest claimed mathlib has "no HNN extensions, no Britton's lemma". Mathlib v4.30 actually does have both — `Mathlib/GroupTheory/HNNExtension.lean' including Britton's lemma as `HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range'. Updated the manifest informal_solution to reflect reality: the missing piece is the Boone–Novikov simulation of Turing machines as finitely presented groups, not the HNN-extension machinery itself. Also fixed backtick typos in the manifest notes (`...' → `...`). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
kim-em
added a commit
that referenced
this pull request
Jun 3, 2026
Codex review of PR #384 confirmed faithfulness of the formal statement (existential shape correct; IsSimpleGroup includes Nontrivial so trivial-presentation witnesses are excluded; no vacuous-truth exploit) and caught two real errors. (1) My prior text claimed Higman's 1951 group was finitely presented and simple; in fact the 1951 paper constructs a finitely *generated* infinite simple group as a simple quotient of the four-generator "chain of squarings" group with no nontrivial finite quotients — the simple quotient need not be finitely presented. The first infinite finitely-presented simple groups are the Higman–Thompson groups G_{n,r} from Higman's 1974 monograph. Rewrote docstring + manifest accordingly. (2) Same HNN/Britton fix as #383: mathlib v4.30 DOES have HNN extensions and Britton's lemma in `Mathlib/GroupTheory/HNNExtension.lean'; corrected the "mathlib lacks X" list. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
kim-em
added a commit
that referenced
this pull request
Jun 3, 2026
#384) * feat: add Higman infinite finitely-presented simple group eval problem Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix: correct 1951-vs-1974 attribution + mathlib HNN claim on §122 Higman Codex review of PR #384 confirmed faithfulness of the formal statement (existential shape correct; IsSimpleGroup includes Nontrivial so trivial-presentation witnesses are excluded; no vacuous-truth exploit) and caught two real errors. (1) My prior text claimed Higman's 1951 group was finitely presented and simple; in fact the 1951 paper constructs a finitely *generated* infinite simple group as a simple quotient of the four-generator "chain of squarings" group with no nontrivial finite quotients — the simple quotient need not be finitely presented. The first infinite finitely-presented simple groups are the Higman–Thompson groups G_{n,r} from Higman's 1974 monograph. Rewrote docstring + manifest accordingly. (2) Same HNN/Britton fix as #383: mathlib v4.30 DOES have HNN extensions and Britton's lemma in `Mathlib/GroupTheory/HNNExtension.lean'; corrected the "mathlib lacks X" list. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds Novikov's theorem (P.S. Novikov 1955, independently W.W. Boone 1958) as an eval problem: there exists a finitely presented group with undecidable word problem.
The Lean statement is
∃ n (rels : Set (FreeGroup (Fin n))), rels.Finite ∧ ¬ WordProblemSolvable (PresentedGroup.mk rels). Pure existence of a pathological finite presentation; the negation (every finite presentation has solvable word problem) was disproved by Novikov and Boone.WordProblemSolvableis computability-genuine —ComputablePred (fun w : List (Fin n × Bool) => φ (FreeGroup.mk w) = 1), captured by mathlib'sComputablePred/Computablestack.The classical proof simulates a universal Turing machine: encode the halting problem as a finitely presented semigroup whose word problem mirrors halting, then lift the semigroup presentation to a finitely presented group via Boone's HNN-extension machinery (using Britton's lemma to prove the lift preserves non-equivalence). Mathlib v4.30 has
FreeGroup,PresentedGroup,Group.IsFinitelyPresented, the full computability stack (Nat.Partrec.Code,Partrec,Computable,ComputablePred), HNN extensions (Mathlib/GroupTheory/HNNExtension.lean— including Britton's lemma asHNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range), but no Turing-machine-to-finitely-presented-group simulation and no Novikov / Boone unsolvability result.§122 of Knill's Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).
🤖 Prepared with Claude+Codex+Aristotle