Kaplansky's problem: which integers are u-invariants of fields?

### What is the conjecture

The $u$-invariant $u(F)$ of a field $F$ of characteristic $\ne 2$ is the largest dimension of an
anisotropic quadratic form over $F$, or $\infty$ if there is no largest one. Kaplansky introduced
it in *Quadratic forms*, J. Math. Soc. Japan 5 (1953), 200–207, and conjectured that every finite
value is a power of $2$.

That is false, and the question of which integers actually occur is open. Known: $u(F) \notin
\{3, 5, 7\}$ (classical); Merkurjev refuted the conjecture with $u = 6$ (1989) and then showed
every positive even integer occurs (1991); Izhboldin constructed $u = 9$ (Ann. of Math. 154
(2001), 529–587); Vishik $u = 2^r + 1$ for every $r \ge 3$ (2009); and a 2026 preprint of
Karpenko covers every $n$ with neither $n + 1$ nor $n + 3$ a power of $2$. So the problem is open
exactly for $2^r - 1$ and $2^r - 3$ with $r \ge 4$, the smallest being $13$ and $15$. The survey
of Merkurjev and Parimala records the expectation that every odd $n \ge 9$ occurs.

**Sources:**
- A. Merkurjev, R. Parimala, *Quadratic forms beyond arithmetic*, Notices Amer. Math. Soc. 72
(2025), no. 7, 711–718, §5.1, https://doi.org/10.1090/noti3192
- I. Kaplansky, *Quadratic forms*, J. Math. Soc. Japan 5 (1953), 200–207,
https://doi.org/10.2969/jmsj/00520200
- O. Izhboldin, *Fields of $u$-invariant 9*, Ann. of Math. 154 (2001), 529–587,
https://doi.org/10.2307/3062141
- N. Karpenko, *Fields of any $u$-invariant but a 2-power minus 1 or 3*, preprint, 5 August 2026,
https://sites.ualberta.ca/~karpenko/publ/u1or3-02.pdf

### Prerequisites needed

Mathlib has `QuadraticMap.Anisotropic` and `QuadraticMap.Nondegenerate` but nothing about the
$u$-invariant. What is needed is a set `anisotropicDims F` of dimensions of nondegenerate
anisotropic forms over `F`, so that "$u(F) = n$" is `IsGreatest (anisotropicDims F) n` and
"$u(F) = \infty$" is `¬ BddAbove (anisotropicDims F)` — no numeric invariant and no convention
for the infinite case. That is about a hundred lines and needs no new theory.

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

* ams-11
* ams-12

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

I have a branch ready and will open the PR.

AI disclosure: the formalization was drafted with Claude Code, and reviewed by Codex and by me.

Start by locating Mathlib's QuadraticMap.Anisotropic and QuadraticMap.Nondegenerate definitions and the repository's existing conjecture formalizations. Define the requested set of anisotropic dimensions, then characterize finite values with IsGreatest and the infinite case with ¬ BddAbove. Done means the conjecture and both cases are represented without introducing a numeric invariant; the author notes a branch is already ready.

Written by the indexing model from the issue text.