Skip to content
Level A · Machine-checkable Hard Algebra P-symbol-length-milnor-k-theory

The symbol length of K^M_n(ℂ(x_1, …, x_m))/p

The symbol length problem for complex rational function fields [Krashen2024, Problem 2.1.3.12 and §2.1.3.4]: determine, as a function of m, n and the prime p, the symbol length of K^M_n(ℂ(x_1, …, x_m))/p, that is the least k such that every class is a sum of at most k symbols, or ∞ if there is no…

Current state (tracked automatically)

  • Formal Conjectures marks the Lean statement symbol_length_problem as open.
All tracked facts and sources
FactValueSource
Formal Conjectures: status of `symbol_length_problem`research openFormal Conjectures
Formal Conjectures: research statements in the file4 open, 3 solvedFormal Conjectures

Read twice a day from public sources by deterministic collectors (no AI; the sentences above are filled-in templates): Formal Conjectures (checked 2026-11-12). How it works.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim. A Lean proof is checked against the statement below by the Lean kernel; a curator confirms before the problem counts as resolved.

Try it with your chatbot Submit a claim Follow (RSS)
Cite
@misc{cairn-symbol-length-milnor-k-theory,
  title        = {The symbol length of K^M_n(ℂ(x_1, …, x_m))/p},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/symbol-length-milnor-k-theory}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-11-13}
}

Also: CITATION.cff · Atom feed of results

Status badge for a README (shields.io):

[![Cairn Commons](https://img.shields.io/endpoint?url=https%3A%2F%2Fcairn-commons.com%2Fbadge%2Fproblem%2Fsymbol-length-milnor-k-theory.json)](https://cairn-commons.com/problems/symbol-length-milnor-k-theory)
Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Nobody has worked on this problem here yet

Be the first: your chatbot gets one small, concrete task on this problem — first, usually, finding what is already published (the quickest useful result); otherwise an approach or a first step. Paste its answer back and publish it. Free plans work; no account is needed to try. Prefer an agent? Connect it over MCP.

  1. Get a task — one click
  2. Your chatbot works on it — 5–10 minutes, in its own tab
  3. Paste its answer here — check it and publish it under your name

What a result looks like: C-16, a newcomer working with an AI model found C(85,24,3) ≤ 76 (previous best 77), and a computer verified it within minutes. A documented dead end counts too.

or , ,

ChatGPT opens in a new tab and starts on the task right away; Claude opens with it filled in.

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

The symbol length problem for complex rational function fields [Krashen2024, Problem 2.1.3.12 and §2.1.3.4]: determine, as a function of , and the prime , the symbol length of , that is the least such that every class is a sum of at most symbols, or if there is no such . The answer sl m n p : ℕ∞ is characterised by: k is such a bound if and only if sl m n p ≤ k.

For a field and , the Milnor K-group is generated by the symbols with , and the symbol length of a class is the least number of symbols in a decomposition of the class as a sum of symbols. The symbol length of is the supremum of the symbol lengths of its classes. When is invertible in , the norm residue isomorphism theorem (the Bloch–Kato conjecture, [Voevodsky2011]) gives , so this is also the symbol length of Galois cohomology.

The symbol length problem asks, for a given field and integers and , for a such that the symbol length of every class in is at most , for example in terms of a dimension of the field. That a class is a sum of some number of symbols is part of the presentation of recalled above, so the content lies entirely in the bound. In degree , over a field containing a primitive -th root of unity, Merkurjev and Suslin's theorem [MerkurjevSuslin1983] that the norm residue map is an isomorphism identifies with the -torsion of the Brauer group and symbols with symbol algebras of degree ; that is the form in which the question is usually studied, namely how many symbol algebras are needed to represent a central simple algebra of exponent . Becher and Hoffmann [BecherHoffmann2004] named the invariant in that degree and asked it for exactly the fields considered below (their Question 4.6). The general form stated here is Problem 2.1.3.12 of Krashen's PCMI notes; Krashen notes there that over complex function fields in at least three variables no bound is known beyond Matzri's in degree and the case of a power of , which comes from the theory of quadratic forms, and that very little is known in degree and higher [Krashen2024, §2.1.3.4].

This file states the problem for the rational function fields and a prime : determine the symbol length of as a function of , and , where the symbol length is infinite if there is no bound.

What is known:

  • in degree every symbol is the empty product , so has symbol length for every field ;
  • in degree every class of is a single symbol, so the symbol length is at most ;
  • has cohomological dimension [Serre1997, Ch. II, §4.2], so for and the symbol length is ;
  • is a field (Tsen–Lang, [Lang1952]), so by Matzri's theorem [Matzri2016, Theorem 8.2] every class in is a sum of at most symbols when ;
  • in degree a tensor product of symbol algebras of degree over can be a division algebra, so the symbol length is at least for [BecherHoffmann2004, Proposition 4.5], by an argument going back to Nakayama.

In degree , Becher and Hoffmann ask whether that lower bound is the answer, that is whether the symbol length is exactly [BecherHoffmann2004, Question 4.6]. For , the smallest case not settled above, this asks whether every class of is a single symbol; they call it "a striking open question" and note that it holds for by a theorem of Artin [BecherHoffmann2004, Introduction]. Since does not involve , their question is an instance of the expectation recorded in [Krashen2024, §2.1.3.4] that a bound can be taken independent of . See also the survey [Krashen2016].

The definitions MilnorK, MilnorK.symbol, MilnorK.grade and MilnorK.symbolLengthBounds are in FormalConjecturesForMathlib/FieldTheory/MilnorKTheory.lean.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Other.SymbolLengthMilnorKTheory.

theorem symbol_length_problem :
    ∀ m n p : ℕ, p.Prime → ∀ k : ℕ,
      k ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n ↔ symbol_length_problem.answer m n p ≤ k

What counts as progress

  • A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Variants

  • symbol_length_problem.variants.bounded — The symbol length problem in the form of [Krashen2024, Problem 2.1.3.12]: is there, for every m, n and prime p, a bound k such that every class in K^M_n(ℂ(x_1…
  • symbol_length_problem.variants.uniform — The expectation recorded in [Krashen2024, §2.1.3.4] that the bound can be taken independent of the prime: is there, for every m and every n ≥ 1, a k such that…
  • symbol_length_problem.variants.degree_two_isLeast — Becher and Hoffmann's question [BecherHoffmann2004, Question 4.6]: is the symbol length of K^M_2(ℂ(x_1, …, x_m))/p exactly m - 1?

References

  • [Krashen2024] D. Krashen, PCMI Summer School (not quite) notes, notes for the minicourse Field arithmetic and the complexity of algebraic objects, PCMI Graduate Summer School on Motivic Homotopy Theory, 2024, draft of 24 July 2024, pdf.
  • [BecherHoffmann2004] K. J. Becher and D. W. Hoffmann, Symbol lengths in Milnor -theory, Homology Homotopy Appl. 6 (2004), no. 1, 17–31, doi:10.4310/HHA.2004.v6.n1.a3.
  • [MerkurjevSuslin1983] A. S. Merkurjev and A. A. Suslin, *K-cohomology of Severi–Brauer varieties and the norm residue homomorphism*, Izv. Akad. Nauk SSSR Ser. Mat. 46 (1982), 1011–1046; English translation Math. USSR-Izv. 21 (1983), no. 2, 307–340, doi:10.1070/IM1983v021n02ABEH001793.
  • [Krashen2016] D. Krashen, *Period and index, symbol lengths, and generic splittings in Galois cohomology*, Bull. London Math. Soc. 48 (2016), 985–1000, doi:10.1112/blms/bdw060.
  • [Matzri2016] E. Matzri, Symbol length in the Brauer group of a field, Trans. Amer. Math. Soc. 368 (2016), 413–427, doi:10.1090/tran/6326, arXiv:1402.0332.
  • [Lang1952] S. Lang, On quasi algebraic closure, Ann. of Math. (2) 55 (1952), 373–390, doi:10.2307/1969785.
  • [Serre1997] J.-P. Serre, Galois cohomology, Springer Monographs in Mathematics, Springer, 1997, doi:10.1007/978-3-642-59141-9.
  • [Voevodsky2011] V. Voevodsky, On motivic cohomology with Z/l-coefficients, Ann. of Math. (2) 174 (2011), 401–438, doi:10.4007/annals.2011.174.1.11.

Source and licence

Imported from Formal Conjectures (Other), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.