Prove2Me

brauer_manin_obstruction

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebranumber-theory

Brauer–Manin obstruction: For varieties over number fields, the Brauer–Manin obstruction controls whether local solvability implies global solvability. Conjectured (Colliot-Thélène) to be the only obstruction for rational points on rationally connected varieties. Open for general varieties.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem brauer_manin_obstruction (K : Type*) [Field K] [NumberField K]
    (n : ℕ) (f g : MvPolynomial (Fin n) ℤ) :
    (∃ x : Fin n → K, MvPolynomial.eval x (f.map (algebraMap ℤ K)) = 0 ∧
      MvPolynomial.eval x (g.map (algebraMap ℤ K)) = 0) →
    ∃ C : ℝ, C ≥ 0 := by
  sorry
Source
https://en.wikipedia.org/wiki/Brauer%E2%80%93Manin_obstruction

View graph