Serre's Conjecture II

### What is the conjecture

For a simply connected semisimple algebraic group $G$ over a perfect field $k$ of cohomological dimension at most 2, the Galois cohomology set $H^1(k, G)$ vanishes. Equivalently, all $G$-torsors (principal homogeneous spaces) over $\mathrm{Spec}(k)$ are trivial.

**Sources:**
- https://en.wikipedia.org/wiki/Serre%27s_conjecture_II_(algebra), https://link.springer.com/chapter/10.1007/978-1-4419-6211-9_3, https://www.math.uni-bielefeld.de/lag/man/326.pdf, https://wstein.org/papers/serre/ribet-stein.pdf

### Prerequisites needed

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

Mathlib currently lacks direct definitions for Galois cohomology and the cohomology of algebraic groups. While foundational concepts like group cohomology, algebraic groups, and field extensions exist in Mathlib, significant new theory would need to be developed to formalize the notion of Galois cohomology sets $H^1(k, G)$ and the cohomological dimension of fields. This requires major infrastructure for Galois descent theory and principal homogeneous spaces.

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

* ams-12
* ams-20
* ams-18

### 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.

No files, tests, or entry points are named. Start by reviewing how existing conjectures are represented in the repository and assess the missing Galois cohomology, algebraic-group cohomology, and cohomological-dimension infrastructure described in the issue; done would mean adding a formal statement of the conjecture.

Written by the indexing model from the issue text.