PfisterPythagorasNumber.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 5 contain sorry, 0 declared as axioms

Pfister's problem on the Pythagoras number of $\mathbb{R}(X_1, \dots, X_n)$

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, i.e. the least element of pythagorasBounds K.

Artin's solution of Hilbert's 17th problem shows that a positive semidefinite rational function in $\mathbb{R}(X_1, \dots, X_n)$ is a sum of squares, and Pfister showed that $2^n$ squares suffice ([Pfister1967, Theorem 1]; for the field, Corollary 1 of Theorem 2 in [Pfister1971]). Since sums of squares are positive semidefinite, $p(\mathbb{R}(X_1, \dots, X_n)) \le 2^n$ [Pfister1995, p. 95].

Problem 1 of [Pfister1971, §4] asks for the true value of $p(\mathbb{R}(X_1, \dots, X_n))$. The question is often posed as: is $p(\mathbb{R}(X_1, \dots, X_n)) = 2^n$, i.e. is Pfister's bound optimal? See e.g. [Benoist2017, Question 0.2].

Problem 1 itself quotes the lower bound $n + 1 \le p(\mathbb{R}(X_1, \dots, X_n))$ from Cassels' theorem [Cassels1964]. For $n \ge 2$ the best known bounds are $n + 2 \le p(\mathbb{R}(X_1, \dots, X_n)) \le 2^n$ [Pfister1995, p. 97], where the lower bound follows from the Cassels–Ellison–Pfister theorem [CEP1971]. The bounds agree for $n = 2$, so the value is known for $n \le 2$ and open for every $n \ge 3$. The survey [MerkurjevParimala2025, §5.2] records the question as open even for $\mathbb{R}(X_1, X_2, X_3)$ (Question 5.7).

References:

[Pfister1971] A. Pfister, Sums of squares in real function fields, pp. 297–300 in Actes du Congrès International des Mathématiciens, Tome 1 (Nice, 1970), Gauthier-Villars, 1971, IMU scan.
[Pfister1967] A. Pfister, Zur Darstellung definiter Funktionen als Summe von Quadraten, Invent. Math. 4 (1967), 229–237, doi:10.1007/BF01425382.
[Cassels1964] J. W. S. Cassels, On the representation of rational functions as sums of squares, Acta Arith. 9 (1964), 79–82, doi:10.4064/aa-9-1-79-82.
[Pfister1995] A. Pfister, Quadratic forms with applications to algebraic geometry and topology, London Math. Soc. Lecture Note Ser. 217, Cambridge University Press, 1995.
[CEP1971] J. W. S. Cassels, W. J. Ellison, A. Pfister, On sums of squares and on elliptic curves over function fields, J. Number Theory 3 (1971), 125–149, doi:10.1016/0022-314X(71)90030-8.
[Benoist2017] O. Benoist, On Hilbert's 17th problem in low degree, Algebra Number Theory 11 (2017), 929–959, doi:10.2140/ant.2017.11.929, arXiv:1602.07330.
[MerkurjevParimala2025] A. Merkurjev, R. Parimala, Quadratic forms beyond arithmetic, Notices Amer. Math. Soc. 72 (2025), no. 7, 711–718, doi:10.1090/noti3192.

Imports (1)

FormalConjecturesUtil

theorem PfisterPythagorasNumber.isLeast_pythagorasBounds_real Every sum of squares in $\mathbb{R}$ is a square and $1$ is not a sum of zero squares, so $p(\mathbb{R}) = 1$ line 72 source
Source documentation
Every sum of squares in $\mathbb{R}$ is a square and $1$ is not a sum of zero squares, so $p(\mathbb{R}) = 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, pythagorasBounds, Real, OfNat.ofNat
Proof uses: And.intro, Membership.mem, Set, lowerBounds, IsSumSq, Exists.intro, Fin, Eq, Finset.sum, Finset.univ, HMul.hMul, Real.sqrt, of_eq_true, Eq.trans, True, congrArg, HSMul.hSMul, Finset.card, Singleton.singleton, Finset and 22 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem isLeast_pythagorasBounds_real : IsLeast (pythagorasBounds ℝ) 1 := by
…
```
Mentions: pythagorasBounds
theorem PfisterPythagorasNumber.pfister_problem Pfister's problem (Problem 1 of [Pfister1971, §4]): what is the true value of $p(\mathbb{R}(X_1, \dots, X_n))$, as a function of $n$? sorry line 88 source
Source documentation
Pfister's problem (Problem 1 of [Pfister1971, §4]): what is the true value of $p(\mathbb{R}(X_1, \dots, X_n))$, as a function of $n$? It is $1$, $2$, $4$ for $n = 0, 1, 2$ (pfister_problem.variants.zero, pfister_problem.variants.one, pfister_problem.variants.two) and open for every $n \ge 3$, where only the bounds $n + 2 \le p(\mathbb{R}(X_1, \dots, X_n)) \le 2^n$ are known.

depends on sorry what this means
Statement uses: Nat, sorryAx, Bool.false, IsLeast, pythagorasBounds, MvRatFunc, Fin, Real, MvPolynomial, Finsupp, nonZeroDivisors
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pfister_problem :
    let p : ℕ → ℕ := answer(sorry)
…
```
theorem PfisterPythagorasNumber.pfister_problem.variants.eq_two_pow Pfister's problem in its common yes/no form (e.g. Question 0.2 of [Benoist2017]): is $p(\mathbb{R}(X_1, \dots, X_n)) = 2^n$ for every $n$, i.e. is Pfister's bound optimal? sorry line 99 source
Source documentation
Pfister's problem in its common yes/no form (e.g. Question 0.2 of [Benoist2017]): is $p(\mathbb{R}(X_1, \dots, X_n)) = 2^n$ for every $n$, i.e. is Pfister's bound optimal? This holds for $n \le 2$ and is open for every $n \ge 3$.

depends on sorry what this means
Statement uses: Iff, True, Nat, IsLeast, pythagorasBounds, MvRatFunc, Fin, Real, MvPolynomial, Finsupp, nonZeroDivisors, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pfister_problem.variants.eq_two_pow :
    answer(sorry) ↔ ∀ n : ℕ, IsLeast (pythagorasBounds (MvRatFunc (Fin n) ℝ)) (2 ^ n) := by
…
```
Mentions: pythagorasBounds, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.upper_bound Pfister's theorem: every sum of squares in $\mathbb{R}(X_1, \dots, X_n)$ is a sum of $2^n$ squares [Pfister1995, p sorry line 110 source
Source documentation
Pfister's theorem: every sum of squares in $\mathbb{R}(X_1, \dots, X_n)$ is a sum of $2^n$ squares [Pfister1995, p. 95]; this is Corollary 1 of Theorem 2 in [Pfister1971]. For positive semidefinite polynomials it is [Pfister1967, Theorem 1], the quantitative refinement of Artin's theorem Hilbert17.hilbert_17th_problem in FormalConjectures/HilbertProblems/17.lean.

depends on sorry what this means
Statement uses: Nat, Membership.mem, Set, pythagorasBounds, MvRatFunc, Fin, Real, MvPolynomial, Finsupp, nonZeroDivisors, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pfister_problem.variants.upper_bound (n : ℕ) :
    2 ^ n ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ) := by
…
```
Mentions: pythagorasBounds, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.cassels Cassels' theorem [Cassels1964], as quoted in Problem 1 of [Pfister1971, §4]: $1 + X_1^2 + \dots + X_n^2$ is not a sum of $n$ squares in $\mathbb{R}(X_1, \dots, X_n)$ sorry line 119 source
Source documentation
Cassels' theorem [Cassels1964], as quoted in Problem 1 of [Pfister1971, §4]: $1 + X_1^2 + \dots + X_n^2$ is not a sum of $n$ squares in $\mathbb{R}(X_1, \dots, X_n)$.

depends on sorry what this means
Statement uses: Nat, Not, IsSumSqOfLength, MvRatFunc, Fin, Real, MvPolynomial, Finsupp, nonZeroDivisors, RingHom, Algebra.algebraMap, HAdd.hAdd, OfNat.ofNat, Finset.sum, Finset.univ, HMul.hMul, MvPolynomial.X
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
79 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pfister_problem.variants.cassels (n : ℕ) :
    ¬IsSumSqOfLength n (algebraMap (MvPolynomial (Fin n) ℝ) (MvRatFunc (Fin n) ℝ)
      (1 + ∑ i, MvPolynomial.X i * MvPolynomial.X i)) := by
…
```
Mentions: IsSumSqOfLength, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.add_one_le The lower bound line 131 source
Source documentation
The lower bound $n + 1 \le p(\mathbb{R}(X_1, \dots, X_n))$ quoted in Problem 1 of [Pfister1971, §4]: $1 + X_1^2 + \dots + X_n^2$ is a sum of $n + 1$ squares but, by Cassels' theorem pfister_problem.variants.cassels, not of $n$ squares. It is superseded by pfister_problem.variants.lower_bound for $n \ge 2$.

depends on sorry what this means
Statement uses: Nat, Membership.mem, Set, pythagorasBounds, MvRatFunc, Fin, Real, MvPolynomial, Finsupp, nonZeroDivisors, LE.le, HAdd.hAdd, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, IsSumSqOfLength, RingHom, Algebra.algebraMap, Finset.sum, Finset.univ, HMul.hMul, MvPolynomial.X, Exists.intro, Eq, Fin.cons, of_eq_true, Eq.trans, True, congr, congrArg, map_add, map_one, map_sum and 13 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem pfister_problem.variants.add_one_le (n : ℕ) {p : ℕ}
    (hp : p ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ)) : n + 1 ≤ p := by
…
```
Mentions: pythagorasBounds, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.lower_bound The lower bound $n + 2 \le p(\mathbb{R}(X_1, \dots, X_n))$ for $n \ge 2$ [Pfister1995, p sorry line 146 source
Source documentation
The lower bound $n + 2 \le p(\mathbb{R}(X_1, \dots, X_n))$ for $n \ge 2$ [Pfister1995, p. 97], a consequence of the Cassels–Ellison–Pfister theorem [CEP1971]. The hypothesis $n \ge 2$ is needed: $p(\mathbb{R}(X)) = 2 < 3$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Membership.mem, Set, pythagorasBounds, MvRatFunc, Fin, Real, MvPolynomial, Finsupp, nonZeroDivisors, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pfister_problem.variants.lower_bound (n : ℕ) (hn : 2 ≤ n) {p : ℕ}
    (hp : p ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ)) : n + 2 ≤ p := by
…
```
Mentions: pythagorasBounds, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.zero Documented declaration: zero line 156 source
Source documentation
$p(\mathbb{R}(X_1, \dots, X_n)) = 1$ for $n = 0$, i.e. $p(\mathbb{R}) = 1$: here the bounds $n + 1$ and $2^n$ of pfister_problem.variants.add_one_le and pfister_problem.variants.upper_bound agree. Compare isLeast_pythagorasBounds_real, the same value for ℝ itself.

depends on sorry what this means
Statement uses: IsLeast, Nat, pythagorasBounds, MvRatFunc, Fin, OfNat.ofNat, Real, MvPolynomial, Finsupp, nonZeroDivisors
Proof uses: And.intro, Membership.mem, Set, lowerBounds, PfisterPythagorasNumber.pfister_problem.variants.upper_bound, PfisterPythagorasNumber.pfister_problem.variants.add_one_le
45 instances, coercions and auxiliary constants left out.
```
theorem pfister_problem.variants.zero : IsLeast (pythagorasBounds (MvRatFunc (Fin 0) ℝ)) 1 :=
…
```
Mentions: pythagorasBounds, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.one $p(\mathbb{R}(X)) = 2$ [Pfister1995, p line 167 source
Source documentation
$p(\mathbb{R}(X)) = 2$ [Pfister1995, p. 96]: Pfister's bound gives $p \le 2$, and Cassels' theorem pfister_problem.variants.cassels gives $p \ge 2$ through pfister_problem.variants.add_one_le, since $1 + X^2$ is a sum of two squares that is not a square in $\mathbb{R}(X)$.

depends on sorry what this means
Statement uses: IsLeast, Nat, pythagorasBounds, MvRatFunc, Fin, OfNat.ofNat, Real, MvPolynomial, Finsupp, nonZeroDivisors
Proof uses: And.intro, Membership.mem, Set, lowerBounds, PfisterPythagorasNumber.pfister_problem.variants.upper_bound, PfisterPythagorasNumber.pfister_problem.variants.add_one_le
45 instances, coercions and auxiliary constants left out.
```
theorem pfister_problem.variants.one : IsLeast (pythagorasBounds (MvRatFunc (Fin 1) ℝ)) 2 :=
…
```
Mentions: pythagorasBounds, MvRatFunc
theorem PfisterPythagorasNumber.pfister_problem.variants.two $p(\mathbb{R}(X_1, X_2)) = 4$ [CEP1971], as recorded in [Pfister1971, §4] and [Pfister1995, p line 176 source
Source documentation
$p(\mathbb{R}(X_1, X_2)) = 4$ [CEP1971], as recorded in [Pfister1971, §4] and [Pfister1995, p. 96]: the bounds $n + 2$ and $2^n$ agree when $n = 2$.

depends on sorry what this means
Statement uses: IsLeast, Nat, pythagorasBounds, MvRatFunc, Fin, OfNat.ofNat, Real, MvPolynomial, Finsupp, nonZeroDivisors
Proof uses: And.intro, Membership.mem, Set, lowerBounds, PfisterPythagorasNumber.pfister_problem.variants.upper_bound, PfisterPythagorasNumber.pfister_problem.variants.lower_bound, le_rfl
46 instances, coercions and auxiliary constants left out.
```
theorem pfister_problem.variants.two : IsLeast (pythagorasBounds (MvRatFunc (Fin 2) ℝ)) 4 :=
…
```
Mentions: pythagorasBounds, MvRatFunc