∑math20

Dynamical systems and ergodic theory · Result 151

A C1 counterexample to the entropy conjecture

1 paperLean

Constructs a noninvertible C1 self-map of a compact smooth manifold with zero topological entropy but eigenvalue 2 on second homology. This disproves the homological entropy lower bound for general C1 self-maps: homological growth need not force positive orbit complexity.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A C^1 Counterexample to the Entropy Conjecture

A C^1 Counterexample to the Entropy Conjecture

OpenAI · September 25, 2026

We disprove the general C1 self-map formulation of Shub's entropy conjecture. We construct a noninvertible C1 self-map of a compact smooth manifold without boundary whose topological entropy is zero, while its action on second real homology has eigenvalue 2. Thus the topological entropy is strictly smaller than the logarithm of the homological spectral radius.

Read PDF Download Source

Cite
@misc{OAI:A-C1-Counterexample-to-the-Entropy-Conjecture-September-25-2026,
  author = {{OpenAI}},
  title = {{A $C^1$ Counterexample to the Entropy Conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-C1-Counterexample-to-the-Entropy-Conjecture-September-25-2026/article.pdf}{OAI:A-C1-Counterexample-to-the-Entropy-Conjecture-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Shub's entropy conjecture predicts that a smooth self-map's topological entropy is at least the logarithm of the spectral radius of its action on real homology. The formalization gives a counterexample to the general \(C^1\) self-map version: a noninvertible \(C^1\) map on a compact smooth manifold without boundary has topological entropy zero, while its action on second real homology has a nonzero eigenvector with eigenvalue \(2\). Thus the homological lower bound is strictly positive and fails for this map.

Comparator links

ResultComparator statement
A \(C^1\) counterexample to the entropy conjectureC1EntropyCounterexample.lean

Scope note on GitHub →