Resolution of singularities in positive characteristic

### What is the conjecture

Let $k$ be a field and let $X$ be an integral scheme, separated and of finite type over $k$. A
*resolution of singularities* of $X$ is a proper birational morphism $f : Y \to X$ with $Y$
integral and smooth over $k$. Birational here means that $f$ restricts to an isomorphism between
a dense open subscheme of $Y$ and a dense open subscheme of $X$.

**Conjecture.** If $k$ is perfect of characteristic $p > 0$, then every such $X$ admits a
resolution of singularities.

Hironaka proved this in characteristic zero. In positive characteristic it is known in dimension
at most three: dimensions one and two are classical, and dimension three is due to Cossart and
Piltant. It is open from dimension four on.

Perfectness of $k$ matters for the statement in this form. If $k$ is imperfect and
$a \in k \setminus k^p$, then $\operatorname{Spec} k(a^{1/p})$ is integral, separated and of
finite type over $k$, but every scheme birational to it has function field $k(a^{1/p})$, which is
inseparable over $k$, so none of them is smooth over $k$. Over a general field one asks instead
for $Y$ regular.

**Sources:**
- https://en.wikipedia.org/wiki/Resolution_of_singularities
- H. Hironaka, *Resolution of singularities of an algebraic variety over a field of characteristic
zero: I, II*, Ann. of Math. 79 (1964), 109-203 and 205-326,
https://doi.org/10.2307/1970486 and https://doi.org/10.2307/1970547
- J. Kollár, *Resolution of singularities - Seattle lecture*, https://arxiv.org/abs/math/0508332,
Theorem 36, for Hironaka's theorem stated for all schemes of finite type over a characteristic
zero field
- H. Hauser, *On the problem of resolution of singularities in positive characteristic (or: a proof
we are still waiting for)*, Bull. Amer. Math. Soc. 47 (2010), 1-30,
https://doi.org/10.1090/S0273-0979-09-01274-9
- J. Lipman, *Desingularization of two-dimensional schemes*, Ann. of Math. 107 (1978), 151-207,
https://doi.org/10.2307/1971141
- V. Cossart, O. Piltant, *Resolution of singularities of threefolds in positive characteristic I,
II*, J. Algebra 320 (2008), 1051-1082 and 321 (2009), 1836-1976,
https://doi.org/10.1016/j.jalgebra.2008.03.032 and
https://doi.org/10.1016/j.jalgebra.2008.11.030. These assume the variety is quasi-projective and
the ground field differentially finite over a perfect subfield.
- V. Cossart, O. Piltant, *Resolution of singularities of arithmetical threefolds*, J. Algebra 529
(2019), 268-535, https://doi.org/10.1016/j.jalgebra.2019.02.017. Theorem 1.1 removes both
restrictions: every reduced separated Noetherian quasi-excellent scheme of dimension at most
three admits a proper birational morphism from an everywhere regular scheme, in any
characteristic.

### Prerequisites needed

None. Mathlib has `AlgebraicGeometry.Scheme.BirationalOver`, `IsProper`, `Smooth`,
`LocallyOfFiniteType`, `QuasiCompact`, `IsSeparated` and `AlgebraicGeometry.IsIntegral`, which is
everything the statement needs.

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

* ams-14

### Choose either option

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

Start by reviewing existing formal conjecture entries in the repository and the listed Mathlib definitions: AlgebraicGeometry.Scheme.BirationalOver, IsProper, Smooth, LocallyOfFiniteType, QuasiCompact, IsSeparated, and IsIntegral. Done means adding a Lean statement matching the conjecture; the issue indicates that the author plans to do this, so coordinate before starting.

Written by the indexing model from the issue text.