Can proofs be embedded in a space parameterised by their semantics?

In Extreme Proofs I: The Irrationality of $\sqrt{2}$, the great John Conway and Joseph Shipman proposed treating the proofs of a theorem as points in a space whose coordinates can be parameterised by certain characteristics:

Other “values” that have been proposed include brevity, generality, constructiveness, visuality, nonvisuality, “surprise,” elementarity, and so on. A single mathematician may hold more than one of the values dear. Clearly the ordering of proofs cannot be a total order.

hence the term extreme proofs, the vertices of this idealised proof simplex, each point maximising a single attribute. Conway & Shipman, Mathematical Intelligencer 35(3), 2013. Every other proof worth reading, they suggest, lives in the convex hull of the extreme proofs. They sketched this idealised space by hand in their paper by comparing six or seven proofs they knew of the irrationality of the square root of two.

Can we realise Conway and Shipman's idea today with LLMs and embedding models? That is, can we ask a model that is saturated on proof benchmarks to write proofs under prompts that each maximise one attribute, embed the results with a multilingual encoder, and see whether the geometry Conway and Shipman drew by hand appears in the embedding.

For the purposes of our analysis, we refine this idea to the following: does a retrieval-trained multilingual text encoder cleanly separate mathematical arguments?

Executive summary

I generated 2,082 proofs of three theorems (infinitude of primes, irrationality of $\sqrt{2}$, Pythagoras) with claude-opus-5: known techniques $\times$ six languages $\times$ two styles, plus prompts asking for one extreme and embedded everything with BGE-M3 BGE is BAAI General Embedding, from the Beijing Academy of Artificial Intelligence. M3 stands for Multi-Linguality, Multi-Functionality, Multi-Granularity. Chen et al., 2024. . The embedding itself mostly measures vocabulary and register, not proof argument: a bag-of-words matches it. Masking the discriminative vocabulary and re-embedding lands in the middle: cross-lingual technique transfer drops from 0.97 to 0.72, and the Latin$\leftrightarrow$CJK block falls to 0.56, but nothing reaches chance (0.20). The idea of Conway and Shipman of there being a convex hull of proof arguments remains unproven. What does separate the extremal directions is two coordinates, and neither of them is related to the embeddings: a character count, and a count of named results a proof invokes.

The corpus

2,082 proofs across three theorems, generated by claude-opus-5 (medium effort) via the Message Batches API. Each record stores its full prompt, model, effort and token usage.

Three arms per theorem:

• Technique arm. Named known proofs (Euclid, Euler product, Fürstenberg, …) $\times$ six languages (en, fr, de, es, zh, ja) $\times$ two styles (terse, verbose) $\times$ five samples.
• Extreme arm. Eight extremal criteria $\times$ six languages $\times$ five samples. No technique is prescribed and instead the prompt asks for e.g. brevity, or elementarity, or machinery.
• Scope arm. Proofs of neighbouring statements ($\sqrt{3}$, $\sqrt[3]{2}$, primes $\equiv 2 \pmod{5}$, the law of cosines…) with no prescribed criterion. Its first cell is the theorem itself, so it is the interior point every extreme should be extreme relative to. The scope arm was built to ask whether the model changes argument when the mathematics forces it — no Euclidean proof exists for primes $\equiv 2 \pmod{5}$, and one does for primes $\equiv 3 \pmod{4}$. But then I realised that those two statements also carry different vocabulary, so we cannot disentangle argument from wording, which is the distinction this article is about. The records are in the repository.

Chinese and Japanese are added to disentangle Indo-European language factors.

Building the instrument

Before embedding, we can measure the corpus by a crude character count to see if we can see our expected axes, and indeed we can. When log-transformed and z-scored within language (script density is assumed to be multiplicative: a Chinese proof of the same content typically runs about $0.57\times$ the length of the English one), we see the direction prompts move length eight to ten times more than the residual language spread within a direction on all three theorems.

What the sphere of cosines looks like

BGE-M3, being a contrastively trained encoder, is empirically anisotropic on a corpus like this: every record is a mathematical proof, so every record shares a topic, therefore the whole corpus huddles in a cap on the unit sphere. The minimum cosine between any two proofs here is about 0.29, between a terse Japanese $\sqrt{2}$ proof against a verbose German counting argument about primes. The mean pair sits at 0.59.

Language is largely additive

Subtracting each language’s mean embedding takes the same-technique/cross-language cosine gap from $+0.012$ to $+0.361$. The minimum cosine level over the corpus is 0.29 and the mean is 0.59, so this is large. And, since we used a mean language vector, this suggests that language enters as a single vector translation added to an otherwise language-independent content vector:

Subtracting that language component drops a language probe from 1.000 to 0.013, below 0.167 being chance, which I cannot account for. Technique classification stays at 1.000. However, that figure is in-sample, and within-class centring sets the six language means to exactly zero, so a linear probe is forced by the arithmetic, not by anything the encoder has captured. Digging further into this I applied centring fitted on one arm and applied to another, and there the removal is only partial: means fitted on the technique arm leave a language probe at 0.43 on the extreme arm against chance 0.17. But those two numbers differ in estimation and in arm at once, so some of the residual may be a register shift rather than leakage. What does hold out of sample is the technique direction: a probe trained on five languages and tested on the held-out sixth scores 1.000 / 0.992 / 0.997 on the three theorems.

While researching I found that this centring result replicates Libovický et al. 2020, which did the same thing with a different encoder. They subtracted each language's mean vector and found that language information mostly disappears. They also found that it does not all go away — the encoders are only partly language-neutral to begin with. I should have spent some time researching the methods I applied and not just the topic, i.e. proof geometry.

Cross-lingual transfer holds

To test the cross-lingual transfer of the embeddings, I trained the technique probe on English only and applied it to the other five languages, on the raw, uncentred embeddings. Technique held with a minimum accuracy of 0.90.

The “near-orthogonal factor subspaces”

While experimenting with the embeddings I noticed that the technique, language and style subspaces look near-orthogonal: the minimum principal angle between technique and language is $78.9^\circ$. At first that seemed interesting; it reads as if these could be cleanly separable, independent factors.

But they are not. Permuting the technique labels within each (language, style) cell gives a null at $77.0^\circ$, with $p(\text{null}\le\text{observed})=0.86$. The measured angle value is not significant.

The reason is the high dimensionality. For random unit vectors in $\mathbb{R}^{n}$, $\mathbb{E}\big[\langle u,v\rangle^{2}\big]=n^{-1}$, so a space holds $e^{\Theta(\varepsilon^{2}n)}$ pairwise $\varepsilon$-orthogonal directions against only $n$ exactly orthogonal ones. At $n=1024$ that gives near-orthogonality without any additional assumptions.

But what about lexicality?

The purpose of this endeavour is to study the proof arguments, but on reflection, many proof techniques and styles rely heavily on uncommon words due to the nature of mathematical prose. To test that, I used the English sub-corpus, holding style out (training on terse records, testing on verbose, so no grid cell appears on both sides) and asked: can TF-IDF alone recover which technique a proof uses?

This suggests indeed technique is recoverable from vocabulary alone. However, this result would be consistent with the encoder reading arguments and with it reading only vocabulary. Separating those two readings would require disentangling vocabulary from the text somehow.

Masking the vocabulary

To further investigate, I rewrote the corpus so the give-away terms were replaced by a neutral placeholder, and asked the same questions again. There are two ways of choosing what to remove, with opposite results:

Named machinery. Masking every entry from a hand-built registry of named results, every mathematician’s surname in six languages, and every technique-specific symbol, does not move the lexicality: 1.000 before and 1.000 after. These do not identify technique.

Descriptive vocabulary. When selecting terms by classifier weight instead (chosen on terse records and tested on verbose) it produces a slope, as can be seen in Figure 5: it takes roughly 400 masked word types per language before a bag of words hits chance on primes and $\sqrt{2}$. About 60% of the text is still on the page when chance is reached. The terms that are doing the most work are squarefree, contradicting, distributivity, contrapositive which are ordinary mathematical prose, not proper nouns.

Does the encoder capture what the bag-of-words did not?

The previous results on disentangling the lexicality from the argument structure were inconclusive. So let's try embedding the masked corpus where the bag-of-words was at chance, and ask whether BGE-M3 still recovers the technique across languages. If it holds, something beyond the masked vocabulary is represented. If it falls to chance with the words, every technique result above is a lexical artefact and Figure 3 was shared technical vocabulary alignment.

It turns out the answer is genuinely in the middle, and ends up more informative than either clean outcome. Figure 6 is the result for the infinitude of primes theorem, with one masked tier (400 word types per language). Where a bag-of-words is at chance (0.20), all transfer directions stay above it, and most by a wide margin.

Three things follow from this. First, the technique geometry is not purely lexical as shown. Second, a large share of the cross-script transfer in Figure 3 depended exactly on the vocabulary the mask removed: the Latin$\leftrightarrow$CJK block drops by 0.38, and French$\to$Chinese collapses to 0.38. The encoder represents something beyond the top-400 discriminative word types, but its cross-script alignment leans on shared technical vocabulary. Third, the one masked cell that stays near-perfect is Japanese$\leftrightarrow$Chinese (0.96–0.98): the two languages that share han characters appear to keep their alignment after the per-language masks, which is exactly where a vocabulary-bridge account would predict this survival.

We are not able to test the convex hull claim

Conway and Shipman claimed that every proof should sit inside the convex hull of the extremes. To test that, I need a way to know when a proof does not fit within any of the known proof arguments. One way would be to get the nearest-centroid across a technique and see how close each proof is to that, but then how do you determine when a proof is too far from this centroid? We can take the 5th percentile: the distance that 95% of the known members fit into. Anything further out than that is called out-of-set. On primes this returns six of eight directions as out-of-set. That is interesting, but what about the others?

On $\sqrt{2}$, everything is out-of-set by this measure, including brevity, which on primes was 0/30. On Pythagoras almost nothing is. These three corpora were built in the same way, and yet this gives three incompatible pictures. Reading twelve of the flagged primes proofs by hand shows what it actually detects: a formal, hedged, and encyclopedic register that moves a record in embedding space without changing its mathematics. So the convex hull claim remains untested. I have no working way I can think of to ask whether a proof has left the known set because every instrument applied so far measures wording.

A coordinate that is not just wording

I asked the LLM for one arm of proofs to use the heaviest machinery it could justify. Then after embedding I checked which known proof each one most resembles by cosine similarity: measure the distance to the average of each technique's proofs, take the closest. Twenty-two of the thirty machinery proofs came back as closest to Fürstenberg. This suggests the similarity measure cannot tell “uses abstract terminology” from “uses powerful theorems.”

So let's try counting the latter directly: the number of distinct named external results a proof invokes, matched from a registry in all six languages.

An obvious objection to this is length: the invoked results count correlates with length at $+0.59$. So what if we compare machinery against the longest 30 technique-arm records? It turns out those are longer than the machinery proofs (length $z$ $+1.45$ vs $+0.91$) and invoke 1.40 results against machinery’s 16.63. So we are not just measuring length as a coordinate. The measure is also script-independent (median CJK/Latin ratio 0.84) which is not obvious for a name-matching instrument as constructed.

However this coordinate has almost no resolution outside the one distinction it was built to show. Seven of the eight directions sit at 0.00–0.13 invoked results. It decisively separates heavy machinery from abstract vocabulary, but nothing else.

Finally, where that leaves the geometry under this analysis: brevity and elementarity separate on length and coincide at zero dependence on results invoked. constructiveness and generality sit at nearly the same length and are $10\times$ apart in dependence. For two coordinates to mean something is the minimum for Conway and Shipman’s geometric framing to be worth taking literally. On this evidence the geometry is real but not substantial. Two coordinates separated the directions, and neither is related to the embeddings: one is character count, the other a registry match. I could not prove that the embedding model encoded any extra geometry.

Limitations

• Only one encoder used. The analysis was checked against only one embedding model and so the artefacts discussed may be model-specific; this could be improved by running the same analysis on separate encoding models.
• Proof correctness is unverified beyond twelve records read by hand. My assumption is that since the model used is saturated on simple proof benchmarks it can be relied upon.
• Registry coverage. The $\sqrt{2}$ and Pythagoras registries were built from the literature rather than validated against their corpora.