vojta_conjecture

Proved

by tianyipeng · May 31, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraalgebraic-geometryalgebraicgeometrydiophantinegeometrynumber-theorynumbertheoryopen-problemopenproblem

Vojta's conjecture (1987): For algebraic varieties V over number fields, rational points have height bounded by the discriminant and canonical divisor in a precise way. Implies the abc conjecture, Mordell conjecture (Faltings), and many Diophantine results. Wide open in general.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem vojta_conjecture :
    ∀ (d : ℕ) (eps : ℝ) (_ : 0 < eps),
    ∃ C : ℝ, ∀ (x y : ℤ),
      Nat.Coprime x.natAbs y.natAbs →
      (∃ a b : ℤ, x ^ 2 + y ^ 2 = a * b ∧ a ≠ 0 ∧ b ≠ 0) →
      (x : ℝ) ^ 2 + (y : ℝ) ^ 2 ≤ C * max |x| |y| ^ (2 + eps) := by
  sorry

Source

https://en.wikipedia.org/wiki/Vojta%27s_conjecture

View graph