Papers With

← All papers
First page of The modified Cartan conjecture

The modified Cartan conjecture

Alexandre Eremenko, Zongben Xu, Teng Zhang

math.CV Sep 20, 2026 · v1
formalization mathlib ai-agents analysis
Read PDF arXiv abstract Code
TL;DR
The main theorems, including the sharp radius 2-√3 and the Kobayashi–Royden applications, are formalized in Lean 4 with Mathlib; the formalization was generated by OpenAI Codex.
Abstract
In 1928 H. Cartan stated a conjecture about holomorphic curves in $\mathbb{P}^n$ parametrized by the unit disc, omitting $n+2$ hyperplanes in general position. He proved it for $n=2$. In 1996 the first-named author constructed counterexamples for all $n\geq 3$, and proposed a modified form of Cartan's conjecture which he proved for $n=3$. In this paper we prove this modified conjecture in all dimensions. As a byproduct we prove a quantitative version of the classical theorem that analytic functions are linearly dependent if and only if their Wronskian determinant is zero. We interpret our results in terms of the Kobayashi–Royden pseudometric on the complement of $n+2$ hyperplanes, and on smooth algebraic varieties in the algebraic torus.
Problem

In 1928 Cartan conjectured a Bloch-principle analogue of Borel's theorem for holomorphic curves in P^n omitting n+2 hyperplanes. Counterexamples were found for n≥3, and a modified conjecture was proposed and proved only for n=3. The paper settles the modified conjecture in all dimensions.

Approach

The proof uses a quantitative lower bound on Wronskians, which gives an effective form of the theorem that analytic functions are linearly dependent if and only if their Wronskian vanishes. It also uses a growth estimate for units, proved by induction over shrinking radii, and a preorder argument on quotients over nested disks. A sharp radius 2-√3 for five functions is obtained by comparing harmonic functions along hyperbolic geodesics. The main results are formalized in Lean 4 with Mathlib; the formalization was generated by OpenAI Codex and checked by the Lean kernel.

Results

The modified Cartan conjecture is proved for all n, with the sharp radius R_5 = 2-√3 in the five-function case. The paper characterizes the zero directions of the Kobayashi–Royden pseudometric on hyperplane complements and on subvarieties of the algebraic torus. These results are machine-checked in Lean 4.