Pfister's problem: the Pythagoras number of ℝ(X₁, …, Xₙ)

### What is the conjecture

Pfister's problem on the Pythagoras number of the rational function field ℝ(X₁, …, Xₙ). The Pythagoras number p(K) of a field K is the least p such that every sum of squares in K is a sum of p squares. Pfister showed p(ℝ(X₁, …, Xₙ)) ≤ 2ⁿ, and Problem 1 of §4 of his ICM address asks for the true value:

> A. Pfister, *Sums of squares in real function fields*, Actes du Congrès International des Mathématiciens (Nice, 1970), Tome 1, pp. 297–300 ([IMU scan](https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1970.1/ICM1970.1.ocr.pdf)).

The question is often posed as whether Pfister's bound is optimal, i.e. whether p(ℝ(X₁, …, Xₙ)) = 2ⁿ (e.g. Question 0.2 of Benoist, *On Hilbert's 17th problem in low degree*, Algebra Number Theory 11 (2017), [arXiv:1602.07330](https://arxiv.org/abs/1602.07330)). The best known bounds are n + 2 ≤ p(ℝ(X₁, …, Xₙ)) ≤ 2ⁿ for n ≥ 2, so the value is known for n ≤ 2 and open for every n ≥ 3; the 2025 Notices survey of Merkurjev and Parimala (vol. 72, no. 7, Question 5.7) records it as open even for n = 3.

Planned formalisation: the open problem in both forms ("what is the value" and "is it 2ⁿ"), together with Pfister's upper bound, Cassels' theorem, and the Cassels–Ellison–Pfister lower bound as solved variants, and the known cases n = 0, 1, 2.

### Prerequisites needed

A counted version of Mathlib's `IsSumSq` ("sum of `n` squares") and the set of admissible lengths, to be added to `FormalConjecturesForMathlib`. `MvRatFunc` from `FormalConjecturesForMathlib` gives ℝ(X₁, …, Xₙ).

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

* ams-11
* ams-12
* 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 the counted `IsSumSq` prerequisite and the existing `MvRatFunc` support in `FormalConjecturesForMathlib`. Done means formalizing both open-problem statements, Pfister's upper bound, the named lower-bound and Cassels variants, and the known cases for n = 0, 1, 2.

Written by the indexing model from the issue text.