The Inverse Generator Problem on Hilbert Spaces

If $A$ generates a bounded $C_0$ -semigroup on a Hilbert space and has dense range, does $A^{-1}$ also generate a bounded $C_0$ -semigroup? Posed by deLaubenfels in 1988. Answered negatively: Lorist, Meyries and Veraar construct a bounded operator with dense range generating a bounded, strongly stable semigroup whose inverse generates no $C_0$ -semigroup at all. The counterexamples come from one explicit finite-dimensional construction, using bases of $\mathbb{C}^{2n}$ with uniformly bounded partial-sum projections but unconditionality constants growing like $n^\alpha$ .

Result: Disproved(see note)
Status: Resolved
AI contribution: AI-assisted
Method: Construction
Field: Semigroup theory
Posed by: Ralph deLaubenfels
Year posed: 1988
Years open: 38y
Solved: 2026-08-06
Model: ChatGPT 5.6 Pro, Claude Fable
Vendor: OpenAI, Anthropic
Collaborators: Emiel Lorist, Martin Meyries, Mark Veraar
Verification: Unreviewed
Publication: Preprint
Significance: 22 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

One finite-dimensional construction settles several related questions. Besides the inverse generator problem, it gives a generator whose Cayley transforms satisfy the ordinary Kreiss resolvent condition but are neither strongly Kreiss bounded nor power bounded, and it shows the Crank-Nicolson scheme is unstable in operator norm both over long times at fixed step size and under mesh refinement at fixed final time. Version 2 adds Theorem 1.4, whose part (i) solves Question 6.1 of Chalmoukis, Tsikalas and Yakubovich; that question is tracked as its own entry.

What the AI did

ChatGPT 5.6 Pro by OpenAI was used to explore Schauder basis counterexamples to the inverse generator problem. It also assisted the adaptation of Ansorena's construction used to obtain the explicit Schauder basis in Proposition 2.1, and was used to optimize the explicit constants in Theorem 1.1 and Proposition 2.1 by repeatedly dissecting the estimates and searching for numerical improvements.

In version 3, the authors additionally provide a complete Lean 4 formalization of Theorem 1.1. This formalization was produced using Claude Fable by Anthropic. The formalized theorem is the finite-dimensional construction underlying the subsequent counterexamples. The paper attributes exploration, assistance, optimization and formalization to the models rather than the central mathematical construction itself, so the AI contribution remains classified as AI-assisted.

Verification

Version 3 has a complete Lean 4 machine-checked proof of Theorem 1.1, the explicit finite-dimensional construction underlying the counterexamples. The accompanying repository states that the development is self-contained on top of Mathlib, contains no sorry, no native_decide and no numerical or floating-point proof steps, and that the final theorem depends only on Lean's standard axioms propext, Classical.choice and Quot.sound.

However, the Lean development formalizes Theorem 1.1 rather than the infinite-dimensional inverse-generator conclusion of Theorem 1.2. In particular, the passage assembling the finite-dimensional blocks into the Hilbert-space counterexample has not been formally verified or independently expert-reviewed. The entry should therefore remain Unreviewed rather than being upgraded to Lean-checked or Lean-verified.

Sources

Related entries

Same work resolves bothKreiss constant separation

Submitted by RustyKestrel290 on 07 Aug 2026