Grothendieck–Katz p-curvature conjecture

### What is the conjecture

The Grothendieck–Katz p-curvature conjecture is an open problem in arithmetic differential Galois theory. Let $M$ be a differential module over a function field $K$ of characteristic $0$, and let $\psi_p(M)$ denote the $p$-curvature of $M$ modulo a prime $p$. The conjecture states: if $\psi_p(M) = 0$ (the $p$-curvature vanishes) for almost all primes $p$, then the monodromy group of $M$ is finite. Equivalently, the conjecture asserts that the differential Galois group of a system of linear differential equations can be determined by its reductions modulo primes, providing an arithmetic analogue of the Hasse Principle for differential equations.

**Sources:**
- https://arxiv.org/abs/1610.05674, https://math.univ-lyon1.fr/~roques/LNGKpCC.pdf, https://projecteuclid.org/journals/duke-mathematical-journal/volume-167/issue-10/The-p-curvature-conjecture-and-monodromy-around-simple-closed-loops/10.1215/00127094-2018-0008.short, https://web.math.princeton.edu/~yunqingt/p-curv.pdf, https://en.wikipedia.org/wiki/Grothendieck–Katz_p-curvature_conjecture

### Prerequisites needed

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

The conjecture requires formalization of differential modules, $p$-curvature (an operator-theoretic notion in characteristic $p$ reduction), differential Galois groups, and monodromy groups. While basic algebraic geometry and category theory (Tannakian duality) are available in Mathlib, significant infrastructure for differential Galois theory—including the construction of differential Galois groups for differential modules, reduction modulo primes, and $p$-curvature operators—would need to be developed. The formalization would likely require substantial work in differential algebra and its interaction with model theory.

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

* ams-12
* ams-14
* ams-34

### 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 by me, I could not verify the exact statement but the sources seem to point to correct websites for further information.