Function-field reconstruction from Milnor K-theory and Galois data

3 papersLean

Reconstructs function fields of transcendence degree at least two over algebraically closed constants from \(K^{\mathrm M}_1/\ell\), \(K^{\mathrm M}_2/\ell\), and their product. These data recover the perfect closure and constants when ℓ differs from the characteristic, and the original field and its named base in equal characteristic. Also proves Bogomolov–Pop reconstruction from abelian-by-central pro-ℓ Galois data away from the characteristic.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 3

Reconstruction of Function Fields from Mod-ℓ Milnor K-Theory

OpenAI · October 5, 2026

We prove a mod-ℓ Bogomolov–Pop reconstruction theorem for function fields of transcendence degree at least two over arbitrary algebraically closed fields of characteristic different from ℓ. The groups \(K^{\mathrm M}_1/\ell\) and \(K^{\mathrm M}_2/\ell\), together with their full bilinear product, determine the perfect closure and its constant field. Every compatible isomorphism of these data is induced by a field isomorphism up to a single scalar in \(\mathbb F_\ell^\times\), with only Frobenius ambiguity in the field isomorphism in positive characteristic.

Read PDF Download Source

Cite

@misc{OAI:Reconstruction-of-Function-Fields-from-Mod-ell-Milnor-K-Theory-October-5-2026,
  author = {{OpenAI}},
  title = {{Reconstruction of Function Fields from Mod-$\ell$ Milnor $K$-Theory}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Reconstruction-of-Function-Fields-from-Mod-ell-Milnor-K-Theory-October-5-2026/mod-ell-bogomolov-pop.pdf}{OAI:Reconstruction-of-Function-Fields-from-Mod-ell-Milnor-K-Theory-October-5-2026}},
  year = {2026}
}

Reconstruction from Milnor K-theory modulo the characteristic

OpenAI · October 5, 2026

Let K and L be finitely generated extensions of transcendence degree at least two over algebraically closed fields of characteristic p. We prove that every isomorphism of their first Milnor K-groups modulo p preserving the degree-two Steinberg relations is a nonzero scalar multiple of the map induced by a unique field isomorphism. The proof recovers projective lines over the subfields of pth powers by an elementary calculation with derivations.

Read PDF Download Source

Cite

@misc{OAI:Reconstruction-from-Milnor-K-theory-modulo-the-characteristic-October-5-2026,
  author = {{OpenAI}},
  title = {{Reconstruction from Milnor $K$-theory modulo the characteristic}},
  howpublished = {OpenAI Math Release preprint
    \href{https://github.com/openai/math/blob/main/preprints/Reconstruction-from-Milnor-K-theory-modulo-the-characteristic-October-5-2026/paper.pdf}{OAI:Reconstruction-from-Milnor-K-theory-modulo-the-characteristic-October-5-2026}},
  year = {2026}
}

The Bogomolov-Pop reconstruction theorem

OpenAI · September 23, 2026

We prove the Bogomolov–Pop reconstruction conjecture for function fields of transcendence degree at least two over arbitrary algebraically closed fields of characteristic different from ℓ. The pro-ℓ abelian-by-central datum determines the perfect closure and its constant field, with precisely the Frobenius and ℓ-adic unit ambiguities.

Read PDF Download Source

Cite

@misc{OAI:The-Bogomolov-Pop-reconstruction-theorem-September-23-2026,
  author = {{OpenAI}},
  title = {{The Bogomolov--Pop reconstruction theorem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Bogomolov-Pop-reconstruction-theorem-September-23-2026/paper.pdf}{OAI:The-Bogomolov-Pop-reconstruction-theorem-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

The Bogomolov-Pop reconstruction theorem

Scope

The Bogomolov–Pop reconstruction conjecture concerns recovering a function field and its constants from pro-\(\ell\) abelian-by-central Galois data. The linked formalization proves injectivity of the reconstruction correspondence for function fields of transcendence degree at least two over algebraically closed fields of characteristic different from the prime \(\ell\).

If two isomorphisms of perfect closures preserving the constant fields induce the same Galois-data isomorphism modulo \(\ell\)-adic unit scaling, then they agree modulo Frobenius. The selected statement proves this uniqueness; existence of a field isomorphism for every admissible Galois-data isomorphism is outside it.

Comparator links

Result	Comparator statement
Injectivity of Bogomolov–Pop reconstruction modulo the stated ambiguities	BogomolovPopInjectivity.lean

Scope note on GitHub →