The geometry of snowflaked Ptolemaic metric spaces

My coauthors June Huh, Mario Kummer, Oliver Lorscheid, and I just posted a paper called Lorentzian polynomials and matroids over triangular hyperfields, Part 2: Analytic aspects on the arXiv preprint server. This is the first paper of mine to contain a substantial result proved by AI, and also the first to contain a proof formally verified in Lean. So I thought I would take this opportunity to tell a bit of the backstory.

Although our paper is motivated by the general theory of Lorentzian polynomials and matroids with coefficients, which are a bit daunting to explain in a short post, the parts in which AI played a decisive role can be explained in a completely elementary way. I will first state some of our main results, as well as our main open conjecture, in terms of basic linear algebra. Then I will discuss how AI—primarily Chat GPT-5.5—was able to prove a theorem that had previously eluded us.

The \mathbb{T}_q-inequalities

We assume n\geq 4 in what follows, to avoid trivialities.

Definition.

  1. We call an n\times n real matrix A=(A_{ij}) admissible if it is symmetric, has zero diagonal, and has strictly positive off-diagonal entries.
  2. We say that an admissible matrix A satisfies the \mathbb{T}_0-inequalities if, for every quartet \{i,j,k,\ell\}\subseteq[n] with i<j<k<\ell, the maximum of the three products \displaystyle A_{ij}A_{k\ell}, A_{ik}A_{j\ell}, A_{i\ell}A_{jk} is attained at least twice.
  3. Let q>0. We say that an admissible matrix A satisfies the \mathbb{T}_q-inequalities if, for every quartet \{i,j,k,\ell\}\subseteq[n] with i<j<k<\ell, the three numbers \displaystyle (A_{ij}A_{k\ell})^{1/q}, (A_{ik}A_{j\ell})^{1/q},(A_{i\ell}A_{jk})^{1/q} are the side lengths of a possibly degenerate Euclidean triangle.

In a precise sense, the \mathbb{T}_0-inequalities can be regarded as the q\to 0 “tropical limit” of the \mathbb{T}_q-inequalities for q>0. Also, if 0\leq q<q', then every matrix satisfying the \mathbb{T}_q-inequalities automatically satisfies the \mathbb{T}_{q'}-inequalities.

The \mathbb{T}_q-inequalities and Lorentzian signature

It follows from a theorem of Brändén and Huh that an admissible matrix A satisfying the \mathbb{T}_0-inequalities is Lorentzian: it has at most one positive eigenvalue. The appendix to our new paper gives six proofs of the key fact underlying this statement: the leaf-to-leaf distance matrix of every metric tree is Lorentzian. (The \mathbb{T}_0-inequalities are closely related to the celebrated four-point condition characterizing tree metrics in phylogenetic analysis.)

A natural generalization—and strengthening—is to ask whether, for each n, there is a positive constant q=q(n) such that every admissible n\times n matrix satisfying the \mathbb{T}_q-inequalities must be Lorentzian. One might imagine that this follows from a compactness argument, but the space of admissible matrices is not compact, and this noncompactness turns out to be a serious obstacle.

One of our theorems says that such a constant does exist:

Theorem A. For n\geq 4, set

\displaystyle \varepsilon(n):=\log_2\!\left(1+\frac{1}{n-2}\right).

Let A\in\mathbb{R}^{n\times n} be admissible, and suppose that A satisfies the \mathbb{T}_{\varepsilon(n)}-inequalities. Then A is Lorentzian.

Our proof takes a perhaps-unexpected detour through a connection with Euclidean embeddings of metric spaces.

Schoenberg theory

The following result is a variant of a classical theorem of Schoenberg:

Theorem (Schoenberg). Let v_1,\dots,v_m be points in some Euclidean space \mathbb{R}^d, and let

\displaystyle B=\left(\|v_i-v_j\|^2\right)_{1\leq i,j\leq m}.

Then the associated Cayley–Menger matrix

\displaystyle A:=\begin{pmatrix}0&\mathbf{1}^{\top}\\[2pt]\mathbf{1}&B\end{pmatrix}

has at most one positive eigenvalue.

(Although we will not need it here, an appropriately formulated converse is also true.)

Here is the connection with Theorem A. After rescaling A by a positive diagonal matrix, we may arrange that every entry in its first row and first column, apart from the diagonal entry, is equal to 1. Let B be the remaining (n-1)\times(n-1) block, and define d(i,j):=B_{ij}^{1/q}. The \mathbb{T}_q-inequalities for quartets containing the first index are exactly the triangle inequalities for d, so d is a metric on n-1 points. If (X,d^{q/2}) embeds isometrically into Euclidean space, then B is its squared-distance matrix, and Schoenberg’s theorem applies.

Thus Theorem A reduces to the following result of Timothy Faver, Katelynn Kochalski, Mathav Kishore Murugan, Heidi Verheggen, Elizabeth Wesson, and Anthony Weston:

Theorem (FKMVWW). Let m\geq 2, let (X,d) be an m-point metric space, and set

\displaystyle \eta(m):=\log_2\!\left(1+\frac{1}{m-1}\right).

If 0<p<\eta(m), then the snowflaked metric space (X,d^{p/2}) admits an isometric embedding into \mathbb{R}^{m-1}.

Taking m=n-1 and p=q proves Theorem A when q<\varepsilon(n). The endpoint q=\varepsilon(n) follows by a limiting argument.

The word snowflaked is used because, in metric geometry, replacing a metric d by d^\alpha for 0<\alpha<1 is called taking a snowflake of the metric space. (The terminology alludes to the classical Koch snowflake curve.)

The bound is not optimal

For n=4, Theorem A is easy to prove, and one can do better than \varepsilon(4). If A is an admissible 4\times 4 matrix, an explicit calculation—closely related to Heron’s classical formula for the area of a triangle in terms of its side lengths—shows that A is Lorentzian if and only if it satisfies the \mathbb{T}_2-inequalities. Closely related is the fact that the FKMVWW theorem is not optimal when m=3: every three-point metric space can be realized as a triangle in \mathbb{R}^2, so in this case one can take p=2.

Define q(n) to be the supremum of all q \geq 0 such that every admissible n\times n matrix satisfying the \mathbb{T}_q-inequalities is Lorentzian. Theorem A says that q(n) > 0 for all n, and the preceding calculation says that q(4)=2.

An explicit construction in our paper gives the following general upper bound for q(n):

Theorem B. For every n\geq 4,

\displaystyle q(n)\leq p(n):=\begin{cases}2\log_2\!\left(\dfrac{n}{n-2}\right),&\text{if }n\text{ is even},\\[7pt]\log_2\!\left(\dfrac{n+1}{n-3}\right),&\text{if }n\text{ is odd}.\end{cases}

The upper and lower bounds supplied by Theorems A and B agree up to absolute constant factors, and thus \displaystyle q(n)=\Theta(1/n).

We believe that the upper bound gives the correct answer:

Conjecture A. For every n\geq 4, we have q(n)=p(n).

There are two distinct reasons that the lower bound in Theorem A is not sharp:

  1. The exponent in the FKMVWW theorem is not optimal. For example, when m=4—which corresponds to n=5—we have \eta(4)=\log_2(4/3)<1. But a theorem of Blumenthal shows that, for every four-point metric space (X,d), the snowflaked space (X,d^{p/2}) admits an isometric embedding into \mathbb{R}^3 for all 0<p\leq 1. To the best of our knowledge, the optimal general exponent remains open for m>4.
  2. The reduction of Theorem A to the FKMVWW theorem discards some of the extra structure supplied by the \mathbb{T}_q-inequalities.

Evidence for the conjecture

As already mentioned, Conjecture A is true for n=4. Our best additional evidence for the conjecture, aside from the general upper bound in Theorem B, is the following result whose original proof was produced by GPT-5.5 Pro:

Theorem C. q(5) \geq\log_2(3).

Note that Theorem A gives only the weaker lower bound

\displaystyle q(5)\geq \log_2(4/3).

Combining Theorem C with Theorem B gives:

Corollary. q(5) = \log_2(3).

As previously mentioned, the proof of Theorem A discards some extra structure implied by the \mathbb{T}_q-inequalities. We now turn to a more in-depth discussion of this additional structure.

Definition. A metric space (X,d) is Ptolemaic if, for every four points x,y,z,w\in X,

\displaystyle d(x,y)d(z,w)\leq d(x,z)d(y,w)+d(x,w)d(y,z).

The name refers, of course, to the classical Ptolemy inequality in Euclidean geometry. Ptolemaic metric spaces are quite natural objects to study; for example, Schoenberg proved that a real normed vector space is Ptolemaic if and only if its norm comes from an inner product.

The normalization described earlier explains why Ptolemaic spaces arise naturally in our setting: the \mathbb{T}_q-inequalities involving the distinguished first index give the triangle inequalities for d, while the remaining quartet inequalities are exactly the Ptolemy inequalities. From this one can show that Conjecture A is equivalent to the following statement:

Conjecture B. Let m\geq 4 and 0<q<p(m+1). If (X,d) is an m-point Ptolemaic metric space, then the snowflaked space (X,d^{q/2}) admits an isometric embedding into \mathbb{R}^{m-1}.

GPT-5.5 Pro produced a proof of Theorem C (which is equivalent to Conjecture B in the special case m=4) with no substantial mathematical assistance from my coauthors or me.

Brief outline of the proof

The key new idea in ChatGPT’s proof of Theorem C is a clever reduction from an arbitrary four-point Ptolemaic metric to a handful of boundary cases. Blumenthal’s theorem already covers 0 < q\leq 1, so the proof concentrates on 1\leq q\leq\log_2 3. By Schoenberg’s criterion, it is enough to prove that a certain 3\times 3 Gram matrix associated with the snowflaked metric is positive semidefinite; its 2\times 2 principal minors are automatically nonnegative, so the only issue is its determinant. Holding five of the six distances fixed and varying the sixth, ChatGPT observed that this determinant is a concave quadratic function of the q^{\rm th} power of the varying distance. The values allowed by the triangle and Ptolemy inequalities form an interval, so concavity says that it is enough to check the two endpoints. At an endpoint, either a triangle inequality is an equality, meaning that one point lies on a geodesic between two others, or a Ptolemy inequality is an equality; in the latter case, an inversion of the metric turns the configuration into the former. A series of auxiliary lemmas, ultimately reducing matters to line and star metrics, handles these boundary configurations.

Checking and refining the proof

There were parts of the original proof that I did not understand, so I asked GPT-5.5 Pro and Claude Opus a number of questions. Those exchanges eventually produced a significantly simpler version of the argument.

The proof was still fairly complicated and difficult to check, so I enlisted David Renshaw’s help in formalizing it in Lean. David used Claude Code together with Lean to autoformalize the proof. Apart from writing the theorem statement in Lean and supplying Claude Code with the natural-language proof from our draft manuscript, neither David nor I provided further mathematical input. After the harness ran overnight, the resulting Lean development checked successfully. The Lean formalization can be found here.

As a bonus, Claude Code found some simplifications to the case analysis during formalization. We therefore ended up with a proof that is not only formally verified, but also easier for a human to read than the original. (Perhaps this gives a glimmer of hope to those currently despairing about the future of mathematics; there are manifold ways in which AI can help improve human understanding of mathematics—presumably the main goal of whatever it is that we mathematicians claim to do! Of course, there are clearly huge downsides as well, but that is a topic for another post…)

Looking ahead, I view Conjecture B—or, equivalently, Conjecture A—as an interesting challenge for humans, future AI systems, or both.

This entry was posted in A.I., Combinatorics, Formalization, Linear algebra, Tropical geometry and tagged , , , , , . Bookmark the permalink.

Leave a comment