Goncharov Conjecture

### What is the conjecture

For a field $F$, Goncharov's conjecture states that the cohomology of a certain motivic complex $\Gamma(F, n)$ placed in degrees $[1,n]$ is isomorphic to the motivic cohomology groups, providing a description of the algebraic K-groups $K_n(F) \otimes \mathbb{Q}$ in terms of generators and relations that generalize Milnor's K-theory. The conjecture extends Zagier's earlier conjectures on polylogarithms and relates to the Beilinson-Lichtenbaum axioms.

**Sources:**
- https://en.wikipedia.org/wiki/Goncharov_conjecture, https://arxiv.org/abs/2210.11938, https://arxiv.org/abs/2012.05599, https://www.sciencedirect.com/science/article/abs/pii/S000187082400272X, https://gauss.math.yale.edu/~ag727/polylog.pdf

### Prerequisites needed

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

The Goncharov conjecture requires significant infrastructure from algebraic K-theory and motivic cohomology. While Mathlib has basic commutative algebra and category theory foundations, it lacks formal definitions of: (1) motivic cohomology groups, (2) Bloch's complex and related constructions, (3) scissors congruence groups, and (4) the full apparatus of Beilinson-Lichtenbaum axioms. Additionally, the formalization would require establishing the connection between multiple polylogarithm constructions and motivic complexes. This represents substantial new theory development beyond what currently exists in Mathlib.

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

* ams-19
* ams-14
* ams-12

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

The issue names no repository files, tests, or entry points; start by reviewing existing formal-conjecture structure and the linked mathematical sources. Determine the prerequisite infrastructure needed before formalizing the conjecture, with completion requiring a formal statement supported by the required motivic and algebraic K-theory definitions.

Written by the indexing model from the issue text.