The cuspidal-cubic point ideal is proper

Proved

CuspidalCubicInput.pointIdeal_ne_top

by wenxinzhang · Aug 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

commutative-algebrainvertible-modulespicard-groups

For the coordinate ring of the cuspidal cubic $Y^2=X^3$ over $\mathbb C$ , the explicitly defined point ideal is a proper ideal.

Preamble

import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Expand
import Mathlib.Algebra.Polynomial.Taylor
import Mathlib.RingTheory.PicardGroup
import Mathlib.LinearAlgebra.DirectSum.TensorProduct
import Definitions.Def_RybinP18_CuspidalCubicInput

open WeierstrassCurve
open WeierstrassCurve.Affine
open Polynomial
open scoped Polynomial.Bivariate
open scoped DirectSum

Formal statement

namespace CuspidalCubicInput

noncomputable section





























lemma pointIdeal_ne_top : pointIdeal ≠ ⊤ := by
  sorry

























































end
end CuspidalCubicInput

Source

CUHK-Shenzhen AI Math Problem 18, https://rybindmitry.github.io/problems/18.html. Lean formalization by Patricia Purtill and Kenta Kitamura, discussed at https://github.com/google-deepmind/formal-conjectures/pull/4644#issuecomment-5089566133; staged from Kenta Kitamura's Apache-2.0 repository https://github.com/KitaKen1/mo507128-lean at commit e9507429c01c4288089e4af1c92a03b7d1e17f74.

View graph