Conjectura
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Problem JC-002

Conjectura.Problems.JC002.Statement

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Statements.Mathematics.AlgebraicGeometry.JacobianConjecture
import Mathlib.Data.Complex.Basic

/-! # Problem JC-002

Problem JC-002 — The plane Jacobian conjecture. OPEN

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.JC002

/-- Decide the Jacobian conjecture in dimension 2 over `ℂ`. Open since 1939. -/
def goal : Prop := Conjectura.AlgebraicGeometry.JacobianConjectureProp ℂ (Fin 2)

end Conjectura.JC002