In the talk
Unimath - its present and its future, July 10, 2017. Video and slides of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. (abstract)
Voevodsky mentioned that he was still interested in formalising his pre-Univalent foundations work, but on page 29 of the slides says:
Another direction is the one that I have stated in my Bernays lectures at the ETH in 2014 - to formalize a proof of Milnor’s conjecture on Galois cohomology.
It has not been developing much. On the one hand, I discovered that formalizing it classically it is not very interesting to me because I am quite confident in that proof and in its extension to the Bloch–Kato Conjecture.
On the other hand, when planning a development of a constructive version of this proof one soon encounters a problem. The proof uses the so called Markurjev–Suslin transfinite argument that relies on the Zermelo’s wellordering theorem that in turn relies on the axiom of choice for sets.
There is a note to the abstract, which says (I have reformatted slightly):
Toward the end of the talk, Voevodsky says it would be good to find a constructive proof to replace the "Merkurjev–Suslin transfinite argument" in the proof of Bloch–Kato. Merkurjev says they did not use any transfinite induction in their argument, and has provided the following additional details:
"Let $F$ be a field, $S$ the set of all $n$-symbols over $F$ (modulo $\ell$) and $T$ the set of all finite subsets of $S$. We order $T$ by inclusion. For any $A$ in $T$ let $X_A$ be the product of norm varieties $X_a$ for all symbols $a$ in $A$. If $A$ is a subset of a finite set $B$ in $T$, we have projection $X_B \to X_A$ and hence a field homomorphism $F(X_A) \to F(X_B)$. Let $F_1$ be the colimit of this system of fields. Then construct a field extension $F_2/F_1$ the same way (replacing $F$ by $F_1$), etc. We get a tower of field extensions $F$ in $F_1$ in $F_2$ in ... Finally, let $K$ be the union of all $F_i$. Clearly, every $n$-symbol over $K$ is trivial modulo $\ell$."
See also Theorem 1.12 of the book The Norm Residue Theorem in Motivic Cohomology by Haesemeyer and Weibel, which presents a transfinite version of the argument.
So this raises the question:
what problem is left regarding formalising the argument and/or finding the desired constructive proof?
I presume there are a lot of details, but is it known what might be the major obstacle? Or is the argument provided by Merkurjev still insufficient to address Voevodsky's concerns: the "transfinite argument" is not needed, but there are other issues with the simpler construction?
