AI Proved What?

Episode 009, October 2026

The whole field from a shadow

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

Covers result 009 in OpenAI’s catalog: all 3 papers. See its connections to other results and the work it cites.

Play Episode 009: The whole field from a shadow? Bogomolov’s program, functions modulo squares. A grid of orange and grey switches with an arrow pointing down to C(x, y).

6:03. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00A shadow of a field
  2. 1:00Functions modulo squares
  3. 1:58Why two variables
  4. 2:36What was known
  5. 3:13The claim
  6. 4:07How the rebuild works
  7. 5:10Lean, and the caveats

The claim, in plain words

Take a field of functions in two or more variables over an algebraically closed field, such as ℂ(x, y), the rational functions in x and y with complex coefficients. Keep each nonzero function only up to ℓ-th powers for a fixed prime ℓ different from the characteristic (for ℓ = 2, up to squares), and pair the resulting classes formally with one rule: f paired with 1 − f gives zero (the Steinberg relation). In the language of Milnor K-theory, this is K1M/ℓ and K2M/ℓ with their product.

Result 009 claims that this data determines the field. For two such function fields, every isomorphism of the degree-one groups that respects the pairing comes from an isomorphism of the fields’ perfect closures, and the correspondence is a bijection up to two unavoidable ambiguities: one global scalar in 𝔽ℓ× (none when ℓ = 2), and, in characteristic p, powers of Frobenius. A companion paper claims the Galois version, the Bogomolov–Pop conjecture: the pro-ℓ quotient of the Galois group in which commutators are central determines the field, over any algebraically closed constants. A third paper treats classes modulo p in characteristic p.

What it doesn’t claim

Nothing is claimed for one variable: there, over ℂ, every curve’s function field has the same free profinite Galois group, so Galois data cannot tell curves apart. The constants must be algebraically closed. The data are infinite, so the result says what the data determine, not that there is an algorithm to rebuild the field.

Where it stands

Posted as preprints
OpenAI, September 23 and October 5, 2026; released October 6, 2026
Peer reviewed
Not yet
Checked in Lean
Partly: OpenAI formalized only the uniqueness half of the Galois version (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and the papers are unchanged since the repository’s first public version. We found no public critique specific to this result.

What was known

  • Bogomolov (1991) proposed reconstructing such function fields from the pro-ℓ abelian-by-central quotient of their Galois groups.
  • Bogomolov and Tschinkel proved reconstruction for surfaces (2008) and then in every dimension (2011), over algebraic closures of finite fields; Pop proved the same independently (2012).
  • Over general algebraically closed constants, Pop (2018) reconstructed in dimension at least three from pro-ℓ data with divisorial inertia supplied.
  • For mod-ℓ Milnor K-theory, Topaz (2016) needed dimension at least five, with the rational subgroups supplied.

How the proof goes

  1. Valuations. Pairs of characters f, g with f(x)g(1 − x) = f(1 − x)g(x) are visible in the pairing; known local theory turns them into quasi-divisorial valuations, which mostly correspond to curves along which functions vanish. Pop’s density theorem recognizes residual curves over algebraic closures of finite fields.
  2. Curve subfields. For a function t, the transported classes of t − a, for all constants a, are supported on divisors of bounded degree (a Riemann–Hurwitz argument); an incidence variety shows they all come from one curve’s function field.
  3. Rational lines. Ratios of local parameters at smooth points give rational one-variable subfields, and matching their points gives bijections between projective lines.
  4. Field operations. A blowup detects many coordinates at once; additive triples recover addition, giving an isomorphism of perfect fields that induces the original map up to one scalar.

The Lean statement

theorem main_graph_injective (ell : ℕ) [Fact ell.Prime]
    (k K l L : Type*) [Field k] [Field K] [Field l] [Field L]
    [IsAlgClosed k] [IsAlgClosed l] ...
    (hK : 2 ≤ Algebra.trdeg k K) (hL : 2 ≤ Algebra.trdeg l L) :
    ∀ (a a' : IsomF k K l L) (b : IsomCUnits ell K L),
      PhiGraph a b → PhiGraph a' b → a = a'

This abridged statement is from the challenge file. It says that if two field isomorphisms (modulo Frobenius) induce the same map on the Galois data (modulo ℓ-adic unit scaling), they are equal: the uniqueness half of the Bogomolov–Pop theorem. The other half, that every admissible map on Galois data comes from a field isomorphism, is not formalized, and neither is the Milnor K-theory theorem. The proof is 5 files and 3,339 lines; it is not listed in OpenAI’s formalization catalog, and we have not run the check.

The example in the video

  • f(t) = t3(t − 1)2/(t + 1) has orders 3, 2, −1 and −4 at 0, 1, −1 and ∞. Modulo squares only the parity survives: odd at 0 and −1, so [f] = [t(t + 1)]. The set of odd-order points always has an even number of elements, since the orders add up to zero. Checked with SymPy.

Read the source

The 3 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00A shadow of a field

Here’s a strange kind of puzzle. Take every rational function in two variables, x and y, with complex coefficients: x + y, x² − y³, 1/(x − y), and so on. Together they form a field: you can add, subtract, multiply and divide them. Now throw away almost everything. Keep each function only up to squares, so f and f times any square count as the same. Then pair classes formally, with just one rule: pairing any function f with 1 − f gives zero. What’s left is a vast collection of on and off switches, plus a pairing table. Result 009 in OpenAI’s math repository claims that this shadow is enough to rebuild the entire field, up to two unavoidable ambiguities in general, and here, none at all. A companion paper claims the same from a small piece of the field’s Galois group, as Fedor Bogomolov proposed in 1991.

1:00Functions modulo squares

Start with one variable, t. Over the complex numbers every constant is a square, so only zeros and poles matter. Take t³(t − 1)²/(t + 1). Its orders are three at zero, two at one, −1 at −1, and −4 at infinity. Up to squares, only the parity survives: odd at zero and at −1, even everywhere else. So this function has the same class as t(t + 1). Each class is just a set of points where the order is odd, and that set always has an even number of points. In two variables, classes are about curves instead of points: the curves along which a function vanishes, or blows up, an odd number of times. The theorem works the same way with cubes, fifth powers, or powers by any prime. These are the first two Milnor K-groups modulo a prime, and the rule about f and 1 − f is the Steinberg relation.

1:58Why two variables

Why two variables? Because one isn’t enough. Over the complex numbers, the full Galois group of every curve’s function field is the same free group, so Galois data can’t tell two curves apart. Grothendieck’s anabelian philosophy says that in the right settings, Galois groups determine geometry. Bogomolov’s proposal was bolder: with two or more variables over an algebraically closed field, a tiny piece of the Galois group should suffice, the quotient in which every commutator commutes with everything. Our two collections of switches are a mirror image of that piece, taken modulo a prime and seen from the dual side.

2:36What was known

Bogomolov and Yuri Tschinkel proved it for surfaces in 2008, and then in every dimension, but only when the constants are the algebraic closure of a finite field. Florian Pop proved the same independently in 2012. Over the complex numbers, or any other algebraically closed field, it stayed open. Pop handled dimension three and up in 2018, but only with extra information supplied. For the finite version, Adam Topaz needed dimension at least five, plus the one-variable rational subfields handed over in advance.

3:13The claim

Result 009 claims the full answer. Take two function fields of dimension at least two, over any algebraically closed fields of characteristic different from the prime. Every isomorphism of the two collections that respects the pairing table comes from an isomorphism of the fields themselves. Two ambiguities remain, and they can’t be avoided. Multiplying every class by the same nonzero number, modulo the prime, preserves the whole puzzle. And in characteristic p, the Frobenius map, which raises everything to the pth power, just multiplies every class by p. So the field comes back up to these, and up to pth roots. A companion claims to prove the Galois version, the Bogomolov–Pop conjecture, in the same generality, and a short third paper handles classes modulo p in characteristic p.

4:07How the rebuild works

The rebuild climbs a ladder. First, pairs of characters that obey a special alternating rule reveal valuations, using known local theory: mostly the curves along which functions vanish, plus some that also measure the constants, which get sorted out later. Next come one-variable subfields. For each function t, the matching classes of the family t − a, for every constant a, sit on curves of bounded degree, and an incidence variety shows that the matching classes all come from a single curve’s function field. Then come rational lines. Ratios of local coordinates at smooth points give subfields that look like functions of one variable, and matching their points gives bijections between projective lines. Finally, the field operations. Reading many functions’ values at once, near a single point, recovers addition, and with it the whole field. The paper then checks that this field isomorphism induces the original map, up to one scalar.

5:10Lean, and the caveats

There is a Lean formalization, but it covers only half of the Galois version: uniqueness. If two field isomorphisms induce the same map on the Galois data, up to scaling, they agree up to Frobenius. It’s about 3,300 lines in five files. The hard half, rebuilding the field, isn’t formalized, and neither is the Milnor K-theory theorem. We haven’t run the check. The caveats. These are preprints, 73 pages across three papers, not peer reviewed. The theorem needs at least two variables and algebraically closed constants. And the data are infinite, so this is a statement about what the shadow determines, not a procedure you could run. Keep only the parity of zeros and poles, plus one rule for pairing them, and the whole field comes back. If the proof holds.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.