AI Proof WatchKeep up with AI contributions

A Globally Asymptotically Stable Planar Homogeneous Polynomial Vector Field With No Polynomial Lyapunov Function

Jun Liu, Maxwell Fitzsimmons

Liu and Fitzsimmons give an explicit planar homogeneous cubic polynomial vector field with integer coefficients whose origin is globally asymptotically stable and has a positive radially unbounded C¹ homogeneous Lyapunov function, but has no positive definite homogeneous polynomial with nonpositive Lie derivative and no local real-analytic weak Lyapunov function.

Sources for this record

What was already known

The homogeneous polynomial Lyapunov converse conjecture remained open. Known rational homogeneous certificates and earlier nonhomogeneous analytic-obstruction examples did not refute it.

AI involvement AI-centered

Liu and Fitzsimmons credit GPT-5.6 Sol Pro with finding the explicit counterexample and initial arguments. They independently verified the model content and wrote the final analysis; Codex helped draft and formalize it.

GPT-5.6 Sol Pro discovered the decisive explicit field and initial proof ideas, while the human authors completed and verified the final paper.

Importance Notable

The explicit field refutes the converse conjecture and strengthens the obstruction to local real-analytic functions.

Limitations

The reported Lean check covers all four main-theorem items and includes an axiom audit, but the cited repository is a moving branch. The paper’s v1 theorem is the assessed version.

Technical verification Formal (Lean 4/mathlib proof of all four Theorem II.2 items with axiom audit + human)

The v1 paper reports Lean 4 formalization of all four items of its main theorem and an independent human check of AI-generated content. The linked repository maps those four statements to exported Lean declarations and reports standard-axiom audits. These are source-reported complete checks of the explicit example, not a local rebuild.

Independent checking

Independent verification of AI-generated content

Checker
Jun Liu and Maxwell Fitzsimmons, human authors
Scope
AI-generated counterexample and mathematical arguments retained in the article
Basis
Reported by the linked checker
Evidence source

Formal checking

Lean theorem compilation and printed axiom dependencies for the four exported mainTheorem items

Checker
Lean 4 kernel in the authors' reported development
Scope
All four items of Theorem II.2 for the explicit cubic field: global stability, nonpolynomial certificate, polynomial obstruction and local analytic obstruction
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

The human authors give a mechanism-level account of the explicit certificate, the Fejér–Riesz/Fourier contradiction and the leading-term analytic obstruction.

Correction and publication history