OP-0096OpenAlgebra

Andrews–Curtis conjecture

Can every balanced presentation of the trivial group be reduced to the standard one by elementary relator moves?

Source-reported statusAs of 2026-07-31Source & evidence ↓

Read original source ↗ 0 Submit progress Lean 4 ↓Discussion (0)

Problem statement

Let $\langle x_1,\ldots,x_n\mid r_1,\ldots,r_n\rangle$ be a balanced presentation of the trivial group. Can its relators always be transformed to $(x_1,\ldots,x_n)$ using finitely many of the following moves?

Invert a relator.
Multiply one relator by another.
Conjugate a relator by any word in the generators.

A bounded computational search that finds no sequence does not establish a counterexample. This question concerns the original conjecture; stabilized variants allowing extra generator–relator pairs are distinct.

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Progress & source assessment

TheoremDB’s 31 July 2026 packet reports the conjecture for thickenable balanced presentations as a known special case, citing Lackenby. Its recorded work does not resolve the unrestricted conjecture.

References

[1]TheoremDB P48, Andrews–Curtis conjecture. Snapshot 31 July 2026. link

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.