What this registry is, the mathematics behind it, how a result becomes a proof, where the counterexamples come from, and the tools you can use. Pick a section below, or open any question to read the answer.
It is a record for geometric function theory. For a normalized analytic function, it tracks which classes the function belongs to, such as starlike or convex, and how strong the evidence is. Alongside that record it holds machine-checked proofs of sharp coefficient bounds, a searchable library of papers, and two application labs. The live site is the authoritative source for the current state.
It is for researchers in complex analysis, for students learning the field, and for anyone who wants to check a coefficient bound or test a function. You do not need to install anything. Almost everything runs in the browser.
If you have a function in mind, open /verify and paste it. If you want certified results, browse the machine proofs. If you want the published work, search the papers. The families page lists every class in the registry, and the hierarchy page shows how the classes contain one another.
It studies analytic functions that map the unit disk one-to-one onto some shape. The central fact is that the shape is encoded in the function’s Taylor coefficients. Constrain the shape, say to a star shape, and the coefficients are forced into a specific region. Finding the exact edge of that region is the core problem of the field, and it is often surprisingly hard. See the Bieberbach conjecture for the most famous example.
Univalent means one-to-one. A univalent function never sends two different points of the disk to the same place. These are the distortion-free ways to deform the disk into another shape, which is why they appear in conformal mapping and fluid flow.
A function is starlike if its image is star-shaped about the origin: every ray from the origin meets the image in a single segment. It is convex if its image is a convex set. Convex functions sit inside the starlike functions, so convex is the stronger property.
The field studies the normalization f(z) = z + a₂z² + a₃z³ + …,
that is f(0) = 0 and f′(0) = 1. Special functions, such as Bessel or
Mittag-Leffler, are converted into this form first. For example,
f(z) = z·J₀(√z) = z − z²/4 + z³/64 − …
In 1994, Ma and Minda unified a long list of one-off subclasses into a single family. You pick a function φ with φ(0) = 1, and the class is every f for which zf′/f is subordinate to φ. Different choices of φ give different image shapes, such as a lemniscate, a cardioid, or an exponential region. The registry catalogues a wide range of them; browse them on the families page.
We write f ≺ g when the values of f stay inside the region that g draws over the disk. For a Ma–Minda class, the quantity zf′/f must stay inside the region drawn by φ. Think of φ as a budget that zf′/f is not allowed to leave.
These are the specific combinations of coefficients that researchers bound over a class. Fekete–Szegő is |a₃ − μa₂²|. The Hankel determinants are H₂(2) = a₂a₄ − a₃² and the larger H₃(1). Zalcman is |a₂a₃ − a₄| and its relatives. Each class-and-functional pair is its own optimization problem, and the machine proofs work through them one by one.
The Koebe function k(z) = z/(1−z)² is the most important example in the field. It is starlike, and it is extremal for the whole class of univalent functions: it reaches the largest coefficients allowed. The registry also uses it as a test anchor, because several of its exact values are known. Its Schwarzian norm, for instance, is exactly 6, so it checks that the Schwarzian machinery is reporting the right number.
It says that every univalent f with the standard normalization satisfies |aₙ| ≤ n. Bieberbach posed it in 1916, and it stayed open for almost 70 years until de Branges proved it in 1985. The Koebe function shows the bound cannot be improved. That long gap is a good measure of how hard exact coefficient problems are.
One class often contains another. Convex sits inside starlike, which sits inside univalent. The hierarchy page draws this containment graph, so you can see at a glance which property implies which. A proof for an outer class carries down to every class inside it.
A sufficient condition reads “if P then starlike”. It guarantees the property, yet a starlike function may still fail P, as with C01. A necessary condition reads “if starlike then P”. Every starlike function satisfies it, but P alone does not guarantee starlikeness. The proven coefficient bounds on /proofs are necessary conditions: a value above the bound means the function is not in that class.
The defining condition Re(zf′/f) > 0 is both necessary and sufficient, but it must hold across the whole disk. That is exactly what the certified tier checks.
They are classical sufficient conditions for starlikeness, checked exactly from the coefficients.
C01 (Schild/Alexander): if Σ n|aₙ| ≤ 1 for n ≥ 2, then f is starlike.
C02 (Nasr-Aouf): if Σ (n−1)|aₙ| ≤ 1, then f is starlike.
Both are sufficient but not necessary. Many starlike functions fail them; the Koebe function has Σ n|aₙ| = ∞.
They are tests for univalence built from the Schwarzian derivative or the pre-Schwarzian. Nehari’s criterion and Becker’s criterion each give a sufficient condition for a function to be univalent. The registry computes these norms for each family and shows them on the family pages. They earn their keep when the direct starlike or convex test is inconclusive.
Every check declares a direction. It either screens, which is heuristic and can be wrong either way, or it proves, or it disproves, both of which are certified. The engine runs three tiers, cheapest first.
Tier 1, float grid screen (about 5 ms). It evaluates the criterion, such as Re(zf′/f) > 0, on a grid of points in the disk. This is fast, but a sample is never a certificate. It only screens.
Tier 2, certified interval arithmetic. It re-evaluates with rounding-safe interval arithmetic (mpmath), splitting the disk into arcs until each one is decided. If the enclosure clears the threshold across the whole domain, the property is proven. If it falls the wrong side, the engine returns a certified counterexample. A winding-number check confirms there are no stray zeros.
Tier 3, exact symbolic (SymPy). For polynomials and closed forms, exact coefficient conditions give complete proofs.
The rule is simple: a grid hit is evidence, and a proof or disproof counts only when interval or symbolic arithmetic produces it. The methods report has the full detail.
Yes. /verify is a sandbox, so nothing is written to the registry. You get the tiered verdict, the image domain f(𝔻) as an exportable figure, and a check of your coefficients against the proven sharp bounds of any class. A disproof verdict is a certified counterexample.
You can also call it from code. Run pip install -e ., then
import gft; gft.verify(coeffs). The README lists the tier
functions.
Two forms. The first is a closed form in SymPy syntax, such as
z/(1-z)^2 or z*exp(z), where f(0) = 0 and
f′(0) = 1 are required. The second is a list of Taylor coefficients
[a₂, a₃, …]. A closed form gives stronger results, because the engine can
avoid the truncation error that a finite coefficient list carries. See the
failure modes for why that matters.
Trust a proof or a disproof only when it comes from the interval tier or the symbolic tier. A grid screen is evidence, not proof. The verify page marks the authoritative result for you, so you do not have to judge the tiers yourself. The reasoning is in how verification works.
It shows the shape the function maps the disk onto. The thin curves are circles |z| = r carried through f, and the bold curve is the image of the boundary. You can read the geometry straight off it: a star shape for a starlike function, a convex blob for a convex one. The figure is drawn in your browser and exports as PNG or TikZ.
A screen is heuristic and can be wrong in either direction. A proof certifies that the property holds. A disproof certifies that it fails, and hands you a witness point. Only the interval and symbolic tiers can prove or disprove; the grid tier can only screen.
Take a functional L over a Ma–Minda class. We reduce max |L|² to a polynomial on a box, using the exact Schur parametrization. A certified branch-and-bound search then proves max |L| ≤ V + ε: it encloses the polynomial on each box with interval arithmetic and splits until every piece clears the target. The certificate is written to disk and re-checked independently in 30-digit arithmetic. An explicit extremal attains a matching lower bound. Browse the results at /proofs.
Every bound on /proofs is certified: the upper bound is proved by rounding-safe branch-and-bound, and an explicit extremal attains a matching lower bound. So the sharp constant is bracketed in [attained, V + ε]. What differs between results is how tightly that bracket is closed. There are two levels.
Closing an enclosure to a proven exact constant needs a local certificate at the extremal, which is on the roadmap. Until then the honest status is a rigorous bracket plus a recognised candidate. See why we label so carefully.
We are careful to separate certifying a value from claiming it is new. The engine certifies a narrow genre - sharp coefficient functionals (Fekete–Szegő, Hankel, Zalcman, logarithmic and inverse coefficients) over Ma–Minda classes. It screens a broader set (radii, inclusions, membership) and simply catalogues the rest (subordination, distortion, operator-theory results). We do not claim to “verify the literature”.
Each certified value carries an honest provenance tag:
This is the same discipline as the proven / enclosure / screen labels, applied to provenance: a wrong “new” claim is worse than no claim.
It is the step that makes the problem finite. Rather than test infinitely many functions, we rewrite a whole class exactly in terms of a few parameters that range over a box. The bound then becomes a polynomial inequality on that box. On a proof page it is the first lemma, “Schur parametrisation is exact”.
The engine computes with intervals instead of single numbers, so every result is a guaranteed range. Each step is widened to absorb floating-point rounding. So when the engine reports that a value stays below a threshold, that is a proof rather than an estimate. The same idea powers the counterexamples.
It is the search that covers the whole class. The engine splits the parameter box into smaller boxes and certifies each one, splitting further wherever a box is undecided, until the bound holds everywhere. The “boxes” and “certified leaves” counts on a proof page are this search written down. A count in the hundreds of thousands is normal.
Each proof page lists the lemmas it rests on, each one checkable by hand. It links the raw certificate as JSON, the matching papers under “In the literature”, and a plain-language report where one exists. Every certificate is also re-checked independently in 30-digit arithmetic. Nothing asks you to take our word for it.
The open problems page lists bounds we cannot yet prove exactly. Some are certified enclosures with a recognised candidate, where closing the last gap is the open work. Others are conjectures the engine cannot certify at all yet. We list them in the open rather than hide them, because a negative result is still a result.
After the reduction, H₃(1) lives on a seven-dimensional box, and the bound turns loose long before the search can cover it. Roughly ten billion boxes would be needed, which is out of reach. The human proof sidesteps this by reducing the dimension first, by hand, before any search. A machine version of that reduction is the next milestone. The full account is in the hardness map.
A counterexample is a proof that a function fails a property. It is a single point where the defining inequality is violated, certified by interval arithmetic. For starlikeness, it is a point where Re(zf′/f) is provably negative, so the function cannot be starlike there. Each row on the verify page is one such witness, with the point and the certified bound shown.
From the verifier itself. Paste a function into /verify, and if the rigorous tier disproves a property, that verdict is a counterexample. The corpus on the page is the set of these certified disproofs, gathered from running the verifier across the registry. So a witness is a sound enclosure, not a sampled point that happened to look negative.
Usually not. Most functions are not starlike on the whole disk, so a single witness is rarely news on its own. The witnesses that carry weight are the ones that refute a published claim, or that pin the exact radius where a property breaks. We read the corpus with that in mind, rather than by raw count.
1,088 papers are indexed, with extracted claims for starlikeness, convexity, coefficient bounds, radii, and Ma–Minda subordination. /papers searches by title, author, and claim text, and filters by result type. Each machine proof links the matching papers, so you can see whether a bound is already published.
No. We record what each paper claims, namely the class, the functional, and the bound, together with a link to the source. We do not lift the proof itself. None of this enters our own proofs: a language model reads the papers as a librarian, never as a mathematician. A SymPy check then drops any claim that does not match the class it names. See do you use AI in the proofs.
Each machine proof has an “In the literature” section listing the papers in the corpus that touch that class and functional. Family pages list the papers that cite them. The point is to let you cross-check our machine result against published work before relying on either.
The expansions page gives a₂ through a₅ as explicit polynomials in the Schur parameters, for each class. These are the building blocks the proofs rest on, written out so you can read them or reuse them in your own work.
Yes. The site serves JSON for scripted use, including
/api/v2/stats for the live counts and
/api/v2/counterexamples for the certified witnesses. The
certificate behind each proof is downloadable as JSON from its proof page.
The whole registry runs on a single SQLite database, and each proof certificate is a JSON file you can fetch. The coefficient expansions and the proven bounds are also served as static JSON, so a script can read them without scraping the pages.
Two sandboxes put the registry’s functions to work. The crypto lab studies S-box constructions and reports statistical metrics; it never claims a construction is secure, only what the metrics measure. The image lab applies special-function kernels to images. Both run off precomputed data, which is part of why the site stays fast. See how the site is so fast.
Never in the proof path. A language model helps read and catalogue the papers, and that output is gated by a deterministic check and labelled clearly. Every proof is produced by deterministic mathematics, namely interval arithmetic and symbolic computation, with no model anywhere in the chain.
Yes. There is no random step anywhere. Every certificate regenerates from the repository at a recorded commit, and an independent checker re-verifies each one in high precision. If a number on the site ever drifts from what the code computes now, a staleness gate is meant to catch it.
Four are documented, and each has a regression test.
FM1, truncation false negative. A truncated Taylor polynomial of a slowly decaying function, such as the Koebe function, oscillates near |z| = 1, so a naive scan can report a violation where the true function is fine. The fix is a closed-form evaluation or a certified tail bound.
FM2, grid false positive. A grid that stops short of the boundary can miss a violation just beyond it. The fix is the rigorous tier, which covers the whole domain by subdivision rather than sampling.
FM3, interval dependency blow-up. Expanded polynomials overestimate in interval arithmetic on degenerate faces. The fix is a factored evaluator that keeps shared factors intact, so cancellations are seen.
FM4, floating-point unsoundness. The fix is to widen every float operation by its rounding-error bound, and to re-verify each certificate with an independent high-precision check.
In short, grid checks are evidence; the certified tier and its independent recheck are the proof.
Each proof page has a cite button that produces a reference to the machine result. Before you cite it as new, check the “In the literature” section to see whether the bound is already published. If it is, cite the paper; our result then stands as an independent confirmation.
Because honesty is the product. A proven-exact sharp constant is a theorem. A certified enclosure is a rigorous bracket with a candidate inside it. A screen is only evidence. We label each one clearly, in the interface and in the data, so that no result claims more than it can support.
All the heavy computation happens offline. Scripts bake the results into static files, and the pages simply render them. The server does almost no mathematics per request, so it stays quick even though the proofs behind it are large.