Faltings' theorem (Mordell conjecture) | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: Unavailable.

Informal solution: Unavailable.

/-- [Stichtenoth, Corollary 1.3.4] (finitely many poles). -/
theorem declaration uses `sorry`finite_setOf_place_notMem [BundledFunctionField K F] (x : F) :
    {v : Place K F | x ∉ v}.Finite := byK:Type u_1F:Type u_2inst✝³:Field Kinst✝²:Field Finst✝¹:Algebra K Finst✝:BundledFunctionField K Fx:F⊢ {v | x ∉ v}.Finite
  sorryAll goals completed! 🐙

/-- Every function field of genus at least 2 (equivalently, every curve of geometric genus
at least 2) over a number field has only finitely many rational points.
Note: if K is not the full constant field of F/K then there are no rational points, because
every place contains the full constant field. -/
theorem declaration uses `sorry`faltings [NumberField K] [BundledFunctionField K F] (h : 2 ≤ genus K F) :
    {v : Place K F | Module.rank K (IsLocalRing.ResidueField v) = 1}.Finite := byK:Type u_1F:Type u_2inst✝⁴:Field Kinst✝³:Field Finst✝²:Algebra K Finst✝¹:NumberField Kinst✝:BundledFunctionField K Fh:2 ≤ genus K F⊢ {v | Module.rank K (IsLocalRing.ResidueField ↥v) = 1}.Finite
  sorryAll goals completed! 🐙