Eden's conjecture on the maximal local Lyapunov dimension
Let be a dynamical system on with a global attractor . Eden's conjecture states that the supremum of the local Lyapunov dimensions over is attained at a stationary point or on an unstable periodic orbit embedded in . Is that true?
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI co-developed
- Method
- Construction
- Field
- Dynamical Systems
- Posed by
- Alp Eden, PhD thesis (Indiana University, 1989), p. 98, Question 1; see also Eden, M2AN 23 (1989) 405-413
- Year posed
- 1987
- Years open
- 39y
- Solved
- 2026-09-13
- Model
- GPT-6 Astra
- Vendor
- OpenAI
- Collaborators
- Evan Li, Lily Zhang
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
A (polynomial) flow on with a global attractor containing an invariant two-torus with an irrational flow, where the local Lyapunov dimension is , while it is at most at every stationary point and on every periodic orbit. So the supremum is not attained at a stationary point or periodic orbit, with or without the word "unstable". The repository also refutes a version for strange (noninteger Hausdorff dimension) local attractors and the critical-path form of Eden's Question 1.
A concurrent independent counterexample, also AI-assisted and formalised in Lean, is Matthew Colbrook's "Aperiodic maximisers of Lyapunov dimension" (Zenodo, 21 September 2026): a polynomial system on of dimension on a torus for every . The repository's current construction, revised on 17 October, appears to be its case ; the September commits used a different setting.
What the AI did
The repository README, under Credit: "Much of the counterexample construction was assisted by GPT-6 Astra. The authors independently searched the literature to verify the findings and discern the valid statements to use."
Verification
Read by this site on 3 November 2026 at commit 69547cb, not rebuilt; the repository has no CI. The headline statements in EdensConjecture/EStatements.lean and their definitions were read: a C1 flow on Euclidean space solving its ODE, a compact invariant set attracting every bounded subset of the phase domain, the local Lyapunov dimension as the infimum of orders with negative upper growth rate of the singular-value function, its supremum over the attractor, and instability as failure of orbital Lyapunov stability. In the global counterexample the phase domain is all of R^5, so the attractor is genuinely global. The proof gives local dimension 9/2 on the torus and at most 3 at every stationary or periodic point, and DefinitionCheck.lean proves the Kuznetsov-Reitmann and both Kaplan-Yorke definitions agree there. The EdensConjecture library has no sorry, admit, axiom declarations, native_decide, unsafe, implemented_by or opaque; sorry appears only in separate, unimported Kuznetsov-Eden files. The formal statement was written by the provers and is not anchored in Formal Conjectures or a tracker. Eden's thesis was not available here; the statement was compared with Kuznetsov (arXiv 1602.05410) and Wikipedia.
Sources
Submitted by Pink on