Dixmiers Conjecture

### What is the conjecture

The Dixmier conjecture concerns endomorphisms of the Weyl algebra. Let $k$ be a field of characteristic zero, and let $A_1 = k\langle x, y \mid yx - xy = 1 \rangle$ denote the first Weyl algebra over $k$. The conjecture states that every endomorphism of $A_1$ is an automorphism. Equivalently, if $\phi: A_1 \to A_1$ is a ring homomorphism, then $\phi$ is bijective.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Dixmier_conjecture, https://arxiv.org/abs/2410.06959, https://arxiv.org/abs/2210.00257, https://arxiv.org/abs/math/0512171

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-01-22)

The Weyl algebra $A_1$ is not yet formalized in Mathlib. While Mathlib has comprehensive support for polynomial rings and noncommutative algebra basics (via the Algebra.RingQuot and related modules), the specific construction and properties of the Weyl algebra as a quotient of the free associative algebra would need to be developed. Additionally, formalizing the statement requires robust definitions of endomorphisms and automorphisms of noncommutative rings, which exist in Mathlib but would need to be specialized to this context. The proof strategy (which may involve graded algebra structures or filtrations) would require additional infrastructure. Significant new theory development is needed to set up the Weyl algebra and establish its fundamental properties before attempting the conjecture.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-16

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

Start by reviewing Mathlib's Algebra.RingQuot and related polynomial and noncommutative algebra modules, then consult the cited sources for the precise conjecture. Done requires developing the Weyl algebra infrastructure and formalizing the statement that every endomorphism of it is an automorphism; no repository file or test is named.

Written by the indexing model from the issue text.