Problem JC-003

Conjectura.Problems.JC003.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-003

Problem JC-003 — the Jacobian conjecture is false in dimension 3.

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.JC003

/-- Refute the Jacobian conjecture in dimension 3 over `ℂ`. -/
def goal : Prop := ¬ Conjectura.AlgebraicGeometry.JacobianConjectureProp ℂ (Fin 3)

end Conjectura.JC003