Zariski-Lipman Conjecture

### What is the conjecture

An algebraic variety $X$ over the complex numbers $\mathbb{C}$ with locally free tangent sheaf $\Omega_X^1$ is smooth. Equivalently, if $R$ is a commutative ring such that the module of Kähler differentials $\Omega_{R/k}$ is projective, then $R$ is a regular ring.

**Sources:**
- https://en.wikipedia.org/wiki/Zariski%E2%80%93Lipman_conjecture https://arxiv.org/abs/2202.02109, https://www.sciencedirect.com/science/article/abs/pii/S0021869322003453, https://www.cambridge.org/core/journals/forum-of-mathematics-sigma/article/lipmanzariski-conjecture-in-genus-one-higher/1E598F7582034A5FD120EB37016F1A1D

### Prerequisites needed

**Formalizability Rating:** 4/5 (as of 2026-01-20)

The conjecture requires formalization of algebraic varieties, tangent sheaves, smoothness properties, commutative rings, derivations, and the notion of regular rings. Mathlib has foundations in commutative algebra (regular rings, derivations), but lacks significant infrastructure for algebraic varieties, tangent sheaves, and scheme theory. Additional theory development would be needed to formalize the full statement, particularly around scheme morphisms and smoothness in the scheme-theoretic sense.

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

* ams-14
* ams-13
* 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

Created by AI, reviewed and edited by me.

Start by reviewing the repository's existing formalized conjectures and the stated mathlib foundations for commutative algebra and derivations. Assess the missing infrastructure for algebraic varieties, tangent sheaves, smoothness, scheme morphisms, and regular rings. Done means adding a Lean formalization of the conjecture, with the required supporting theory developed or identified.

Written by the indexing model from the issue text.