Functions of a complex variable

The Lean Pool projects whose card's first MSC2020 code is in class 30, Functions of a complex variable: 4 articles, one per card.

TheoremFormalized Complex Analysis in Lean#

Formalizes Poisson integral formulas on the unit disc and arbitrary centered discs, Herglotz–Riesz representation, and Harnack's inequality on the unit disc, plus infrastructure for univalent function classes S and Σ.

Quoted from the card LeanPool/projects/leancomplexanalysis.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.LeanComplexAnalysis.harnack_ineq

TheoremRadó's theorem for Riemann surfaces#

Proves that every connected Hausdorff one-dimensional complex manifold is second countable. The development constructs a nonconstant harmonic function by Perron's method, builds the étale space of its harmonic-conjugate germs, and applies a formalized Poincaré-Volterra lemma to its discrete-fiber evaluation map.

Quoted from the card LeanPool/projects/rado-theorem.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: Rado Kirov.
  • Source: Radó's theorem for Riemann surfaces by Rado Kirov.
  • Project repository: rkirov/jordan_pick, at commit b3c9b7cf.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
  • License: Apache-2.0.
  • MSC2020: 30F15, 30F20, 54D65.
  • In Lean Pool: LeanPool/Rado, from the card LeanPool/projects/rado-theorem.yaml.
Sources
Leanrado_riemannSurface

TheoremRiemann Mapping Theorem#

Formalizes a proof of the Riemann mapping theorem for proper simply connected plane domains with primitives.

Quoted from the card LeanPool/projects/riemann-mapping-theorem.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanRMT · main · montel · hurwitz

TheoremSendov's conjecture and the Phelps–Rodriguez conjecture#

Proves Sendov's conjecture in full generality: if every zero of a complex polynomial of degree at least two lies in the closed unit disk, then every zero has a critical point within distance one. Also proves the Phelps–Rodriguez strengthening, with strict inequality unless the zero lies on the unit circle and the polynomial is a scalar multiple of z^n - a^n, and recovers Rubinstein's boundary theorem. Formalizes Tao's digestion of Lech Mazur's proof: the problem is reduced to a numerical inequality in the degree and one real parameter, settled by exact rational Bernstein certificates for degrees up to one hundred and by an analytic large-degree reduction beyond. Includes the top case of Maclaurin's inequality and multiset AM–GM, a defect inequality on the closed unit disk, a sharp bound on log(sinh h / h), kernel-checked polynomial certificate infrastructure, and a packed-exponentiation bridge for exact moment integrals.

Quoted from the card LeanPool/projects/sendov-conjecture.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 10 main results, each with its informal statement quoted from the card. The scan finds 8 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Sendov.sendov (theorem; a main declaration), declared in LeanPool/Sendov/Conjecture.lean, line 162: “For every natural number n at least two and every complex polynomial p of degree n all of whose roots have norm at most one, every root a of p admits a root of the derivative of p within distance at most one of a.” Its source, as the card gives it: “Sendov's conjecture (1962); Tao's blog post of 12 August 2026, Conjecture 1, following Mazur's proof; upstream Sendov/Conjecture.lean. First publicly announced 2026-08-12 23:10:54 UTC in that post, with the Lean repository completed the same day.”
  • Sendov.phelps_rodriguez (theorem; a main declaration), declared in LeanPool/Sendov/Conjecture.lean, line 87: “Under the same hypotheses, either some root of the derivative lies at distance strictly less than one from a, or a has norm one and p equals a nonzero scalar multiple of X^n - a^n.” Its source, as the card gives it: “Phelps–Rodriguez conjecture; Tao's blog post, Conjecture 2; upstream Sendov/Conjecture.lean. The equality case is Rubinstein's 1968 theorem.”
  • SendovConjecture.sendov (theorem), declared in LeanPool/Sendov/Conjecture.lean, line 191: “The same statement in the Mathlib-only form of the upstream statement of record: for every complex polynomial p of degree at least two such that every complex w with p(w) = 0 has norm at most one, every zero a of p admits a root of the derivative within distance at most one of a.” Its source, as the card gives it: “Upstream Solution.lean, the declaration checked by the upstream comparator setup.”
  • Sendov.rubinstein_one (theorem), declared in LeanPool/Sendov/Boundary.lean, line 214: “If a polynomial of degree n at least two with all roots in the closed unit disk vanishes at one, then either its derivative has a root within distance strictly less than one of the point one, or the polynomial equals its leading coefficient times X^n - 1.” Its source, as the card gives it: “Rubinstein's theorem; Tang–Zhang arXiv:2508.10341, equation (5.1) and Remark 5.1, run to equality; upstream Sendov/Boundary.lean.”
  • Sendov.stat_lt_one (theorem), declared in LeanPool/Sendov/Main.lean, line 44: “For every degree n at least five and every real parameter alpha between zero and seventeen satisfying the feasibility constraint c^2 ≤ A, the quantity R n alpha of the blog post's equation stat is strictly less than one.” Its source, as the card gives it: “Equation (stat) of Tao's blog post; degrees five to one hundred by Bernstein certificates (upstream Sendov/FiniteRange), degrees at least 101 by the analytic reduction (upstream Sendov/LargeDegree).”
  • Multiset.esymm_card_pred_le, which the scan does not find declared in the project's files at this commit: “For a nonempty multiset of nonnegative reals of cardinality m, the (m-1)-st elementary symmetric function is at most m times the (m-1)-st power of the mean.” Its source, as the card gives it: “Maclaurin's inequality, top case; upstream Sendov/Analytic/Maclaurin.lean.”
  • Multiset.prod_le_mean_pow, which the scan does not find declared in the project's files at this commit: “The product of a multiset of nonnegative reals is at most the mean raised to the cardinality.” Its source, as the card gives it: “Multiset AM–GM inequality; upstream Sendov/Analytic/Maclaurin.lean.”
  • Sendov.defect (theorem), declared in LeanPool/Sendov/Analytic/Defect.lean, line 97: “For a multiset of complex numbers in the closed unit disk, the product of the norms times the sum of the norms of 1/z minus the conjugate of z is at most one minus the square of that product.” Its source, as the card gives it: “The defect lemma; upstream Sendov/Analytic/Defect.lean.”
  • Sendov.log_sinh_div_le (theorem), declared in LeanPool/Sendov/Common/Sinh.lean, line 249: “For every positive real h, the logarithm of sinh h divided by h is at most the square root of h^2 + 9 minus three.” Its source, as the card gives it: “Upstream Sendov/Common/Sinh.lean; the crux of the beta-bound step.”
  • Sendov.pev_pos_of_bern (theorem), declared in LeanPool/Sendov/FiniteRange/Certificate.lean, line 138: “If the Bernstein expansion of an integer coefficient list on an interval from zero to p/q equals p^d times a polynomial P and every Bernstein coefficient is positive, then P is positive on that interval.” Its source, as the card gives it: “Lean Pool port infrastructure replacing the upstream per-certificate ring identities; LeanPool/Sendov/FiniteRange/Certificate.lean.”
Project
  • Authors: Terence Tao.
  • Source: Sendov's conjecture in Lean.
  • Mathematical source, as the card gives it: “T. Tao, A digestion of the proof of Sendov's conjecture, blog post, 12 August 2026, digesting Lech Mazur's AI-assisted proof; the boundary case follows Q. Tang and T. Zhang, arXiv:2508.10341, equation (5.1) and Remark 5.1.”
  • Project repository: teorth/sendov, at commit 1ddea92d.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”. The card's note: “The upstream README states that essentially all Lean source was written by Claude Opus 5 in Claude Code under the direction and review of Terence Tao, who set the targets, supplied the informal proof and staged plans, and made the mathematical decisions.”
  • License: Apache-2.0.
  • MSC2020: 30C15, 30C10, 12D10.
  • In Lean Pool: LeanPool/Sendov, from the card LeanPool/projects/sendov-conjecture.yaml.
Sources
LeanSendov.sendov · Sendov.phelps_rodriguez

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.