Linearization Conjecture

### What is the conjecture

The Linearization Conjecture concerns algebraic actions of the multiplicative group $\mathbb{C}^*$ on complex affine space. An action is **linearizable** if there exist coordinates in which the action becomes linear.

**Conjecture:** Every algebraic action of $\mathbb{C}^*$ on $\mathbb{C}^n$ is linear in some coordinates of $\mathbb{C}^n$.

This conjecture is **open for $n > 3$**. It is known to be true for $n \leq 3$.

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

**Sources:**
- https://en.wikipedia.org/wiki/Algebraic_group_action, https://ncatlab.org/nlab/show/linearization+of+group+actions https://mathoverflow.net/a/80448

### Prerequisites needed

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

Mathlib provides foundational theory for group actions (in `GroupAction`), affine spaces (as special cases of modules over polynomial rings), and algebraic geometry concepts. The statement requires formalizing: (1) algebraic actions of $\mathbb{C}^*$ (the multiplicative group), (2) the notion of an action being linear in given coordinates, and (3) statements about $\mathbb{C}^n$. These concepts largely connect existing Mathlib infrastructure, though some definitions around linearization and coordinate change may need to be introduced. The main missing piece is explicit formalization of when an action is linearizable, which is a moderate but manageable task.

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

* ams-14
* ams-20

### 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 GroupAction infrastructure and its affine-space and module concepts. Determine how to define algebraic actions of C* on complex affine space and linearizability under coordinate changes. Done means adding a precise Lean statement of the conjecture, with any required definitions and supporting formalization.

Written by the indexing model from the issue text.