Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Novikov-Boone: some finitely presented group has unsolvable word problem
Statement
There exists a finitely presented group whose word problem is unsolvable.
Remarks
This is the fixed-presentation form of the classical Novikov-Boone theorem. It already says that one particular finitely presented group has no decision algorithm for triviality of words; it is not merely a statement about varying the presentation as part of the input.
Depends on
Used by
- FALSE: an unsolvable word problem means no individual word can be decided False statement
- FALSE: every finitely presented group has solvable word problem False statement
- FALSE: recursively enumerable trivial words already give a decision algorithm False statement
- FALSE: the Novikov-Boone theorem proves only the uniform problem is unsolvable False statement
- Adian-Rabin: every Markov property is undecidable on finite presentations Remark
Dependency tree · two levels
2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Charles F. Miller III, Decision Problems for Groups - Survey and Reflections (standard reference, not scraped)