Cancellation Conjecture

### What is the conjecture

Let $k$ be an algebraically closed field and let $C = \mathbb{A}^1_k$ denote the affine line over $k$. The **Cancellation Conjecture** states that if $X$ is an affine variety over $k$ such that $X \times C \cong \mathbb{A}^{m+1}$ for some positive integer $m$, then $X \cong \mathbb{A}^m$. In other words, if a product of an affine variety with the affine line is isomorphic to affine $(m+1)$-space, then that variety must be isomorphic to affine $m$-space. This conjecture is proven for $m \leq 2$ but remains open for $m > 2$.

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

**Sources:**
- https://en.wikipedia.org/wiki/Cancellation_problem, https://mathoverflow.net/questions/tagged/cancellation-conjecture, https://arxiv.org/abs/1111.4065

### Prerequisites needed

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

Formalizing the Cancellation Conjecture requires substantial infrastructure in algebraic geometry that is partially present in Mathlib. The core concepts of affine varieties, isomorphisms of varieties, and polynomial rings are available or can be built on existing structures. However, the precise definition of affine varieties as objects (schemes or algebraic varieties in the classical sense), the notion of isomorphism in the category of affine varieties, and properties specific to affine space need careful formalization. While Mathlib has schemes, developing the classical algebraic geometry setting with explicit algebraic varieties and their properties would require moderate additional definitional work beyond what is currently available, particularly the characterization of affine $n$-space and its uniqueness properties.

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

* ams-14
* ams-13

### 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 existing formalized conjectures in the repository and the available Mathlib scheme infrastructure. Then determine how affine varieties, affine space, and isomorphisms should be represented before formalizing the Cancellation Conjecture. Done means the conjecture is added as a checked Lean statement with its required definitions and imports.

Written by the indexing model from the issue text.