Navier–Stokes Lost in Translation

# Navier–Stokes lost in translation – Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
Source: [https://arxiv.org/html/2610.08144](https://arxiv.org/html/2610.08144)
## Navier–Stokes lost in translation – Why Lean verification of AI autoformalisation does not guarantee correct natural language proofsThanks:\*Corresponding author: a\.hansen@damtp\.cam\.ac\.uk

A\. BastounisAddress:Department of Mathematics, King’s College LondonEmail address:[alexander\.bastounis@kcl\.ac\.uk](mailto:[email protected])F\. CircelliAddress:Department of Applied Mathematics and Theoretical Physics, University of CambridgeEmail address:[fac43@cam\.ac\.uk](mailto:[email protected])andA\. C\. Hansen\*Address:Department of Applied Mathematics and Theoretical Physics, University of CambridgeEmail address:[a\.hansen@damtp\.cam\.ac\.uk](mailto:[email protected])

###### Abstract\.

Autoformalisation is increasingly used to verify mathematical texts, including those generated by AI, as in OpenAI’s announced proof of blow\-up of solutions to the Navier\-Stokes equations\. In this process, an AI system translates the text from a natural language \(NL\) into a formal language such as Lean\. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified\. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully\. In particular, we highlight that the problem of resolving ambiguities in mathematical NL text, which is necessary in order to provide semantically faithful translation, is arbitrarily high up in the Solvability Complexity Index \(SCI\) hierarchy/arithmetical hierarchy \(the SCI=∞=\\infty\)\. Hence, informally, providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem \(which has SCI=1=1\)\. To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean ‘verifications’\. These include OpenAI’s announced Navier\-Stokes proof\. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow\-up of solutions to the Navier\-Stokes equations\.

###### Key words and phrases:

AI Autoformalisation, Navier\-Stokes equations, Solvability Complexity Index hierarchy, boundaries of AI, Hilbert’s 10th problem

###### 2020 Mathematics Subject Classification

35Q30, 03Dxx \(primary\) and 68V20, 68Txx, 03B65 \(secondary\)

## 1\.Introduction: Two types of Autoformalisation

We start by describing the two main types of autoformalisation from a natural language \(NL\) to a formal language:

1. \(i\)Translating an alleged proof in an NL to obtain a formal Lean proof\.Suppose a theorem \(the statement, not including a proof\) has already been faithfully and correctly translated into Lean\. Suppose also the theorem is accompanied by an alleged NL proof\. The goal is to let a machine \(which we will call AI\) translate the NL proof into Lean to obtain a formal proof of the theorem\. Success is declared when the AI has produced a ‘translation’ which Lean accepts as a valid proof \(meaning it compiles\), with no use of Lean’s ‘sorry’ keyword or extra axioms being permitted\.

1. \(ii\)Faithful semantic translation of a mathematical text\.Suppose we are given a mathematical text \(e\.g\. a book or a paper\) written in an NL\. The goal is to let an AI translate every definition, theorem, proposition, proof etc\. in the text to Lean code that compiles, see e\.g\. the example in §[5\.1](https://arxiv.org/html/2610.08144#S5.SS1)\. The definitions, statements and proofs must themselves be translated, semantically preserving the source’s mathematical content\. For a book, this obligation applies throughout and includes the dependencies between concepts and results\. If the stated goal is to validate its proofs, correspondence to the written arguments must also be established\. In particular, a different, provable assertion would not constitute a semantically faithful translation\. This autoformalisation problem is much harder than problem \(i\) above \(see §[4](https://arxiv.org/html/2610.08144#S4)\)\.

Warning:Meeting the success criterion of[\(i\)](https://arxiv.org/html/2610.08144#S1.I1.i1)does not mean that the original NL proof is correct\. Indeed, a full Lean compilation of the ‘translation’ does not guarantee a semantically faithful translation\. The AI could very easily change the semantics of the translation in order to satisfy this success criterion\. For example, the NL proof could be wrong while the ‘translated’ proof is correct \(see Example[2\.1](https://arxiv.org/html/2610.08144#S2.Thmtheorem1)\)\. Another possibility is that both the NL proof and the formal proof are correct, but completely different \(see Example[2\.2](https://arxiv.org/html/2610.08144#S2.Thmtheorem2)\)\. A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes, with \(of course\) different proofs\. The latter happens in OpenAI’s announced proof of blow\-up of Navier\-Stokes equations\. In all cases the correctness of the formal proof does not say anything about the correctness of the NL proof\.

To answer the question: ‘Is the NL argument correct?’ one needs to consider the second form of autoformalisation[\(ii\)](https://arxiv.org/html/2610.08144#S1.I2.i2)\. This is, however, in general an extremely difficult problem, as we discuss in §[4](https://arxiv.org/html/2610.08144#S4)\. In fact, it is strictly harder than the Halting problem\.

Because of the phenomenon of mistranslations – as highlighted in this paper – the NL proof by OpenAI and other autoformalised Lean proofs should not prima facie be trusted without the same peer review process and scrutiny that other proofs are subjected to\. The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments\.

Disclaimer:We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean\.

![Refer to caption](https://arxiv.org/html/2610.08144v1/cubic_squish.jpg)Figure 1\.ChatGPT\-6 \(Astra Ultra\) ‘translates’ the wrong NL ‘proof’ in Example[2\.1](https://arxiv.org/html/2610.08144#S2.Thmtheorem1)into a correct proof in Lean that correctly compiles\.
## 2\.When an AI autoformalised ‘translation’ is not semantically faithful

In order to illustrate the issues with the first type of autoformalisation described in §[1](https://arxiv.org/html/2610.08144#S1)we consider several examples of mistranslation\. We begin with some elementary examples to highlight the issue, and then turn to more technical examples of mistranslation in OpenAI’s announced proof of blow\-up of Navier\-Stokes equations in §[3](https://arxiv.org/html/2610.08144#S3)\.

###### Example 2\.1\(A correct statement with an incorrect NL proof, and a ‘translation’ to a different, correct Lean proof\)\.

Consider the following theorem:

Letp⁡\(x\)=x3−x2−x\+1p\(x\)=x^\{3\}\-x^\{2\}\-x\+1, wherex∈ℝx\\in\\mathbb\{R\}\. Thenp⁡\(x\)⩾0p\(x\)\\geqslant 0forx⩾−1x\\geqslant\-1\.

###### Incorrect NL proof\.

The roots are−1\-1, of multiplicity two, and11, of multiplicity one\. Hence111Note that the ‘hence’ is also dubious without mentioning the leading coefficient ofpp\.,

p⁡\(x\)=\(x−1\)​\(x\+1\)2⩾0,p\(x\)=\(x\-1\)\(x\+1\)^\{2\}\\geqslant 0,since both factors are nonnegative on the stated domain\. ∎

The above proof is incorrect; the multiplicities of the stated roots are wrong and hence the claimed factorisation ofp⁡\(x\)p\(x\)is wrong too\. In the exchange shown in Figure[1](https://arxiv.org/html/2610.08144#S1.F1), a user presented the incorrect NL argument above as their ‘proof’ and asked the chatbot to write this argument as a Lean proof, providing a Lean code that compiles\. The chatbot returned a correct Lean proof by finding the correct multiplicities of the roots\. This example demonstrates how the first form of autoformalisation above can result in a wrong NL proof being mistranslated into a correct Lean proof\.

![Refer to caption](https://arxiv.org/html/2610.08144v1/matrix_example_slim.jpg)Figure 2\.ChatGPT\-6 \(Astra Ultra\) ‘translates’ the correct NL proof in Example[2\.2](https://arxiv.org/html/2610.08144#S2.Thmtheorem2)into a completely different proof in Lean that compiles\.###### Example 2\.2\(A correct statement with a correct NL proof, which is ‘translated’ into a Lean proof with a different mathematical argument \)\.

Consider the following theorem:

LetA=\(ai​j\)A=\(a\_\{ij\}\)be a real symmetricn×nn\\times nmatrix\. Thentr⁡\(A2\)⩾0\\operatorname\{tr\}\(A^\{2\}\)\\geqslant 0\.

###### Correct NL proof\.

DiagonaliseAAin an orthonormal eigenbasis\. Sincetr⁡\(A2\)\\operatorname\{tr\}\(A^\{2\}\)is invariant under a change of basis, we may assumeA=diag⁡\(λ1,…,λn\)A=\\operatorname\{diag\}\(\\lambda\_\{1\},\\ldots,\\lambda\_\{n\}\)\. Now compute

\(2\.1\)tr⁡\(A2\)=∑i\(A2\)i​i=∑i,jai​j​aj​i\.\\operatorname\{tr\}\(A^\{2\}\)=\\sum\_\{i\}\(A^\{2\}\)\_\{ii\}=\\sum\_\{i,j\}a\_\{ij\}a\_\{ji\}\.Asai​j=0a\_\{ij\}=0fori≠ji\\neq jandai​i=λia\_\{ii\}=\\lambda\_\{i\}, this reduces to∑iλi2⩾0\\sum\_\{i\}\\lambda\_\{i\}^\{2\}\\geqslant 0\. ∎

In the exchange shown in Figure[2](https://arxiv.org/html/2610.08144#S2.F2), a user presented the correct NL argument above as their proof and asked the chatbot to write this argument as a Lean proof which compiles\. The chatbot, however, returned a different proof displayed in Figure[2](https://arxiv.org/html/2610.08144#S2.F2)\. The code gives a correct Lean proof, which has a distinctly different argument compared to the original NL proof that the chatbot was asked to write up in Lean\. Indeed, the Lean proof starts directly at \([2\.1](https://arxiv.org/html/2610.08144#S2.E1)\), keeping the original matrixAA: it then usesaj​i=ai​ja\_\{ji\}=a\_\{ij\}to conclude that

∑i,jai​j​aj​i=∑i,jai​j2⩾0\.\\sum\_\{i,j\}a\_\{ij\}a\_\{ji\}=\\sum\_\{i,j\}a\_\{ij\}^\{2\}\\geqslant 0\.The unfaithful translation of the argument simply omits the change of basis and then proceeds in the same manner as the NL proof \(using symmetry rather than diagonality to obtain a sum of squares\)\. Both proofs are correct, yet this example demonstrates how the first form of autoformalisation above can mistranslate a correct NL proof to yield a completely different valid Lean proof\.

## 3\.Mistranslation in practice – OpenAI’s announced Navier\-Stokes proof

The three\-dimensional incompressible Navier\-Stokes regularity problem has a long history\[[11](https://arxiv.org/html/2610.08144#bib.bib11),[18](https://arxiv.org/html/2610.08144#bib.bib18),[55](https://arxiv.org/html/2610.08144#bib.bib55),[48](https://arxiv.org/html/2610.08144#bib.bib48),[42](https://arxiv.org/html/2610.08144#bib.bib42),[24](https://arxiv.org/html/2610.08144#bib.bib24),[47](https://arxiv.org/html/2610.08144#bib.bib47),[29](https://arxiv.org/html/2610.08144#bib.bib29),[18](https://arxiv.org/html/2610.08144#bib.bib18)\]\(we can only cite a small subset of papers here\), dating back to Leray’s fundamental paper from 1934\[[33](https://arxiv.org/html/2610.08144#bib.bib33)\], and was designated a Clay Millennium Prize Problem in 2000\[[23](https://arxiv.org/html/2610.08144#bib.bib23)\]\. In the GitHub repository accompanying its recently announced proof of finite\-time blow\-up of solutions to the Navier\-Stokes equations, OpenAI writes:

> *‘This repository contains Lean 4 formalizations of the results presented in “Finite time blowup for Navier–Stokes” \[their announced NL proof\] and “Finite time blowup for the Euler equation” by OpenAI\.’*

It is natural to ask whether this formalisation in Lean represents a semantically faithful translation of the NL paper, so that we can conclude that the NL paper represents a correct proof? Interestingly, OpenAI’s announced proof becomes a great source for examples of mistranslations, exactly as pointed out in §[2](https://arxiv.org/html/2610.08144#S2)\. In particular, the Lean formalisation does not represent a semantically faithful translation of the NL paper, meaning that the Lean formalisation provides no guarantee that the NL proof is correct\. We provide several examples below \(see also Remark[3\.4](https://arxiv.org/html/2610.08144#S3.Thmtheorem4)\)\.

![Refer to caption](https://arxiv.org/html/2610.08144v1/Figure3Fixed.jpg)Figure 3\.ChatGPT\-6 \(Astra Ultra\) shares our concern that the NL argument in Lemma 8\.6 in the announced proof of blow\-up of Navier–Stokes has not been faithfully translated into Lean\. In particular, there is a discrepancy between Lemma 8\.6 and the cited Lean estimate: the latter uses one additional input derivative to control the same torus derivatives of the output\. See Example[3\.1](https://arxiv.org/html/2610.08144#S3.Thmtheorem1)for details\.### 3\.1\.When the NL paper declares stronger statements than what Lean proves

We commence with an example that complements those in §[2](https://arxiv.org/html/2610.08144#S2)\. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement\.

###### Example 3\.1\(The NL paper claims a stronger inverse estimate than the cited Lean formalisation\)\.

Figure[3](https://arxiv.org/html/2610.08144#S3.F3)concerns the estimate in[Lemma 8\.6, equation \(8\.19\)](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf#page=95), of OpenAI’s*Finite time blowup for Navier–Stokes*\. We compare this estimate with the cited Lean declarations at[commitf9e8bc5](https://github.com/openai/NavierStokesAndEuler/tree/f9e8bc5b38b6e212696e8a30e3e91517af887bbd)\(click to see the documentation on Github\)\. The issue is a change in the order of the input derivatives required to bound the output derivatives\. In particular, we have the following discrepancy\. Withmma nonnegative integer, the comparison in Figure[3](https://arxiv.org/html/2610.08144#S3.F3)is

\(3\.1\)NL paper, equation \(8\.19\):‖N−1​F‖Cym⩽Cm​‖F‖Cym\+4,\\displaystyle\\\|N^\{\-1\}F\\\|\_\{C\_\{y\}^\{m\}\}\\leqslant C\_\{m\}\\\|F\\\|\_\{C\_\{y\}^\{m\+4\}\},\(3\.2\)Lean Estimate:‖N−1​F‖Cym⩽Km​‖F‖Cym\+5\.\\displaystyle\\\|N^\{\-1\}F\\\|\_\{C\_\{y\}^\{m\}\}\\leqslant K\_\{m\}\\\|F\\\|\_\{C\_\{y\}^\{m\+5\}\}\.*Summary: The Lean code produced by OpenAI often has stronger conditions on bounds on the derivatives of various functions than the corresponding results in the NL paper*\.

Above,F:P×𝕋2→ℂF:P\\times\\mathbb\{T\}^\{2\}\\to\\mathbb\{C\}is a function of parameters inPPand a torus variabley∈𝕋2y\\in\\mathbb\{T\}^\{2\}, with𝕋2:=ℝ2/ℤ2\\mathbb\{T\}^\{2\}:=\\mathbb\{R\}^\{2\}/\\mathbb\{Z\}^\{2\}\. The non\-negative constantsCmC\_\{m\},KmK\_\{m\}are independent ofFFbut allowed to depend onmmand the fixed directionvtv\_\{t\}\(which defines an operatorN=vt⋅∇yN=v\_\{t\}\\cdot\\nabla\_\{y\}\)\. Note the above norms only involve torus derivatives\. See §[3\.1\.1](https://arxiv.org/html/2610.08144#S3.SS1.SSS1)for further explanation of the notation\.

The proof of Lemma 8\.6 opens with the following passage \(source paper,[page 96](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf#page=96)\):

> “The divisor bound \(6\.7\) gives\|vt⋅k\|−1⩽C⁡\(1\+\|k\|\)\|v\_\{t\}\\cdot k\|^\{\-1\}\\leqslant C\(1\+\|k\|\)\. Four more derivatives ofFFthan the requested output leave a summable\(1\+\|k\|\)−3\(1\+\|k\|\)^\{\-3\}bound on the Fourier series in two dimensions\. This proves \(8\.19\), smoothness, and uniqueness after fixing the zero Fourier coefficient\. The multiplier commutes with every slow coefficient derivative and preserves reality\.”

The related Lean codes – on the other hand – all use five additional derivatives, not four\. A key example is the following Lean theorem, which appears to bear the closest resemblance to \(8\.19\):

theoremnorm\_derivativeWord\_inverse\_le\(d:Direction\)\{f:SourceP\}

\(hf:ContDiffℝ∞f\)\(hp:Periodicf\)\(w:ListBool\)\(p:P\)\(Y:Plane\)\{C:ℝ\}

\(hzero:∀x∈Icc\(0:ℝ\)1,∀y∈Icc\(0:ℝ\)1,‖f\(p,\(x,y\)\)‖≤C\)

\(hfirst:∀x∈Icc\(0:ℝ\)1,∀y∈Icc\(0:ℝ\)1,

‖SmoothFourierData\.xJet\(w\.length\(\*@\\textcolor\{red\}\{\+5\}@\*\)\)\(slicefp\)\(x,y\)‖≤C\)

\(hsecond:∀x∈Icc\(0:ℝ\)1,∀y∈Icc\(0:ℝ\)1,

‖SmoothFourierData\.xJet\(w\.length\(\*@\\textcolor\{red\}\{\+5\}@\*\)\)

\(SmoothFourierData\.swapFunction\(slicefp\)\)\(x,y\)‖≤C\):

‖derivativeWordw\(slice\(inversedf\)p\)Y‖≤

ParametricTorusInverse\.mixedLossConstantw\.length\*C:=by

havehbound:=SmoothFourierData\.coefficient\_seminorm\_bound\(slice\_smoothhfp\)\(hpp\)

\(w\.length\+1\)hzero\(bysimpaonly\[Nat\.add\_assoc\]usinghfirst\)

\(bysimpaonly\[Nat\.add\_assoc\]usinghsecond\)

calc

\_≤\(\(6\*‖omega⁻¹‖\)\*‖omega‖^w\.length\)\*

coeffSeminorm\(w\.length\+1\)\(coefficientfp\):=

inverse\_derivativeWord\_boundd

\(SmoothFourierData\.rapid\_coefficient\(slice\_smoothhfp\)\(hpp\)\)wY

\_≤\(\(6\*‖omega⁻¹‖\)\*‖omega‖^w\.length\)\*

\(\(3^\(\(w\.length\+1\)\+4\)\*C\)\*∑’k:Frequency,\(weightk^\(\*@\\textcolor\{red\}\{4\}@\*\)\)⁻¹\):=

mul\_le\_mul\_of\_nonneg\_lefthbound\(bypositivity\)

\_=\_:=bysimponly\[ParametricTorusInverse\.mixedLossConstant,Nat\.add\_assoc\];ring

Source \(GitHub permalinks\):openai/NavierStokesAndEuler, commit[f9e8bc5](https://github.com/openai/NavierStokesAndEuler/tree/f9e8bc5b38b6e212696e8a30e3e91517af887bbd)\. File:NavierStokes/SmoothFamilyTorusInverse\.lean\. Declaration:[norm\_derivativeWord\_inverse\_le, lines 1059–1080](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/SmoothFamilyTorusInverse.lean#L1059-L1080)\. Red has been added to highlight aspects relevant to this example\. The displayed Lean code is otherwise unchanged\.

The most important aspects of the above Lean theorem[norm\_derivativeWord\_inverse\_le](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/SmoothFamilyTorusInverse.lean#L1059-L1080)are the two hypotheses:

‖SmoothFourierData\.xJet\(w\.length\(\*@\\textcolor\{red\}\{\+5\}@\*\)\)\(slicefp\)\(x,y\)‖≤C\)

\(hsecond:∀x∈Icc\(0:ℝ\)1,∀y∈Icc\(0:ℝ\)1,

‖SmoothFourierData\.xJet\(w\.length\(\*@\\textcolor\{red\}\{\+5\}@\*\)\)

\(SmoothFourierData\.swapFunction\(slicefp\)\)\(x,y\)‖≤C\)

which222The parameter setPPare the spatial variables which are not relevant to this part of the proof\.should be interpreted as

\|∂m\+5F⁡\(y1,y2\)∂y1m\+5\|⩽C,\|∂m\+5F⁡\(y1,y2\)∂y2m\+5\|⩽C,\\left\|\\frac\{\\partial^\{m\+5\}F\(y\_\{1\},y\_\{2\}\)\}\{\\partial y\_\{1\}^\{m\+5\}\}\\right\|\\leqslant C,\\quad\\left\|\\frac\{\\partial^\{m\+5\}F\(y\_\{1\},y\_\{2\}\)\}\{\\partial y\_\{2\}^\{m\+5\}\}\\right\|\\leqslant C,for everyy=\(y1,y2\)∈𝕋2y=\(y\_\{1\},y\_\{2\}\)\\in\\mathbb\{T\}^\{2\}, and the conclusion

ParametricTorusInverse\.mixedLossConstantw\.length\*C

which333Strictly speaking,wwin OpenAI’s Lean code is defined to be an object in the derivativeWord class: a list of booleans for which each ‘false’ entry corresponds to a derivative in they1y\_\{1\}coordinate and each ‘true’ entry a derivative in they2y\_\{2\}coordinate\.should be interpreted as

\|∂\|w\|N−1​F​\(y1,y2\)∂w\|⩽K\|w\|⋅C,\\left\|\\frac\{\\partial^\{\|w\|\}N^\{\-1\}F\(y\_\{1\},y\_\{2\}\)\}\{\\partial w\}\\right\|\\leqslant K\_\{\|w\|\}\\cdot C,withCCthe same constant as in the hypotheses, and wherewwis a multi\-index\. Technically, to obtain an estimate directly comparable with equation \(8\.19\) in OpenAI’s NL paper, one would need also to take a supremum over all such all multi\-indiceswwwith\|w\|⩽m\|w\|\\leqslant m444This is not explicitly done as part ofnorm\_derivativeWord\_inverse\_le\., thereby obtaining

‖N−1​F‖Cym⩽K^m​‖F‖Cym\+5,\\left\\\|N^\{\-1\}F\\right\\\|\_\{C^\{m\}\_\{y\}\}\\leqslant\\hat\{K\}\_\{m\}\\left\\\|F\\right\\\|\_\{C^\{m\+5\}\_\{y\}\},withK^m=max⁡\(K0,K1,…,Km\)\\hat\{K\}\_\{m\}=\\max\(K\_\{0\},K\_\{1\},\\dotsc,K\_\{m\}\)\. This estimate is then strictly weaker than equation \(8\.19\) due to the extra derivative on the right\-hand side\.

The reason for the above discrepancy is related to the difference in proof method employed by the NL paper and the Lean code\. As the quote above indicates, the NL paper makes use of the convergent series∑k∈ℤ21\(1\+\|k\|\)3\\sum\_\{k\\in\\mathbb\{Z\}^\{2\}\}\\frac\{1\}\{\\left\(1\+\|k\|\\right\)^\{3\}\}by usingm\+4m\+4derivatives\. In contrast, the Lean code displayed above for

\(3\.3\)norm\_derivativeWord\_inverse\_le\\hrefhttps://github\.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/SmoothFamilyTorusInverse\.lean\#L1059\-L1080employs the series∑k∈ℤ21\(1\+\|k1\|\+\|k2\|\)4\\sum\_\{k\\in\\mathbb\{Z\}^\{2\}\}\\frac\{1\}\{\(1\+\|k\_\{1\}\|\+\|k\_\{2\}\|\)^\{4\}\}\(see the exponent ‘4’ highlighted in red in the code \([3\.3](https://arxiv.org/html/2610.08144#S3.E3)\) above\) and thus usesm\+5m\+5derivatives instead\. Tracing the proof of \([3\.3](https://arxiv.org/html/2610.08144#S3.E3)\) we find that the series arises from applying the Lean theorem[coefficient\_seminorm\_bound](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/SmoothFourierData.lean#L368-L387), just as Figure[3](https://arxiv.org/html/2610.08144#S3.F3)mentions\. Consequently, the Lean results discussed in this section are weaker555In fact, some such Lean results are actually incomparable with \([3\.1](https://arxiv.org/html/2610.08144#S3.E1)\), due to the mismatch in the type of derivative\. For example, the Lean theoreminverse\_finiteJetsuses mixed derivatives, not just torus derivatives\. Note however that these results are still usingm\+5m\+5derivatives\.than \([3\.1](https://arxiv.org/html/2610.08144#S3.E1)\) in the NL proof\.

#### 3\.1\.1\.Explanation of the notation and technical information

The variabley=\(y1,y2\)y=\(y\_\{1\},y\_\{2\}\)belongs to a two\-dimensional torus𝕋2=ℝ2/ℤ2\\mathbb\{T\}^\{2\}=\\mathbb\{R\}^\{2\}/\\mathbb\{Z\}^\{2\}\. The fixed vector and differential operator in Lemma 8\.6 are

vt=\(2−1,1\),N=vt⋅∂y=\(2−1\)∂y1\+∂y2\.v\_\{t\}=\(\\sqrt\{2\}\-1,1\),\\qquad N=v\_\{t\}\\cdot\\partial\_\{y\}=\(\\sqrt\{2\}\-1\)\\partial\_\{y\_\{1\}\}\+\\partial\_\{y\_\{2\}\}\.The subscriptttis specified in[equation \(6\.2\)](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf#page=63)of the source paper\. HereF:𝕋2→ℂF:\\mathbb\{T\}^\{2\}\\to\\mathbb\{C\}is smooth, with zero normalized Haar mean:∫\[0,1\]2F⁡\(y\)​𝑑y=0\\int\_\{\[0,1\]^\{2\}\}F\(y\)\\,\\mathrm\{d\}y=0\. The notationN−1​FN^\{\-1\}Fdenotes the unique smooth zero\-mean solutionφ\\varphiofN​φ=FN\\varphi=F\. The zero\-mean requirement assures this solution is uniquely specified \(else any solution, via addition of a constant, yields another\)\. For smoothG:𝕋2→ℂG:\\mathbb\{T\}^\{2\}\\to\\mathbb\{C\}and a nonnegative integerrr, the following norm is defined:

‖G‖Cyr:=max⁡supy∈𝕋2a,b⩾0a\+b⩽r⁡\|∂y1a∂y2bG⁡\(y\)\|,a,b∈ℕ\.\\\|G\\\|\_\{C\_\{y\}^\{r\}\}:=\\max\_\{\\begin\{subarray\}\{c\}a,b\\geqslant 0\\\\ a\+b\\leqslant r\\end\{subarray\}\}\\sup\_\{y\\in\\mathbb\{T\}^\{2\}\}\|\\partial\_\{y\_\{1\}\}^\{a\}\\partial\_\{y\_\{2\}\}^\{b\}G\(y\)\|,\\qquad a,b\\in\\mathbb\{N\}\.The subscriptyymeans that other variables are held fixed\. This is relevant in the caseGGis of the formG⁡\(y\)=F⁡\(p,y\)G\(y\)=F\(p,y\)for someF:P×𝕋2→ℂF:P\\times\\mathbb\{T\}^\{2\}\\to\\mathbb\{C\}and some fixedpp\.

### 3\.2\.When a statement and its proof in the NL paper are both mistranslated into Lean

We now give an example that goes further than Example[2\.2](https://arxiv.org/html/2610.08144#S2.Thmtheorem2)in §[2](https://arxiv.org/html/2610.08144#S2)\. In the following example the AI autoformalisation results in a Lean proof of a different bound obtained by a substantively different mathematical argument\.

![Refer to caption](https://arxiv.org/html/2610.08144v1/NavierStokes2.jpg)Figure 4\.ChatGPT\-6 \(Astra Ultra\) shares our concern that the proof of the pressure\-flux bound \(10\.19\) in the announced proof of blow\-up of Navier–Stokes is not semantically faithfully translated into Lean\. Both the stated bound and the mathematical argument used to prove it differ from the cited Lean estimate\. Example[3\.3](https://arxiv.org/html/2610.08144#S3.Thmtheorem3)explains this in further detail, including the notation\.###### Example 3\.3\(The NL paper’s pressure\-flux bound and its proof are both mistranslated\)\.

Figure[4](https://arxiv.org/html/2610.08144#S3.F4)concerns the estimate in[equation \(10\.19\)](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf#page=123)of OpenAI’s*Finite time blowup for Navier–Stokes*\. We compare this estimate, together with its proof, with the cited Lean declaration at[commitf9e8bc5](https://github.com/openai/NavierStokesAndEuler/tree/f9e8bc5b38b6e212696e8a30e3e91517af887bbd)\. The issue here is not only a change in the bound, but also a change in the mathematical argument used to establish it\. In particular, we have the following discrepancy: withR⩾1R\\geqslant 1, the comparison in Figure[4](https://arxiv.org/html/2610.08144#S3.F4)is

\(3\.4\)NL, equation \(10\.19\):\|∫πw⋅∇χR\|⩽CTR\[\(BR\+1\)BR1/2\+R−3/4BR3/4\],for a\.e\.t∈\(0,T\),\\displaystyle\\Bigl\|\\int\\pi\\,w\\cdot\\nabla\\chi\_\{R\}\\Bigr\|\\leqslant\\frac\{C\_\{T\}\}\{R\}\\Bigl\[\(B\_\{R\}\+1\)B\_\{R\}^\{1/2\}\+R^\{\-3/4\}B\_\{R\}^\{3/4\}\\Bigr\],\\text\{ for a\.e\. \}t\\in\(0,T\),\(3\.5\)Lean estimate:\|∫πw⋅∇χR\|⩽CT\[\(BR1/2\+1\)\(ARR\+1R2\)\+R−7/4BR3/4\],∀t∈\(0,T\),\\displaystyle\\Bigl\|\\int\\pi\\,w\\cdot\\nabla\\chi\_\{R\}\\Bigr\|\\leqslant C\_\{T\}\\Bigl\[\(B\_\{R\}^\{1/2\}\+1\)\\Bigl\(\\frac\{A\_\{R\}\}\{R\}\+\\frac\{1\}\{R^\{2\}\}\\Bigr\)\+R^\{\-7/4\}B\_\{R\}^\{3/4\}\\Bigr\],\\forall t\\in\(0,T\),where both the left hand side and the right hand side of both \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\) and \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\) depend ontt; see below for explanation of the notation\. The NL paper’s bound is stated purely in terms ofBRB\_\{R\}, whereas the Lean estimate additionally depends onARA\_\{R\}\. HereCTC\_\{T\}is a finite nonnegative constant, allowed to depend onTT\(which itself is the maximum timescale for which the bounds are considered\) and the norm conventions, but not onRR\. Although[equation \(10\.17\)](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf#page=122)in the NL paper boundsBRB\_\{R\}above usingARA\_\{R\}, it cannot be used to eliminateARA\_\{R\}from the Lean estimate to recover \(10\.19\); the two bounds in \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\) and \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\) are therefore hard to compare\.666In fact, the purpose of the lemma is to establish thatw=0w=0and hence the \(equal to00\) bound on the right hand side of \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\) is stricter than the \(non\-zero\) bound on the right hand side of \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\)\. However, this is only established after completing the entire proof of Lemma 10\.5\.

The closest Lean code to \(10\.19\) \(equation \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\) in our paper\) is the following result:

\{pq:PressureField\}\(H:PressureRecovery\.HypothesesTuvpq\)

\(M\(\*@\\ensuremath\{\{\}\_0\}@\*\)U\(\*@\\ensuremath\{\{\}\_0\}@\*\)G\(\*@\\ensuremath\{\{\}\_0\}@\*\):ℝ\(hM\(\*@\\ensuremath\{\{\}\_0\}@\*\):0≤M\(\*@\\ensuremath\{\{\}\_0\}@\*\)\)\(hU\(\*@\\ensuremath\{\{\}\_0\}@\*\):0≤U\(\*@\\ensuremath\{\{\}\_0\}@\*\)\)\(hG\(\*@\\ensuremath\{\{\}\_0\}@\*\):0≤G\(\*@\\ensuremath\{\{\}\_0\}@\*\)\)

\(hM:∀t∈Icc0T,MemLp\(funx=\>\(u\-v\)\(t,x\)\)2volume∧

comparisonLpNorm2\(funx=\>\(u\-v\)\(t,x\)\)≤M\(\*@\\ensuremath\{\{\}\_0\}@\*\)\)

\(hU:∀t∈Icc0T,MemLp\(funx=\>u\(t,x\)\)3volume∧

comparisonLpNorm3\(funx=\>u\(t,x\)\)≤U\(\*@\\ensuremath\{\{\}\_0\}@\*\)\)

\(hG:∀t∈Icc0T,∀ij:Fin3,

Integrable\(tensorDiffuvtij\)volume∧comparisonLpNorm1\(tensorDiffuvtij\)≤G\(\*@\\ensuremath\{\{\}\_0\}@\*\)\):

∃CP:ℝ,0≤CP∧∀R:ℝ,1≤R→∀t∈Ioo0T,

\|\(\*@\\ensuremath\{\\int\}@\*\)x,\(p\-q\)\(t,x\)\*fderivℝ\(ComparisonCutoffs\.weightR\)x\(\(u\-v\)\(t,x\)\)\|≤CP\*

\(\(cutoffL6\(ComparisonCutoffs\.cutoffR\)\(u\-v\)t^\(1/2:ℝ\)\+1\)\*

\(dissipationRoot\(ComparisonCutoffs\.cutoffR\)\(u\-v\)t/R\+1/R^2\)\+

R^\(\-\(7/4:ℝ\)\)\*cutoffL6\(ComparisonCutoffs\.cutoffR\)\(u\-v\)t^\(3/4:ℝ\)\):=by

obtain\(\*@\\ensuremath\{\\langle\}@\*\)CP,hCP,hbound\(\*@\\ensuremath\{\\rangle\}@\*\):=exists\_uniform\_canonicalCutoffFlux\_boundM\(\*@\\ensuremath\{\{\}\_0\}@\*\)U\(\*@\\ensuremath\{\{\}\_0\}@\*\)G\(\*@\\ensuremath\{\{\}\_0\}@\*\)hM\(\*@\\ensuremath\{\{\}\_0\}@\*\)hU\(\*@\\ensuremath\{\{\}\_0\}@\*\)hG\(\*@\\ensuremath\{\{\}\_0\}@\*\)

refine\(\*@\\ensuremath\{\\langle\}@\*\)CP,hCP,?\_\(\*@\\ensuremath\{\\rangle\}@\*\)

introRhRtht

haveht’:t∈Icc0T:=Ioo\_subset\_Icc\_selfht

havehu:=NavierStokes\.PeriodicUniqueness\.spatial\_smoothH\.smooth\_uht’

havehv:=NavierStokes\.PeriodicUniqueness\.spatial\_smoothH\.smooth\_vht’

exact\(actual\_flux\_integrable\_and\_le\_canonicalNormHht\(zero\_lt\_one\.trans\_lehR\)huhv\)\.2\.trans

\(hboundRhRuvthuhv\(hMtht’\)\.1\(hUtht’\)\.1\(funij=\>\(hGtht’ij\)\.1\)

\(hMtht’\)\.2\(hUtht’\)\.2\(funij=\>\(hGtht’ij\)\.2\)\)

Source \(GitHub permalinks\):openai/NavierStokesAndEuler, commit[f9e8bc5](https://github.com/openai/NavierStokesAndEuler/tree/f9e8bc5b38b6e212696e8a30e3e91517af887bbd)\. File:NavierStokes/R3/PressureFlux\.lean\. Declaration:[exists\_uniform\_actual\_pressure\_flux\_bound, line 576](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFlux.lean#L576)\.

Note that similar bounds \(which are nonetheless distinct from \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\)\) appear in

and[canonicalCutoffFlux\_bound](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFlux.lean#L516-L543)777In addition, there is a similar argument that appears in the fileNavierStokes/R3StressPressureEstimate\.leanas part of the definition of[regularized\_flux\_Bound](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3StressPressureEstimate.lean#L38)\. Once again the bound established there is different from the one in \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\), and, intriguingly, does not appear to be used to prove the Navier Stokes theorem proposed by OpenAI\. It is instead proven as one of the steps in the Lean compilation phase, but it is not directly used\.\. The bound \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\) is given in the following Lean code, taken from that of[exists\_uniform\_actual\_pressure\_flux\_bound, Line 576](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFlux.lean#L585-L589)\.

\(\(cutoffL6\(ComparisonCutoffs\.cutoffR\)\(u\-v\)t^\(1/2:ℝ\)\+1\)\*

\(dissipationRoot\(ComparisonCutoffs\.cutoffR\)\(u\-v\)t/R\+1/R^2\)\+

R^\(\-\(7/4:ℝ\)\)\*cutoffL6\(ComparisonCutoffs\.cutoffR\)\(u\-v\)t^\(3/4:ℝ\)\)

The discrepancy in \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\) above arises through the diverging proof methods employed by the NL paper and the Lean code\. It is beyond the scope, and besides the point, of this article to go into the full technical details of the proof technique for the NL paper’s estimate \(10\.19\) \(in this paper, \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\)\)\. More information is provided below, but in summary three of the main reasons for the differences between the results and strategy used by the NL paper and the Lean argument are as follows:

1. \(1\)The Lean proof does not rely on the boundedness of the Riesz transform as a map fromL3/2→L3/2L^\{3/2\}\\to L^\{3/2\}; it instead invokes Sobolev embedding to move toL2L^\{2\}and uses the boundedness of the Riesz transform inL2L^\{2\}\. The additional derivative involved in the Sobolev embedding is why \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\) featuresARA\_\{R\}\.
2. \(2\)The Lean proof applies Hölder’s inequality with different exponents, which changes the bounds at the end\.
3. \(3\)In the Lean proof, the left hand integral in \([3\.4](https://arxiv.org/html/2610.08144#S3.E4)\) is explicitly shown to be continuous in time\. This ensures that the statement for almost everyt∈\(0,T\)t\\in\(0,T\)can be upgraded to a statement that avoids the ‘almost every’ qualifier\.

#### 3\.2\.1\.Explanation of the notation and technical information

For context, inequality \(10\.19\) appears itself in the proof of a velocity uniqueness result, namely Lemma 10\.5\. In the proof of Lemma 10\.5, using the language of the NL paper, one chooses0⩽φ⩽10\\leqslant\\varphi\\leqslant 1to be smooth, compactly supported and equal to one on the unit ball\. ForR⩾1R\\geqslant 1, they writeφR​\(x\)=φ⁡\(x/R\)\\varphi\_\{R\}\(x\)=\\varphi\(x/R\)andχR=φR8\\chi\_\{R\}=\\varphi^\{8\}\_\{R\}\. Continuing, the NL paper states: ‘*LetRiR\_\{i\}be the Riesz transform with Fourier multiplier operatori​ξi/‖ξ‖2i\\xi\_\{i\}/\\\|\\xi\\\|\_\{2\}\.*’ The NL proof of Lemma 10\.5 begins by assuming that\(v,P\)\(v,P\)and\(u,p\)\(u,p\)are two solutions – withvv\(respectivelyuu\) the velocity andPP\(respectivelypp\) the pressure – to a constructed Navier Stokes problem\. The NL proof definesw:=v−uw:=v\-uandπ:=P−p\\pi:=P\-pand proceeds to establish the vanishing ofww888The Lean proof actually usesw=u−vw=u\-vandπ=p−P\\pi=p\-P, with the sign difference carried through in further definitions\.; the estimate \(10\.19\) is a stepping stone towards this result\. Note thatv,u,wv,u,wall depend on a time parameterttas well as spatial parameters; the time parameter is suppressed throughout the remaining discussion\. The proof also defines a distributionπ∗=∑i,jRi​Rj​gi​j\\pi\_\{\*\}=\\sum\_\{i,j\}R\_\{i\}R\_\{j\}g\_\{ij\}whereRi,RjR\_\{i\},R\_\{j\}are Riesz transforms, and whereg=\(gi​j\)i,j∈\{1,2,3\}g=\(g\_\{ij\}\)\_\{i,j\\in\\\{1,2,3\\\}\}withgi​j=vi​vj−ui​uj=wi​wj\+wi​uj\+ui​wjg\_\{ij\}=v\_\{i\}v\_\{j\}\-u\_\{i\}u\_\{j\}=w\_\{i\}w\_\{j\}\+w\_\{i\}u\_\{j\}\+u\_\{i\}w\_\{j\}\. As indicated in Figure[4](https://arxiv.org/html/2610.08144#S3.F4), using the NL paper’s notation,

AR:=\(∫χR​\|∇w\|2\)1/2,BR:=‖φR4​w‖L6,A\_\{R\}:=\\Bigl\(\\int\\chi\_\{R\}\|\\nabla w\|^\{2\}\\Bigr\)^\{1/2\},\\qquad B\_\{R\}:=\\\|\\varphi\_\{R\}^\{4\}w\\\|\_\{L^\{6\}\},so thatARA\_\{R\}is a localizedL2L^\{2\}gradient norm andBRB\_\{R\}a localizedL6L^\{6\}velocity norm\.

The purpose of definingπ∗\\pi\_\{\*\}is that it is an attempt to get an explicit approximation forπ\\piin terms of the velocity fields; hence instead of directly analysing the integrand in \(10\.19\), one replacesπ\\piin this term byπ∗\\pi\_\{\*\}999A large part of the NL proof of Lemma 10\.5 addresses this issue; ultimately, it suffices to show that∇π=∇π∗\\nabla\\pi=\\nabla\\pi\_\{\*\}in the sense of distributions\.\. The integrand is then factored into a product of two terms:φR4​π∗\\varphi\_\{R\}^\{4\}\\pi\_\{\*\}and another test function containingφR3\\varphi\_\{R\}^\{3\}\. The Lean proof differs here, in that it splits the integral intoφR2​π∗\\varphi\_\{R\}^\{2\}\\pi\_\{\*\}and another test function containingφR5\\varphi\_\{R\}^\{5\}; we shall see the consequences of this change later\.

The NL proof now tries to boundφR4​π∗\\varphi\_\{R\}^\{4\}\\pi\_\{\*\}\. The strategy here is to moveφR4\\varphi\_\{R\}^\{4\}into the argument of the Riesz transformations in the definition ofπ∗\\pi\_\{\*\}; doing so ensures that these Riesz transforms are being applied to functions with compact support inLpL^\{p\}spaces\. In doing so one must pay a penalty, sincea​Ri​b≠Ri​a​baR\_\{i\}b\\neq R\_\{i\}abin general for functionsa,ba,b\. Hence \(10\.18\) in the NL paper establishes that

\(3\.6\)φR4​π∗=∑i,jRi​Rj​\(φR4​gi​j\)\+∑i,j\[φR4,Ri​Rj\]​gi​j\\varphi\_\{R\}^\{4\}\\pi\_\{\*\}=\\sum\_\{i,j\}R\_\{i\}R\_\{j\}\(\\varphi\_\{R\}^\{4\}g\_\{ij\}\)\+\\sum\_\{i,j\}\[\\varphi\_\{R\}^\{4\},R\_\{i\}R\_\{j\}\]g\_\{ij\}where\[⋅,⋅\]\[\\cdot,\\cdot\]is the standard commutator\.

There are a number of differences in the approach the Lean argument uses here\. As mentioned before, the proof in Lean takes out a factor ofφR2\\varphi\_\{R\}^\{2\}instead ofφR4\\varphi\_\{R\}^\{4\}\. Mathematically, the Lean argument is the following calculation101010Lean takes the real parts of many terms in this bound, but this is not especially important for our exposition\.

∫π​w⋅∇χR\\displaystyle\\int\\pi w\\cdot\\nabla\\chi\_\{R\}=∑i,j∈\{1,2,3\}∫gi​jRiRj\(w⋅∇φR8\)=∑i,j∈\{1,2,3\}∫gi​jRiRj\(w⋅8φR2φR5∇φR\)\\displaystyle=\\sum\_\{i,j\\in\\\{1,2,3\\\}\}\\int g\_\{ij\}R\_\{i\}R\_\{j\}\(w\\cdot\\nabla\\varphi\_\{R\}^\{8\}\)=\\sum\_\{i,j\\in\\\{1,2,3\\\}\}\\int g\_\{ij\}R\_\{i\}R\_\{j\}\(w\\cdot 8\\varphi^\{2\}\_\{R\}\\varphi^\{5\}\_\{R\}\\nabla\\varphi\_\{R\}\)\(3\.7\)=8∑i,j∫φR2gi​jRiRj\(w⋅φR5∇φR\)\+8∑i,j∫gi​j\[RiRj,φR2\]\(w⋅φR5∇φR\)\\displaystyle=8\\sum\_\{i,j\}\\int\\varphi\_\{R\}^\{2\}g\_\{ij\}R\_\{i\}R\_\{j\}\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\+8\\sum\_\{i,j\}\\int g\_\{ij\}\[R\_\{i\}R\_\{j\},\\varphi\_\{R\}^\{2\}\]\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)where the first equality is the Lean code[actual\_flux\_eq\_canonicalCutoffFlux](https://github.com/openai/NavierStokesAndEuler/blob/main/NavierStokes/R3/PressureFlux.lean#L211-L219), the second equality is contained in the Lean code[multiplier\_r\_eq\_weight\_deriv](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFluxTest.lean#L26-L34), as well as the code in[cutoffTestandcutoffTest\_flux\_identity](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFluxTest.lean#L284-L291)and the third equality uses the Lean codes given by the Lean theorem[pressurePair\_decomposition](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFlux.lean#L251-L267)and[norm\_cutoff\_pressurePair\_le\_local\_commutator](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFlux.lean#L372-L377)\.

Both the NL proof and Lean proof then attempt to bound the first term in \([3\.6](https://arxiv.org/html/2610.08144#S3.E6)\) and \([3\.7](https://arxiv.org/html/2610.08144#S3.E7)\) respectively111111We do not comment here on how the second sum is treated by Lean and the NL, since differences in the bound and approach can easily be seen by observing the first sum\.\. Here, there are substantial differences\. The NL proof attempts to obtain anL3/2L^\{3/2\}bound on the first term\. It uses Hölder’s inequality to show thatφR4​gi​j∈L3/2\\varphi\_\{R\}^\{4\}g\_\{ij\}\\in L^\{3/2\}and theL3/2→L3/2L^\{3/2\}\\to L^\{3/2\}boundedness of the Riesz transforms \(which is established by citing\[[53](https://arxiv.org/html/2610.08144#bib.bib53)\]\) to get a bound of the form‖Ri​Rj​\(φR4​gi​j\)‖3/2⩽C​‖φR4​gi​j‖3/2⩽C′​\(‖φR4​w‖6\+1\)​‖w‖2⩽C′′​\(BR\+1\)\\\|R\_\{i\}R\_\{j\}\(\\varphi^\{4\}\_\{R\}g\_\{ij\}\)\\\|\_\{3/2\}\\leqslant C\\\|\\varphi^\{4\}\_\{R\}g\_\{ij\}\\\|\_\{3/2\}\\leqslant C^\{\\prime\}\(\\\|\\varphi^\{4\}\_\{R\}w\\\|\_\{6\}\+1\)\\\|w\\\|\_\{2\}\\leqslant C^\{\\prime\\prime\}\(B\_\{R\}\+1\), whereC,C′,C′′C,C^\{\\prime\},C^\{\\prime\\prime\}are all \(potentially different\) constants that can depend onTT\.

By contrast, the Lean proof does not rely on the above citation\[[53](https://arxiv.org/html/2610.08144#bib.bib53)\]\. Instead, it begins by using Hölder’s inequality \(with Hölder conjugates66and6/56/5\) to obtain

\|∫φR2gi​jRiRj\(w⋅φR5∇φR\)\|⩽∥φR2gi​j∥6/5∥RiRj\(w⋅φR5∇φR\)∥6\.\\left\|\\int\\varphi\_\{R\}^\{2\}g\_\{ij\}R\_\{i\}R\_\{j\}\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\right\|\\leqslant\\\|\\varphi\_\{R\}^\{2\}g\_\{ij\}\\\|\_\{6/5\}\\\|R\_\{i\}R\_\{j\}\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\\|\_\{6\}\.
We will first look at how the Lean argument bounds the right hand term∥RiRj\(w⋅φR5∇φR\)∥6\\\|R\_\{i\}R\_\{j\}\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\\|\_\{6\}\(as in the lean code[lpNorm\_six\_rieszTest\_le](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/RieszTestOperators.lean#L223-L239)and[riesz\_rTest\_bound](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFlux.lean#L289-L305)\)\. First, a Sobolev embedding theorem \(bounding theL6L^\{6\}norm by a multiple of theL2L^\{2\}norm of the derivative, because this is an argument done over the spatial variables which are in three dimensions\) is used, as in the file[smooth\_eLpNorm\_six\_toReal\_le](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/SmoothSobolevL6.lean#L140-L150)\. Next, an interchange of derivatives with the Riesz transform \(which comes from the Fourier multipliers\) as stated in both[pderiv\_rieszTest](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/RieszTestOperators.lean#L89-L100)and[partial\_rieszTest](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/RieszTestOperators.lean#L102-L104)is employed to move the gradient operator inside the transform\. Finally, the argument uses the boundedness of the Riesz operators from Schwartz functions inL2L^\{2\}to functions inL2L^\{2\}\(which follows easily from considering the Fourier multipliers of these operators\) as in each of[integral\_norm\_sq\_rieszTest\_le](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/RieszL2Bounds.lean),[lpNorm\_two\_fderiv\_rieszTest\_le](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/RieszTestOperators.lean#L184-L214)and[rieszTest\_memLp\_and\_l2\_bound](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/RieszL2Bounds.lean#L165-L169)\. Symbolically, the calculation is as follows:

∥RiRj\(w⋅φR5∇φR\)∥6⩽C∥∇RiRj\(w⋅φR5∇φR\)∥2⩽C′∥RiRj∇\(w⋅φR5∇φR\)∥2⩽C′∥∇\(w⋅φR5∇φR\)∥2,\\displaystyle\\\|R\_\{i\}R\_\{j\}\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\\|\_\{6\}\\leqslant C\\\|\\nabla R\_\{i\}R\_\{j\}\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\\|\_\{2\}\\leqslant C^\{\\prime\}\\bigg\\\|R\_\{i\}R\_\{j\}\\nabla\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\bigg\\\|\_\{2\}\\leqslant C^\{\\prime\}\\\|\\nabla\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\\\|\_\{2\},whereCCis a constant from the Sobolev inequality andC′C^\{\\prime\}is another constant\. In[norm\_fderiv\_r\_le\_raw](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFluxTest.lean#L139-L184), the Lean proof then bounds \(using the product rule\), forx∈ℝ3x\\in\\mathbb\{R\}^\{3\}\(and fixing the time parameter\)

∥∇\(w⋅φR5∇φR\)\(x\)∥ℓ2⩽\\displaystyle\\\|\\nabla\(w\\cdot\\varphi\_\{R\}^\{5\}\\nabla\\varphi\_\{R\}\)\(x\)\\\|\_\{\\ell\_\{2\}\}\\leqslantφR5​\(x\)​‖∇φR​\(x\)‖ℓ2​‖∇w​\(x\)‖o​p\+φR5​‖∇2φR​\(x\)‖o​p​‖w⁡\(x\)‖ℓ2\\displaystyle\\,\\varphi^\{5\}\_\{R\}\(x\)\\\|\\nabla\\varphi\_\{R\}\(x\)\\\|\_\{\\ell\_\{2\}\}\\\|\\nabla w\(x\)\\\|\_\{op\}\+\\varphi\_\{R\}^\{5\}\\\|\\nabla^\{2\}\\varphi\_\{R\}\(x\)\\\|\_\{op\}\\\|w\(x\)\\\|\_\{\\ell\_\{2\}\}\+5​φR​\(x\)4​‖∇φR​\(x\)‖ℓ22​‖w⁡\(x\)‖ℓ2\.\\displaystyle\+5\\varphi\_\{R\}\(x\)^\{4\}\\\|\\nabla\\varphi\_\{R\}\(x\)\\\|^\{2\}\_\{\\ell\_\{2\}\}\\\|w\(x\)\\\|\_\{\\ell\_\{2\}\}\.
Some further simplification is done \(see for example[norm\_fderiv\_r\_le\_amplitude](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/PressureFluxTest.lean#L187-L225)\), but ultimately this expression leads to theAR/R\+1/R2A\_\{R\}/R\+1/R^\{2\}term present in \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\)\. WhenφR​\(x\)\\varphi\_\{R\}\(x\)was defined, it was done so thatφR​\(x\)∈\[0,1\]\\varphi\_\{R\}\(x\)\\in\[0,1\],‖∇φR​\(x\)‖ℓ2⩽C/R\\\|\\nabla\\varphi\_\{R\}\(x\)\\\|\_\{\\ell\_\{2\}\}\\leqslant C/Rand‖∇2φR​\(x\)‖o​p⩽C2/R2\\\|\\nabla^\{2\}\\varphi\_\{R\}\(x\)\\\|\_\{op\}\\leqslant C\_\{2\}/R^\{2\}\. TheARA\_\{R\}term comes from movingφR4\\varphi\_\{R\}^\{4\}inside the norm in‖∇w​\(x\)‖o​p\\\|\\nabla w\(x\)\\\|\_\{op\}\.

Finally, we note that theBR1/2\+1B\_\{R\}^\{1/2\}\+1term that appears in the Lean statement \([3\.5](https://arxiv.org/html/2610.08144#S3.E5)\) comes from using the definition ofgi​j=wi​wj\+wi​uj\+ui​wjg\_\{ij\}=w\_\{i\}w\_\{j\}\+w\_\{i\}u\_\{j\}\+u\_\{i\}w\_\{j\}to bound‖φR2​gi​j‖6/5\\\|\\varphi\_\{R\}^\{2\}g\_\{ij\}\\\|\_\{6/5\}\. Indeed,\|φR2​gi​j\|⩽2​\|u\|​\|w\|\+\|φR​w\|2\|\\varphi\_\{R\}^\{2\}g\_\{ij\}\|\\leqslant 2\|u\|\|w\|\+\|\\varphi\_\{R\}w\|^\{2\}is established pointwise121212Technically, the Lean theoremnorm\_weighted\_tensorDiff\_leestablishes the result\|s2​gi​j\|⩽2​\|u​\|\|w\|\+\|​s​w\|2\|s^\{2\}g\_\{ij\}\|\\leqslant 2\|u\|\|w\|\+\|sw\|^\{2\}for any0⩽s⩽10\\leqslant s\\leqslant 1, which can then be applied withs=φR​\(x\)s=\\varphi\_\{R\}\(x\)for eachxx\.in[norm\_weighted\_tensorDiff\_le](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/LocalizedTensorBounds.lean#L119)\. The Lean proof bounds∥\|φR​w\|2∥6/5⩽∥φR​w∥12/52\\lVert\|\\varphi\_\{R\}w\|^\{2\}\\rVert\_\{6/5\}\\leqslant\\lVert\\varphi\_\{R\}w\\rVert\_\{12/5\}^\{2\}, and then an interpolation inequality[cutoff\_interpolation\_twelve\_fifths](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/WeightedInterpolation.lean#L150-L161)is used to get

\(3\.8\)‖φR​w‖12/5⩽‖w‖23/4​‖φR4​w‖61/4⩽C​BR1/4\.\\\|\\varphi\_\{R\}w\\\|\_\{12/5\}\\leqslant\\\|w\\\|\_\{2\}^\{3/4\}\\\|\\varphi^\{4\}\_\{R\}w\\\|\_\{6\}^\{1/4\}\\leqslant CB\_\{R\}^\{1/4\}\.Secondly, to bound‖\|u\|​\|w\|‖6/5\\\|\|u\|\|w\|\\\|\_\{6/5\}, a simple application of Hölder in[cross\_norm\_bound](https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/R3/LocalizedTensorBounds.lean#L46)gives‖\|u\|​\|w\|‖6/5⩽‖u‖3​‖w‖2⩽C\\\|\|u\|\|w\|\\\|\_\{6/5\}\\leqslant\\\|u\\\|\_\{3\}\\\|w\\\|\_\{2\}\\leqslant C\. This argument is also distinct from the NL proof, as no12/512/5interpolation like the one present in \([3\.8](https://arxiv.org/html/2610.08144#S3.E8)\) is contained in the proof of Lemma 10\.5\.

### 3\.3\.Mistranslations and OpenAI’s announced Euler proof

Alongside its Navier\-Stokes announcement, OpenAI reported finite\-time blow\-up for the unforced incompressible Euler equations onℝ3\\mathbb\{R\}^\{3\}, starting from smooth, compactly supported initial data\. The Euler blow\-up and well posedness question has a long history, and we will – as in the Navier\-Stokes case – only mention a small subset of results here\[[5](https://arxiv.org/html/2610.08144#bib.bib5),[16](https://arxiv.org/html/2610.08144#bib.bib16),[34](https://arxiv.org/html/2610.08144#bib.bib34),[21](https://arxiv.org/html/2610.08144#bib.bib21),[12](https://arxiv.org/html/2610.08144#bib.bib12),[13](https://arxiv.org/html/2610.08144#bib.bib13),[2](https://arxiv.org/html/2610.08144#bib.bib2),[19](https://arxiv.org/html/2610.08144#bib.bib19),[17](https://arxiv.org/html/2610.08144#bib.bib17)\]\.

The format of the announced Euler paper is similar to the Navier\-Stokes\. There is a NL proof and an autoformalised Lean proof\. As in the Navier\-Stokes case, it is natural to ask whether this formalisation in Lean represents a semantically faithful translation of the NL paper, so that we can conclude that the NL paper represents a correct proof\. It is beyond the scope of this paper to carefully examine the autoformalisation of the Euler proof in a similar way to what we have done in this paper with the Navier\-Stokes case\. However, based on some examinations of the autoformalisation of the Euler case – with both AI and manual tools – we think that the Euler proof will be another great case study for mistranslations in practice\.

We encourage other readers to examine the autoformalisation of OpenAI’s Euler NL proof and determine if there are mistranslations\. Our prediction is based on preliminary examinations, but our assessment is that the likelihood of substantial mistranslations is very high\.

### 3\.4\.Why would mistranslations happen?

When success is judged solely by obtaining a Lean proof which successfully compiles, the procedure followed by the AI can be summarised as follows\.

> Input:A faithful Lean translationX′X^\{\\prime\}of an NL theoremXXand an alleged NL proofYYofXX\. whileno proof ofX′X^\{\\prime\}has been verifieddoThe AI revisesY′Y^\{\\prime\}usingYYas a guide \(that is, the AI attempts a ‘translation’ ofYYintoY′Y^\{\\prime\}\)The AI checks ifY′Y^\{\\prime\}is a valid Lean proof ofX′X^\{\\prime\}\.end whileOutput: the verified proofY′Y^\{\\prime\}\.

The acceptance criterion tests whetherY′Y^\{\\prime\}provesX′X^\{\\prime\}in Lean\. It does not check whether the reasoning inYYhas been preserved\. A revision may repair an error or replace a correct argument by another one, just as in the above examples\. Both count as success under this criterion, and neither establishes fidelity to the original purported proof\. In fact, since the above procedure accepts any valid Lean proof, if the original NL proof is indeed incorrect, the AI is incentivised to find a different proof\.

## 4\.Logic in AI: Why semantic preservation in AI autoformalisation is hard

For generations, logicians, mathematicians, linguists and philosophers have vigorously debated questions concerning natural and formal languages, semantics, and semantic preservation in translation\[[40](https://arxiv.org/html/2610.08144#bib.bib40),[27](https://arxiv.org/html/2610.08144#bib.bib27),[30](https://arxiv.org/html/2610.08144#bib.bib30),[8](https://arxiv.org/html/2610.08144#bib.bib8),[59](https://arxiv.org/html/2610.08144#bib.bib59),[38](https://arxiv.org/html/2610.08144#bib.bib38),[39](https://arxiv.org/html/2610.08144#bib.bib39),[43](https://arxiv.org/html/2610.08144#bib.bib43),[44](https://arxiv.org/html/2610.08144#bib.bib44),[56](https://arxiv.org/html/2610.08144#bib.bib56),[45](https://arxiv.org/html/2610.08144#bib.bib45),[60](https://arxiv.org/html/2610.08144#bib.bib60)\]\. For standard background on formal languages, interpretations and deductive systems, see\[[22](https://arxiv.org/html/2610.08144#bib.bib22), Chapters 1–2\]\. In autoformalisation semantic preservation becomes particularly delicate because of the need to resolve ambiguities, as we will see below\. Throughout, we useℕ=\{0,1,2,…\}\\mathbb\{N\}=\\\{0,1,2,\\ldots\\\}, as in Lean’sNat\.

### 4\.1\.Logic in autoformalisation: Resolving ambiguities is harder than the Halting problem

A crucial problem facing any AI autoformaliser is the task of resolving ambiguities\. Note that ambiguities may not always come from the fact that NLs produce ambiguous statements\. Indeed, as the following example demonstrates, ambiguities can come from the fact that well\-definedness of mathematical objects can depend on computational problems\. This fact indicates that the hardness of resolving such an ambiguity is induced by the hardness of solving certain computational problems\. Hence, results from foundations of mathematics & computation – such as the SCI hierarchy/arithmetical hierarchy – become important in order to understand the difficulty of resolving ambiguities\.

###### Example 4\.1\(A hidden existence presupposition causing ambiguities\)\.

An author of a textbook constructs explicitly a recursive enumeration \(that is, there exists a computer program that can list them\)\{pe\}e∈ℕ\\\{p\_\{e\}\\\}\_\{e\\in\\mathbb\{N\}\}of polynomials ink\+1k\+1variables with integer coefficients\. Later on, they write down a particular value ofee, and definenen\_\{e\}to be the least natural numbernnfor whichpe​\(n,x1,…,xk\)=0p\_\{e\}\(n,x\_\{1\},\\ldots,x\_\{k\}\)=0has no solution in natural numbersx1,…,xkx\_\{1\},\\ldots,x\_\{k\}\. They then define the real numberre=1/\(ne\+1\)r\_\{e\}=1/\(n\_\{e\}\+1\)and make the claim that it is obvious that\(re\+1\)2=re2\+2​re\+1\(r\_\{e\}\+1\)^\{2\}=r\_\{e\}^\{2\}\+2r\_\{e\}\+1\.

At first glance, this may seem like a trivial example to autoformalise\. Indeed, the conclusion that\(re\+1\)2=re2\+2​re\+1\(r\_\{e\}\+1\)^\{2\}=r\_\{e\}^\{2\}\+2r\_\{e\}\+1is elementary to establish in Lean\. The problem is the following: For Lean to prove that\(re\+1\)2=re2\+2​re\+1\(r\_\{e\}\+1\)^\{2\}=r\_\{e\}^\{2\}\+2r\_\{e\}\+1, thenrer\_\{e\}must be well\-defined as a rational number\. In particular, it must be established whether or not there exists annnsuch thatpe​\(n,x1,…,xk\)=0p\_\{e\}\(n,x\_\{1\},\\ldots,x\_\{k\}\)=0has no natural\-number solutionx1,…,xkx\_\{1\},\\ldots,x\_\{k\}\. This issue causes an ambiguity: can Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)be faithfully translated to Lean at all? The answer is as follows: yes, ifrer\_\{e\}is well defined, and no ifrer\_\{e\}is not well defined \(whennen\_\{e\}does not exist\)\. An AI autoformaliser aiming to translate Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)preserving the semantics is faced with the problem of resolving this ambiguity\. Ifrer\_\{e\}is not well\-defined, the AI autoformaliser should not attempt to translate in order to make Lean accept the translation\.

###### Example 4\.3\(A natural attempt to resolve Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)\)\.

It is natural to ask why one cannot simply apply the following algorithm, which may fail to halt and hence does not directly contradict the negative result concerning Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)above:

> Input:Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)ande∈ℕe\\in\\mathbb\{N\}\(recall thateeuniquely defines the claim in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)\)\. whileno translation of Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)has been verified by LeandoThe AI revises an attempted translationY′Y^\{\\prime\}of Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)into Lean\.The AI checks ifY′Y^\{\\prime\}is accepted by Lean\.end whileOutput: the accepted translationY′Y^\{\\prime\}\.

At face value, it seems like this methodology would only accept a translation whennen\_\{e\}is defined, and thus all choices ofeefor which the claim that\(re\+1\)2=re2\+2​re\+1\(r\_\{e\}\+1\)^\{2\}=r\_\{e\}^\{2\}\+2r\_\{e\}\+1in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)is a true unambiguous statement would ultimately be resolved\.

### 4\.2\.Why the algorithm in Example[4\.3](https://arxiv.org/html/2610.08144#S4.Thmtheorem3)cannot solve the problem

There is once again a problem with this approach\. The AI could easily produce an attempted translationY′Y^\{\\prime\}which uses a Lean definition that supplies a default value, whennen\_\{e\}does not exist, in its proof that\(re\+1\)2=re2\+2​re\+1\(r\_\{e\}\+1\)^\{2\}=r\_\{e\}^\{2\}\+2r\_\{e\}\+1\. In particular, for a fixede∈ℕe\\in\\mathbb\{N\}, write forn∈ℕn\\in\\mathbb\{N\}the predicateBe​\(n\)B\_\{e\}\(n\)as follows:

\(4\.1\)Be​\(n\)⟺∀\(x1,…,xk\)∈ℕk,pe​\(n,x1,…,xk\)≠0\.B\_\{e\}\(n\)\\;\\Longleftrightarrow\\;\\forall\\,\(x\_\{1\},\\ldots,x\_\{k\}\)\\in\\mathbb\{N\}^\{k\},\\quad p\_\{e\}\(n,x\_\{1\},\\ldots,x\_\{k\}\)\\neq 0\.With this predicate, a ‘translation’ of Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)in the case wherek=2k=2and

\(4\.2\)pe​\(n,x1,x2\)=x1\+x2−n,p\_\{e\}\(n,x\_\{1\},x\_\{2\}\)=x\_\{1\}\+x\_\{2\}\-n,to Lean code \(that compiles\) can be done in the following way, with similar examples possible for a different choice ofeeand thuspep\_\{e\}\. In particular, suppose an AI suggested the following ‘translation’Y′Y^\{\\prime\}of Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)into Lean:

defp\_e\(nx1x2:Int\):Int:=x1\+x2\-n

defB\_e\(n:Nat\):Prop:=

forall\(x1x2:Nat\),p\_e\(n:Int\)\(x1:Int\)\(x2:Int\)\!=0

noncomputabledefn\_e:Nat:=sInf\{n:Nat\|B\_en\}

noncomputabledefr\_e:Rat:=1/\(n\_e\+1\)

theoremexample\_3\_1:\(r\_e\+1\)^2=r\_e^2\+2\*r\_e\+1:=byring

HeresInfreturns the least element of a nonempty set of natural numbers, but returns00when the set is empty; seeNat\.sInf\_defandNat\.sInf\_emptyin\[[57](https://arxiv.org/html/2610.08144#bib.bib57)\]\. Thus, if no natural number satisfiesBeB\_\{e\}, the code silently assignsne=0n\_\{e\}=0andre=1r\_\{e\}=1\. However, for the polynomial in \([4\.2](https://arxiv.org/html/2610.08144#S4.E2)\), everyn∈ℕn\\in\\mathbb\{N\}admits the natural\-number root\(x1,x2\)=\(n,0\)\(x\_\{1\},x\_\{2\}\)=\(n,0\), sincepe​\(n,n,0\)=n\+0−n=0p\_\{e\}\(n,n,0\)=n\+0\-n=0\. Hence,Be​\(n\)B\_\{e\}\(n\)is false for everynn, and

\{n∈ℕ:Be​\(n\)\}=∅\.\\\{n\\in\\mathbb\{N\}:B\_\{e\}\(n\)\\\}=\\varnothing\.In particular,rer\_\{e\}is not well\-defined\. The ‘proof’ succeeds without resolving the ambiguity and the existence presupposition because it mistranslates the statement by usingsInf;

Warning:With the above ‘translation’Y′Y^\{\\prime\}\(in the grey box\) the algorithm in Example[4\.3](https://arxiv.org/html/2610.08144#S4.Thmtheorem3)will halt and produce a mistranslation\. In this case the semantics of the definition ofnen\_\{e\}have been completely changed\. Indeed, if the above ‘translation’ into Lean had actually been semantically faithful, it would have implied that there is ann∈ℕn\\in\\mathbb\{N\}such thatpe​\(n,x1,x2\)=x1\+x2−np\_\{e\}\(n,x\_\{1\},x\_\{2\}\)=x\_\{1\}\+x\_\{2\}\-nhas no roots\(x1,x2\)∈ℕ2\(x\_\{1\},x\_\{2\}\)\\in\\mathbb\{N\}^\{2\}– this is false\!

### 4\.3\.The root of the difficulty – Creating semantic preserving autoformalisers is a major open problem

All the problems discussed in the different examples above can be summarised in one rule of thumb, which illustrates the root of the problem:

> *Lean acceptance \(compilation\) of translation does not imply semantic preservation\.*

To illustrate the issue we consider the following example:

###### Example 4\.4\(Lean compilation does not imply semantic preservation\)\.

Consider the following two sentences:

- \(1\)*There are infinitely many odd numbers among the natural numbers\.*
- \(2\)*There are infinitely many prime numbers among the natural numbers\.*

Changing the word ‘odd’ to ‘prime’ changes the semantics of the first sentence completely, as it becomes the second sentence\. Suppose an AI should translate sentence \(1\) into Lean\. Suppose also that it did so semantically faithfully and Lean compiles\. What would have happened if the AI instead had made a mistake and changed ‘odd’ to ‘prime’, and then translated sentence \(2\) semantically faithfully to Lean – however, the intention was to translate sentence \(1\)? Lean would still compile, yet the ‘translation’ is actually a mistranslation\.

Example[4\.4](https://arxiv.org/html/2610.08144#S4.Thmtheorem4)reiterates the message in §[4\.2](https://arxiv.org/html/2610.08144#S4.SS2): There are many candidate ‘translations’ that would make Lean compile – some of them would be semantically faithful translations – but many would be mistranslations\. Thus, it will be up to the AI to choose a semantically faithful translation, Lean does not provide a security net if the AI provides a mistranslation\. This means that the AI is subject to the limitations arising from the foundations of mathematics and computations as highlighted in §[4\.1](https://arxiv.org/html/2610.08144#S4.SS1)and Theorem[A\.3](https://arxiv.org/html/2610.08144#A1.Thmtheorem3)\. Indeed, the AI autoformaliser cannot resolve all ambiguities and must therefore admit that there are many cases for which it will not know whether a translation is possible or not – even if a semantic translation is possible\.

How to design trustworthy AI autoformalisers – meaning that they will only provide semantically faithful translations – is beyond the scope of this paper\. Such developments will be announced in forthcoming articles\. The key observation, however, is that even the most advanced models of OpenAI are far from achieving this goal\. In particular, creating trustworthy AI autoformalisers that are capable of preserving semantics is a major open problem\.

## 5\.Summary and perspectives

### 5\.1\.Attempting semantics\-preserving autoformalisation in practice – The Meta attempt

Here is a pertinent example of the second type of autoformalisation – faithful semantic translation of a mathematical text – going awry in practice\. During the spring of 2026, Meta declared a new milestone in autoformalisation: they claimed to have translated 26 mathematics textbooks into Lean, forming a library with 45,000 verified Lean declarations and around 500,000 lines of Lean code\[[46](https://arxiv.org/html/2610.08144#bib.bib46)\]\. These claims were, however, swiftly refuted by the Lean community in the discussion quoted below\[[32](https://arxiv.org/html/2610.08144#bib.bib32)\]\.

- \(i\)Jack McCarthy: ‘Pg\. 17 of the paper claims that 56% of the target statements in this book \[i\.e\. one of the 26 books\] were formalized, but I could not find a single one which did not contain a fatal error like above\. The reality is that 0% of the statements here are accurately formalized\.’
- \(ii\)Brian Nugent: ‘I took a look at the algebraic geometry folder and it appears that the things it did prove \(about 60% of the book according to your website\) were exactly the things that are in Mathlib and it failed on everything else\. \[…\] claiming “my AI autoformalized this AG textbook” in the state that’s its in is simply lying\.’
- \(iii\)Christian Merten: ‘I would like to push back a bit on the point that this project has produced something useful on this front\.’

Fortunately, in this case, Lean experts were quickly able to detect the mistakes made by the AI in the autoformalisation\. This may not be the case in the future: proofs produced by autoformalisation are becoming longer and more complex\. For example, Anthropic’s recent autoformalisation of Fermat’s Last Theorem took 13 million lines of Lean code\[[10](https://arxiv.org/html/2610.08144#bib.bib10)\]\. The increases in both the number and length of autoformalised proofs will make it extremely difficult to catch mistranslations\.

The problem of mistranslations by autoformalisation is particularly relevant in the context of building a unified body of knowledge in Lean, where results are consistent with, and build upon, one another\. A single falsely translated statement in Mathlib means that all further results building upon this statement could be rendered invalid\. Ensuring autoformalisation is done correctly is therefore of utmost importance to ensuring Lean libraries such as Mathlib remain correct and usable\.

We may ask:*why did this autoformalisation project by Meta turn out the way it did?*The answer is that autoformalising AI systems currently follow something akin to the algorithm in Example[4\.3](https://arxiv.org/html/2610.08144#S4.Thmtheorem3)to produce translations\. The project did go beyond this, checking for faithfulness and non\-cheating in the translations; this semantic verification was, however, mainly performed by other AIs\[[46](https://arxiv.org/html/2610.08144#bib.bib46), Section 3 and Appendix D\]\. The fact that this failed highlights the difficulty that AIs have both with producing semantically faithful translations into Lean and with assessing the accuracy of such translations\.

### 5\.2\.Semantics\-preserving autoformalisation and the future of AI in mathematics

The Leiden Declaration from June 2026\[[1](https://arxiv.org/html/2610.08144#bib.bib1)\]discusses how incorrect use of AI can be harmful to mathematics as a discipline\. It singles out in particular the dangers posed by autoformalisation:

> ‘Current automated techniques can produce plausible but unreliable \(or even incorrect\) arguments which are difficult to distinguish from correct mathematical proofs\.This applies not only to informal arguments, but also to formalizations, where the difficulty lies in the translation between computer\-encoded and human presentations of concepts\.’

The boldface text refers exactly to the issues with the two forms of autoformalisation as discussed in this note\. Even more recently, in September 2026, a declaration titled ‘A Severe Misalignment of AI in Mathematics’\[[3](https://arxiv.org/html/2610.08144#bib.bib3)\]initiated by 25 Fields medalists brings up other issues related to AI in mathematics:

> ‘But solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight\. Forgetting this in the world of AI may turn the tool against the primary goal\. Indeed, the mass production at faster and faster pace of “true/false” statements could destroy fertile ground instead of breathing life into new ideas\.’

The quote also relates fundamentally to autoformalisation:

- \(i\)Solving a problem only formally in Lean – without a semantically faithful translation from a correct NL argument that humans can read – would typically only be a proxy for the optimal final product which should provide understanding of the argument \(both an NL argument and a Lean proof with a semantically faithful translation between the two\)\. Without the semantically faithful translation, the NL argument could even be wrong – which is detrimental to human understanding – but would also harm future instalments of AI which rely on massive collections of correct mathematical NL literature in the training process\.
- \(ii\)Pure ‘true/false’ statements coming from only Lean proofs \(lacking a semantically faithful translation from a correct NL argument\) can certainly be useful\. Indeed, we would like to know if the Riemann Hypothesis is true\. However, a principal reason for the interest in this problem stems from the belief that the techniques and ideas used in a proof could be applied broadly to address other questions and to enhance our understanding across analysis, number theory and the many other fields that the Riemann Hypothesis touches on\. A correct but incomprehensible Lean proof would not have the same value – mathematicians will unlikely read millions of lines of Lean code to try to understand\. It would be even worse if an incorrect NL proof of the Riemann Hypothesis is accepted based on a mistranslated Lean proof; we would then have a complete misunderstanding of the facets of this problem\.

As argued above, AI autoformalisers that can guarantee semantically faithful translations do not currently exist\. Thus, developing semantically faithful AI autoformalisation stands as a major open problem, and attempts at quick fixes will typically violate fundamental limitations that date back to Gödel and Turing\.

## Appendix AThe difficulty of resolving ambiguities and Hilbert’s 10th problem

### A\.1\.Help from the SCI hierarchy and Hilbert’s 10th problem

Here we continue the presupposition resolution discussion from Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1), explaining why no AI can resolve it for alle∈ℕe\\in\\mathbb\{N\}\. The basic framework we use is that of the Solvability Complexity Index \(SCI\) hierarchy initiated in\[[28](https://arxiv.org/html/2610.08144#bib.bib28)\]and further developed in\[[7](https://arxiv.org/html/2610.08144#bib.bib7),[6](https://arxiv.org/html/2610.08144#bib.bib6),[15](https://arxiv.org/html/2610.08144#bib.bib15),[25](https://arxiv.org/html/2610.08144#bib.bib25),[14](https://arxiv.org/html/2610.08144#bib.bib14),[4](https://arxiv.org/html/2610.08144#bib.bib4)\]\. The SCI hierarchy is closely connected to S\. Smale’s\[[49](https://arxiv.org/html/2610.08144#bib.bib49),[50](https://arxiv.org/html/2610.08144#bib.bib50)\]program on the foundations of computational mathematics and scientific computing\. This program motivated the early investigations of polynomial root\-finding by C\. McMullen\[[36](https://arxiv.org/html/2610.08144#bib.bib36),[37](https://arxiv.org/html/2610.08144#bib.bib37),[51](https://arxiv.org/html/2610.08144#bib.bib51)\]and P\. Doyle & C\. McMullen\[[20](https://arxiv.org/html/2610.08144#bib.bib20)\]\. Their work yielded pioneering classification results within the SCI hierarchy, predating its formal introduction\. See also the classification results in the SCI hierarchy by S\. Weinberger\[[61](https://arxiv.org/html/2610.08144#bib.bib61)\]\. Although some of the mathematics underlying the SCI hierarchy can be traced back to K\. Gödel\[[26](https://arxiv.org/html/2610.08144#bib.bib26)\]and A\. Turing\[[58](https://arxiv.org/html/2610.08144#bib.bib58)\], the newly developed techniques apply to any model of computation\.

#### A\.1\.1\.An informal introduction to the SCI hierarchy

Here we informally introduce the general SCI hierarchy \(see\[[6](https://arxiv.org/html/2610.08144#bib.bib6),[14](https://arxiv.org/html/2610.08144#bib.bib14)\]for the formal definitions\)\. The SCI hierarchy is designed to accommodate all types of computational problems and categorises the difficulty of computational problems according to the number of limits required to solve them\. A computational problem is given by: a set of inputsΩ\\Omega\(where each element ofΩ\\Omegaspecifies a problem instance\), a metric space\(ℳ,d\)\(\\mathcal\{M\},d\)of candidate solutions, and a solution mapΞ:Ω⇉ℳ\\Xi:\\Omega\\rightrightarrows\\mathcal\{M\}that takes each problem instance to its solution\(s\) \(the double arrow indicates that the solution could be multi\-valued\)\. There is in general also an evaluation setΛ\\Lambdaspecifying which information about the problem instances may actually be accessed by an algorithm\. This will not be relevant131313For the computational problems discussed in this appendix, each problem instance inΩ\\Omegais specified entirely by a single natural number, soΛ\\Lambdaamounts to containing only an identity map\.for this appendix\. A computational problem is often specified simply as\{Ξ,Ω\}\\\{\\Xi,\\Omega\\\}, whenℳ\\mathcal\{M\}andΛ\\Lambdaare understood\.

*The SCI of a computational problem is defined as the minimal number of limits141414This is formalised by the notion of towers of algorithms\.required to solve that problem \(\+∞\+\\inftyif no finite number of limits suffices\)*\. The mainstay classes of the hierarchy are theΔmα\\Delta\_\{m\}^\{\\alpha\}classes, which are defined for eachm⩾0m\\geqslant 0\. Hereα\\alphais related to the model of computation, as explained below\. Informally, we have the following description\. Given a collection𝒞\\mathcal\{C\}of computational problems:

- \(i\)Δ0α\\Delta^\{\\alpha\}\_\{0\}is the set of problems that can be computed in finite time, so that they satisfy SCI=0=0;
- \(ii\)Δ1α\\Delta^\{\\alpha\}\_\{1\}is the set of problems that can be computed using one limit \(they satisfy SCI⩽1\\leqslant 1\) with control of the error, i\.e\., there is a sequence of algorithms\{Γn\}\\\{\\Gamma\_\{n\}\\\}withd⁡\(Γn​\(A\),Ξ⁡\(A\)\)⩽2−n,∀A∈Ωd\(\\Gamma\_\{n\}\(A\),\\Xi\(A\)\)\\leqslant 2^\{\-n\},\\,\\forall A\\in\\Omega;
- \(iii\)Δ2α\\Delta^\{\\alpha\}\_\{2\}is the set of problems that can be computed using one limit \(again SCI⩽1\\leqslant 1\) but sans error control, i\.e\., there is a sequence of algorithms\{Γn\}\\\{\\Gamma\_\{n\}\\\}withlimn→∞Γn​\(A\)=Ξ⁡\(A\),∀A∈Ω\\lim\_\{n\\rightarrow\\infty\}\\Gamma\_\{n\}\(A\)=\\Xi\(A\),\\,\\forall A\\in\\Omega;
- \(iv\)Δm\+1α\\Delta^\{\\alpha\}\_\{m\+1\}, form⩾1m\\geqslant 1, is the set of problems that can be computed by usingmmlimits, \(in other words, SCI⩽m\\leqslant m\), i\.e\., there is a family of algorithms\{Γnm,…,n1\}\\\{\\Gamma\_\{n\_\{m\},\\ldots,n\_\{1\}\}\\\}with limnm→∞…​limn1→∞Γnm,…,n1​\(A\)=Ξ⁡\(A\),∀A∈Ω\.\\lim\_\{n\_\{m\}\\rightarrow\\infty\}\\ldots\\lim\_\{n\_\{1\}\\rightarrow\\infty\}\\Gamma\_\{n\_\{m\},\\ldots,n\_\{1\}\}\(A\)=\\Xi\(A\),\\,\\forall A\\in\\Omega\.

In general, this hierarchy can only be refined further, beyond these classes, if the metric spaceℳ\\mathcal\{M\}admits additional structure, such as being totally ordered\. On the other hand, the hierarchy typically does not collapse, so that we have:

\(A\.1\)Δ0α⊊Δ1α⊊Δ2α⊊…⊊Δmα⊊…\.\\Delta\_\{0\}^\{\\alpha\}\\subsetneq\\Delta\_\{1\}^\{\\alpha\}\\subsetneq\\Delta\_\{2\}^\{\\alpha\}\\subsetneq\\ldots\\subsetneq\\Delta^\{\\alpha\}\_\{m\}\\subsetneq\\ldots\.Depending on the collection𝒞\\mathcal\{C\}of computational problems, however, the hierarchy \([A\.1](https://arxiv.org/html/2610.08144#A1.E1)\) may terminate for a finitemmor continue for arbitrary largemm\.

###### Definition A\.1\(The SCI Hierarchy \(totally ordered set\)\)\.

Given the setup above, suppose in addition thatℳ\\mathcal\{M\}is a totally ordered set\. Define

Σ0α=Π0α=Δ0α,Σ1α=\{\{Ξ,Ω\}∈Δ2α\|∃a sequence of algorithms​\{Γn\}​s\.t\.​Γn​\(A\)↗Ξ⁡\(A\)​∀A∈Ω\},Π1α=\{\{Ξ,Ω\}∈Δ2α\|∃a sequence of algorithms​\{Γn\}​s\.t\.​Γn​\(A\)↘Ξ⁡\(A\)​∀A∈Ω\},\\begin\{split\}\\Sigma^\{\\alpha\}\_\{0\}&=\\Pi^\{\\alpha\}\_\{0\}=\\Delta^\{\\alpha\}\_\{0\},\\\\ \\Sigma^\{\\alpha\}\_\{1\}&=\\\{\\\{\\Xi,\\Omega\\\}\\in\\Delta\_\{2\}^\{\\alpha\}\\ \|\\ \\exists\\ \\textrm\{ a sequence of algorithms \}\\\{\\Gamma\_\{n\}\\\}\\text\{ s\.t\. \}\\Gamma\_\{n\}\(A\)\\nearrow\\Xi\(A\)\\ \\,\\forall A\\in\\Omega\\\},\\\\ \\Pi^\{\\alpha\}\_\{1\}&=\\\{\\\{\\Xi,\\Omega\\\}\\in\\Delta\_\{2\}^\{\\alpha\}\\ \|\\ \\exists\\ \\textrm\{ a sequence of algorithms \}\\\{\\Gamma\_\{n\}\\\}\\text\{ s\.t\. \}\\Gamma\_\{n\}\(A\)\\searrow\\Xi\(A\)\\ \\,\\forall A\\in\\Omega\\\},\\end\{split\}where↗\\nearrowand↘\\searrowdenotes convergence from below and above respectively, as well as, form∈ℕm\\in\\mathbb\{N\},

Σm\+1α=\{\{Ξ,Ω\}∈Δm\+2α\|∃height​m\+1​tower​\{Γnm\+1,…,n1\}​for​\{Ξ,Ω\}​s\.t\.​Γnm\+1​\(A\)↗Ξ⁡\(A\)​∀A∈Ω\},Πm\+1α=\{\{Ξ,Ω\}∈Δm\+2α\|∃height​m\+1​tower​\{Γnm\+1,…,n1\}​for​\{Ξ,Ω\}​s\.t\.​Γnm\+1​\(A\)↘Ξ⁡\(A\)​∀A∈Ω\}\.\\begin\{split\}\\Sigma^\{\\alpha\}\_\{m\+1\}&=\\\{\\\{\\Xi,\\Omega\\\}\\in\\Delta\_\{m\+2\}^\{\\alpha\}\\ \|\\ \\exists\\ \\textrm\{ height \}m\+1\\textrm\{ tower \}\\\{\\Gamma\_\{n\_\{m\+1\},\\ldots,n\_\{1\}\}\\\}\\textrm\{ for \}\\\{\\Xi,\\Omega\\\}\\text\{ s\.t\. \}\\Gamma\_\{n\_\{m\+1\}\}\(A\)\\nearrow\\Xi\(A\)\\ \\,\\forall A\\in\\Omega\\\},\\\\ \\Pi^\{\\alpha\}\_\{m\+1\}&=\\\{\\\{\\Xi,\\Omega\\\}\\in\\Delta\_\{m\+2\}^\{\\alpha\}\\ \|\\ \\exists\\ \\textrm\{ height \}m\+1\\textrm\{ tower \}\\\{\\Gamma\_\{n\_\{m\+1\},\\ldots,n\_\{1\}\}\\\}\\textrm\{ for \}\\\{\\Xi,\\Omega\\\}\\text\{ s\.t\. \}\\Gamma\_\{n\_\{m\+1\}\}\(A\)\\searrow\\Xi\(A\)\\ \\,\\forall A\\in\\Omega\\\}\.\\end\{split\}

See\[[6](https://arxiv.org/html/2610.08144#bib.bib6)\]for the formal definition of the towers of algorithms used to defineΣm\+1α\\Sigma\_\{m\+1\}^\{\\alpha\}andΠm\+1α\\Pi\_\{m\+1\}^\{\\alpha\}above\. A specific case of the definitions of such towers, when the algorithms are Turing machines, is elaborated upon below\. The above definitions apply in particular to the totally ordered metric spaceℳ=\{0,1\}\\mathcal\{M\}=\\\{0,1\\\}; this yields the SCI hierarchy for arbitrary decision problems\. Schematically, the general SCI hierarchy can be viewed in the following way:

\(A\.2\)Π0α\{\\lx@inpgf@ignorespaces\\Pi\_\{0\}^\{\\alpha\}\}Π1α\{\\lx@inpgf@ignorespaces\\Pi\_\{1\}^\{\\alpha\}\}Π2α\{\\lx@inpgf@ignorespaces\\Pi\_\{2\}^\{\\alpha\}\}Δ0α\{\\lx@inpgf@ignorespaces\\Delta\_\{0\}^\{\\alpha\}\}Δ1α\{\\lx@inpgf@ignorespaces\\Delta\_\{1\}^\{\\alpha\}\}Σ1α∪Π1α\{\\lx@inpgf@ignorespaces\\Sigma\_\{1\}^\{\\alpha\}\\cup\\Pi\_\{1\}^\{\\alpha\}\}Δ2α\{\\lx@inpgf@ignorespaces\\Delta\_\{2\}^\{\\alpha\}\}Σ2α∪Π2α\{\\lx@inpgf@ignorespaces\\Sigma\_\{2\}^\{\\alpha\}\\cup\\Pi\_\{2\}^\{\\alpha\}\}Δ3α\{\\lx@inpgf@ignorespaces\\Delta\_\{3\}^\{\\alpha\}\}⋯\{\\lx@inpgf@ignorespaces\\cdots\}Σ0α\{\\lx@inpgf@ignorespaces\\Sigma\_\{0\}^\{\\alpha\}\}Σ1α\{\\lx@inpgf@ignorespaces\\Sigma\_\{1\}^\{\\alpha\}\}Σ2α\{\\lx@inpgf@ignorespaces\\Sigma\_\{2\}^\{\\alpha\}\}====⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneq⊊\\subsetneqNote that theΣ1α\\Sigma\_\{1\}^\{\\alpha\}andΠ1α\\Pi\_\{1\}^\{\\alpha\}classes are crucial as they guarantee the existence of algorithms that will never make mistakes\. They thus become crucial in computer\-assisted proofs, see\[[6](https://arxiv.org/html/2610.08144#bib.bib6), Section 3\]\.

We also use standard facts about the arithmetical hierarchy and oracle computability, for which we refer the reader to\[[52](https://arxiv.org/html/2610.08144#bib.bib52), Chapter 4\]\. Theα\\alphain theΔmα\\Delta\_\{m\}^\{\\alpha\}classes can refer to any model of computation \(e\.g\. the classical Turing model\[[58](https://arxiv.org/html/2610.08144#bib.bib58)\]or the Blum\-Shub\-Smale model\[[9](https://arxiv.org/html/2610.08144#bib.bib9)\]\)\. Hereon, we will takeα=A\\alpha=AwhereAArefers to the arithmetic model of computation\. This means the algorithms are all Turing machines i\.e\. the classical Turing model\.

###### Notation\(Reducibility\)\.

For setsA,B⊆ℕA,B\\subseteq\\mathbb\{N\}, we writeA⩽mBA\\leqslant\_\{m\}Bif there is a total computable functionf:ℕ→ℕf:\\mathbb\{N\}\\to\\mathbb\{N\}such that

\(∀n∈ℕ\)\[n∈A⇔f\(n\)∈B\]\.\(\\forall n\\in\\mathbb\{N\}\)\[n\\in A\\iff f\(n\)\\in B\]\.In this case we sayAAis many\-one reducible toBB, witnessed byff\. We writeA⩽TBA\\leqslant\_\{T\}Bif there is an oracle Turing machine which, withBBon the oracle tape, computes the characteristic function ofAA\. In this case we sayAAis Turing reducible toBB\. The Turing degree of a setA⊆ℕA\\subseteq\\mathbb\{N\}is the set of allC⊆ℕC\\subseteq\\mathbb\{N\}that simultaneously satisfyA⩽TCA\\leqslant\_\{T\}CandC⩽TAC\\leqslant\_\{T\}A\. We sayAAisΣn0\\Sigma\_\{n\}^\{0\}\-complete ifA∈Σn0A\\in\\Sigma\_\{n\}^\{0\}and alsoC⩽mAC\\leqslant\_\{m\}Afor everyC∈Σn0C\\in\\Sigma\_\{n\}^\{0\}\. Similarly,AAisΠn0\\Pi\_\{n\}^\{0\}\-complete ifA∈Πn0A\\in\\Pi\_\{n\}^\{0\}andC⩽mAC\\leqslant\_\{m\}Afor everyC∈Πn0C\\in\\Pi\_\{n\}^\{0\}\. We fix an integer\-coefficient polynomial pairing function⟨,⟩:ℕ2→ℕ\\langle\\textrm\{ \},\\textrm\{ \}\\rangle:\\mathbb\{N\}^\{2\}\\to\\mathbb\{N\}given by

⟨x,y⟩=\(x\+y\)​\(x\+y\+1\)\+2​y,for​\(x,y\)∈ℕ2,\\langle x,y\\rangle=\(x\+y\)\(x\+y\+1\)\+2y,\\textrm\{ for \}\(x,y\)\\in\\mathbb\{N\}^\{2\},which is a computable injection, by\[[41](https://arxiv.org/html/2610.08144#bib.bib41), Section 1, p\. 1001\]\. By iteration, for eachn⩾2n\\geqslant 2we also obtain and hereon fix annn\-ary pairing function⟨,…,⟩:ℕn→ℕ\\langle\\textrm\{ \},\.\.\.,\\textrm\{ \}\\rangle:\\mathbb\{N\}^\{n\}\\to\\mathbb\{N\}, which is also an integer\-coefficient polynomial\.

### A\.2\.Resolving ambiguities is hard

Recall the condition definingnen\_\{e\}in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)\. For an enumeration\(pe\)e∈ℕ\(p\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}of integer\-coefficient polynomials in the variablesn,x1,…,xkn,x\_\{1\},\\ldots,x\_\{k\}, write

\(A\.3\)Be\(n\)⇔\(∀\(x1,…,xk\)∈ℕk\)pe\(n,x1,…,xk\)≠0\.B\_\{e\}\(n\)\\iff\(\\forall\(x\_\{1\},\\ldots,x\_\{k\}\)\\in\\mathbb\{N\}^\{k\}\)\\textrm\{ \}p\_\{e\}\(n,x\_\{1\},\\ldots,x\_\{k\}\)\\neq 0\.Thennen\_\{e\}is defined to be the leastn∈ℕn\\in\\mathbb\{N\}for whichBe​\(n\)B\_\{e\}\(n\)holds, provided such annnexists, and is undefined otherwise\. Completeness throughout this subsection refers to completeness under many\-one reductions\.

###### Theorem A\.3\.

Fixk⩾9k\\geqslant 9\. For any computable enumeration\(pe\)e∈ℕ\(p\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}of all polynomials with integer coefficients ink\+1k\+1variables, letBeB\_\{e\}be as in \([A\.3](https://arxiv.org/html/2610.08144#A1.E3)\)\. Then the set

d:=\{e∈ℕ:\(∃n∈ℕ\)Be\(n\)\}d:=\\\{e\\in\\mathbb\{N\}:\(\\exists n\\in\\mathbb\{N\}\)\\textrm\{ \}B\_\{e\}\(n\)\\\}isΣ20\\Sigma^\{0\}\_\{2\}\-complete\. In particular, no AI can always determine whether the numbernen\_\{e\}specified in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)is well\-defined, even with an oracle for the Halting problem\.

###### Proof\.

We use the usualμ\\munotation for minimum search\[[52](https://arxiv.org/html/2610.08144#bib.bib52)\]\. By the assumption that the enumeratione↦pee\\mapsto p\_\{e\}is computable and the assumption thatpep\_\{e\}has integer coefficients, there exists an algorithm that decides ifpe​\(n,x1,…​xk\)=0p\_\{e\}\(n,x\_\{1\},\\ldots x\_\{k\}\)=0given inputsn,x1,…,xkn,x\_\{1\},\\dotsc,x\_\{k\}\. The condition defining membership inddis thus given by the quantifiers\(∃n∈ℕ\)​\(∀x1∈ℕ\)​…​\(∀xk∈ℕ\)\(\\exists n\\in\\mathbb\{N\}\)\(\\forall x\_\{1\}\\in\\mathbb\{N\}\)\.\.\.\(\\forall x\_\{k\}\\in\\mathbb\{N\}\)over a decidable relation, so we haved∈Σ20d\\in\\Sigma^\{0\}\_\{2\}\.

To obtainΣ20\\Sigma^\{0\}\_\{2\}\-completeness, fix a standard effective enumeration\(Pe\)e∈ℕ\(P\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}of all Turing machines\. Fore,n∈ℕe,n\\in\\mathbb\{N\}, writePe​\(n\)↓P\_\{e\}\(n\)\\downarrowwhenPe​\(n\)P\_\{e\}\(n\)halts andPe​\(n\)↑P\_\{e\}\(n\)\\uparrowwhenPe​\(n\)P\_\{e\}\(n\)does not halt\. Recall that a Diophantine set\[[35](https://arxiv.org/html/2610.08144#bib.bib35)\]is a setA⊆ℕA\\subseteq\\mathbb\{N\}that can be represented using a finite number of unknowns, in the sense that there exists an integers⩾1s\\geqslant 1and an integer\-coefficient polynomialp⁡\(n,x1,…,xs\)p\(n,x\_\{1\},\.\.\.,x\_\{s\}\)ins\+1s\+1variables with:

n∈A⇔\(∃\(x1,…,xs\)∈ℕs\)p\(n,x1,…,xs\)=0\.n\\in A\\iff\(\\exists\(x\_\{1\},\\ldots,x\_\{s\}\)\\in\\mathbb\{N\}^\{s\}\)\\textrm\{ \}p\(n,x\_\{1\},\\ldots,x\_\{s\}\)=0\.The Davis–Putnam–Robinson–Matiyasevich \(DPRM\) theorem\[[35](https://arxiv.org/html/2610.08144#bib.bib35)\]states that the Diophantine sets are precisely the computably enumerable sets\. The nine\-unknown refinement\[[31](https://arxiv.org/html/2610.08144#bib.bib31)\]of the DPRM theorem permits every computably enumerable relation overℕ\\mathbb\{N\}to be represented using nine unknowns\. Applying this to the computably enumerable setK1=\{⟨e,n⟩∈ℕ:Pe​\(n\)↓\}K\_\{1\}=\\\{\\langle e,n\\rangle\\in\\mathbb\{N\}:P\_\{e\}\(n\)\\downarrow\\\}, we find there exists a fixed integer\-coefficient polynomialq0​\(n~,x1,…,x9\)q\_\{0\}\(\\tilde\{n\},x\_\{1\},\.\.\.,x\_\{9\}\), wheren~\\tilde\{n\}is a variable, such that⟨e,n⟩∈K1\\langle e,n\\rangle\\in K\_\{1\}if and only ifq0​\(⟨e,n⟩,x1,…,x9\)q\_\{0\}\(\\langle e,n\\rangle,x\_\{1\},\.\.\.,x\_\{9\}\)admits a root\(x1,…,x9\)∈ℕ9\(x\_\{1\},\.\.\.,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\. Defining the polynomialq⁡\(e,n,x1,…,x9\):=q0​\(⟨e,n⟩,x1,…,x9\)q\(e,n,x\_\{1\},\.\.\.,x\_\{9\}\):=q\_\{0\}\(\\langle e,n\\rangle,x\_\{1\},\.\.\.,x\_\{9\}\), we have for eache,n∈ℕe,n\\in\\mathbb\{N\}:

Pe\(n\)↓⟺\(∃\(x1,…,x9\)∈ℕ9\)q\(e,n,x1,…,x9\)=0\.P\_\{e\}\(n\)\\downarrow\\quad\\Longleftrightarrow\\quad\(\\exists\(x\_\{1\},\\ldots,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\)\\textrm\{ \}q\(e,n,x\_\{1\},\\ldots,x\_\{9\}\)=0\.Fork\>9k\>9, regardqqas independent of the additional variablesx10,…,xkx\_\{10\},\\ldots,x\_\{k\}\. Define the binary predicateW⊆ℕ2W\\subseteq\\mathbb\{N\}^\{2\}by

W⁡\(e,j\)⇔pj​\(n,x1,…,xk\)≡q⁡\(e,n,x1,…,xk\),W\(e,j\)\\iff p\_\{j\}\(n,x\_\{1\},\.\.\.,x\_\{k\}\)\\equiv q\(e,n,x\_\{1\},\.\.\.,x\_\{k\}\),where≡\\equivdenotes that the two polynomials, whose variables aren,x1,…,xkn,x\_\{1\},\.\.\.,x\_\{k\}, have coinciding coefficients; giveneeandjjthis is decidable\. Since\(pe\)e∈ℕ\(p\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}enumerates all integer\-coefficient polynomials ink\+1k\+1variables, the functiont⁡\(e\):=μ​j​\[W⁡\(e,j\)\]t\(e\):=\\mu j\[W\(e,j\)\]is well\-defined and computable\. By the definitions ofddandqq, we have

t\(e\)∈d⟺\(∃n∈ℕ\)Pe\(n\)↑t\(e\)\\in d\\quad\\Longleftrightarrow\\quad\(\\exists n\\in\\mathbb\{N\}\)\\textrm\{ \}P\_\{e\}\(n\)\\uparrowIn other words,ttis a computable many\-one reduction from

NTOT:=\{e∈ℕ:\(∃n∈ℕ\)Pe\(n\)↑\}\\mathrm\{NTOT\}:=\\\{e\\in\\mathbb\{N\}:\(\\exists n\\in\\mathbb\{N\}\)\\textrm\{ \}P\_\{e\}\(n\)\\uparrow\\\}todd\. SinceNTOT\\mathrm\{NTOT\}isΣ20\\Sigma^\{0\}\_\{2\}\-complete, so isdd\. By Post’s theorem\[[52](https://arxiv.org/html/2610.08144#bib.bib52), Chapter 4\], we haved⩽T∅′⇔d∈Δ20d\\leqslant\_\{T\}\\emptyset^\{\\prime\}\\iff d\\in\\Delta\_\{2\}^\{0\}\. Sinced∈Σ20d\\in\\Sigma\_\{2\}^\{0\}, we haved⩽T∅′⇔d∈Π20d\\leqslant\_\{T\}\\emptyset^\{\\prime\}\\iff d\\in\\Pi\_\{2\}^\{0\}\. But whenever a set belongs toΠ20\\Pi\_\{2\}^\{0\}so too does any set that \(many\-one\) reduces to it; thus ifd∈Π20d\\in\\Pi\_\{2\}^\{0\}then byΣ20\\Sigma\_\{2\}^\{0\}\-completeness we would haveΣ20⊆Π20\\Sigma\_\{2\}^\{0\}\\subseteq\\Pi\_\{2\}^\{0\}, contradicting strictness of the arithmetical hierarchy\[[52](https://arxiv.org/html/2610.08144#bib.bib52), Corollary 4\.2\.3, p\. 85\]\. Consequently, we cannot haved⩽T∅′d\\leqslant\_\{T\}\\emptyset^\{\\prime\}\. Sinceddis exactly the set ofeefor whichnen\_\{e\}in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)is well\-defined, the final claim follows\. ∎

The preceding result can be extended to arbitrarily high levels in the SCI hierarchy whilst simultaneously retaining polynomial predicates and the least\-number construction of Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)\. We first generalise the predicateBe​\(n\)B\_\{e\}\(n\)\. Forl⩾2l\\geqslant 2, consider an enumeration\(pe\)e∈ℕ\(p\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}of integer\-coefficient polynomials in thel−1\+kl\-1\+kvariables

n,z2,…,zl−1,x1,…,xk\.n,z\_\{2\},\\ldots,z\_\{l\-1\},x\_\{1\},\\ldots,x\_\{k\}\.LetQjQ\_\{j\}denote∃\\existsfor oddjjand∀\\forallfor evenjj\. We omitz2,…,zl−1z\_\{2\},\\ldots,z\_\{l\-1\}whenl=2l=2\. DefineBe\(l\)​\(n\)B^\{\(l\)\}\_\{e\}\(n\)by the following two cases\.

For evenll, again omittingz2,…​zl−1z\_\{2\},\\ldots z\_\{l\-1\}whenl=2l=2, we have\(A\.4a\)Be\(l\)​\(n\)⇔\\displaystyle B^\{\(l\)\}\_\{e\}\(n\)\\iff\(Q2z2∈ℕ\)⋯\(Ql−1zl−1∈ℕ\)\(∀\(x1,…,xk\)∈ℕk\)\\displaystyle\(Q\_\{2\}z\_\{2\}\\in\\mathbb\{N\}\)\\;\\cdots\\;\(Q\_\{l\-1\}z\_\{l\-1\}\\in\\mathbb\{N\}\)\\;\(\\forall\(x\_\{1\},\\ldots,x\_\{k\}\)\\in\\mathbb\{N\}^\{k\}\)pe​\(n,z2,…,zl−1,x1,…,xk\)≠0,\\displaystyle p\_\{e\}\(n,z\_\{2\},\\ldots,z\_\{l\-1\},x\_\{1\},\\ldots,x\_\{k\}\)\\neq 0,For oddl⩾3l\\geqslant 3,\(A\.4b\)Be\(l\)​\(n\)⇔\\displaystyle B^\{\(l\)\}\_\{e\}\(n\)\\iff\(Q2z2∈ℕ\)⋯\(Ql−1zl−1∈ℕ\)\(∃\(x1,…,xk\)∈ℕk\)\\displaystyle\(Q\_\{2\}z\_\{2\}\\in\\mathbb\{N\}\)\\;\\cdots\\;\(Q\_\{l\-1\}z\_\{l\-1\}\\in\\mathbb\{N\}\)\\;\(\\exists\(x\_\{1\},\\ldots,x\_\{k\}\)\\in\\mathbb\{N\}^\{k\}\)pe​\(n,z2,…,zl−1,x1,…,xk\)=0\.\\displaystyle p\_\{e\}\(n,z\_\{2\},\\ldots,z\_\{l\-1\},x\_\{1\},\\ldots,x\_\{k\}\)=0\.Note that \(using the samekkand polynomial enumeration\)Be\(2\)​\(n\)B^\{\(2\)\}\_\{e\}\(n\)isBe​\(n\)B\_\{e\}\(n\)\. As in\[[52](https://arxiv.org/html/2610.08144#bib.bib52)\], we write∅\(0\)=∅\\emptyset^\{\(0\)\}=\\emptysetand∅\(j\+1\)\\emptyset^\{\(j\+1\)\}for the Halting problem relative to∅\(j\)\\emptyset^\{\(j\)\}, forj∈ℕj\\in\\mathbb\{N\}\.

###### Theorem A\.4\(Presupposition resolution at arbitrary arithmetical levels\)\.

Fixl⩾2l\\geqslant 2andk⩾9k\\geqslant 9\. Fix a computable enumeration\(pe\)e∈ℕ\(p\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}of all integer\-coefficient polynomials inl−1\+kl\-1\+kvariables, and letBe\(l\)B^\{\(l\)\}\_\{e\}be as in \([A\.4](https://arxiv.org/html/2610.08144#A1.E4)\)\. Then

dl:=\{e∈ℕ:\(∃n∈ℕ\)Be\(l\)\(n\)\}d\_\{l\}:=\\\{e\\in\\mathbb\{N\}:\(\\exists n\\in\\mathbb\{N\}\)\\textrm\{ \}B^\{\(l\)\}\_\{e\}\(n\)\\\}isΣl0\\Sigma\_\{l\}^\{0\}\-complete\. In particular, no algorithm can always determine whether the leastnnfor whichBe\(l\)​\(n\)B^\{\(l\)\}\_\{e\}\(n\)holds is well\-defined, even with an oracle for∅\(l−1\)\\emptyset^\{\(l\-1\)\}\.

###### Proof\.

Fixl⩾2l\\geqslant 2\. By its definition,Be\(l\)​\(n\)B^\{\(l\)\}\_\{e\}\(n\)is aΠl−10\\Pi^\{0\}\_\{l\-1\}predicate\. Indeed, it begins withl−2l\-2alternating quantifiers \- the first being a universal quantifier – and the subsequentkkquantifiers are all either existential or all universal; the affected predicate therein, namelype​\(n,z2,…,zl−1,x1,…,xk\)=0p\_\{e\}\(n,z\_\{2\},\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{k\}\)=0, is decidable because the polynomial enumeration is computable and the computation is over the integers\. That is,dl∈Σl0d\_\{l\}\\in\\Sigma\_\{l\}^\{0\}\. ForΣl0\\Sigma\_\{l\}^\{0\}\-hardness, letA⊆ℕA\\subseteq\\mathbb\{N\}be anyΣl0\\Sigma\_\{l\}^\{0\}set\. By definition, there exists a computable relationR⊆ℕl\+1R\\subseteq\\mathbb\{N\}^\{l\+1\}such that

\(A\.5\)a∈A⇔\(Q1z1∈ℕ\)⋯\(Qlzl∈ℕ\)R\(a,z1,…,zl\)\.a\\in A\\iff\(Q\_\{1\}z\_\{1\}\\in\\mathbb\{N\}\)\\;\\cdots\\;\(Q\_\{l\}z\_\{l\}\\in\\mathbb\{N\}\)\\textrm\{ \}R\(a,z\_\{1\},\\ldots,z\_\{l\}\)\.Define a computably enumerable relation on the remaining parameters by

C\(a,z1,…,zl−1\)⟺\{\(∃zl∈ℕ\)R\(a,z1,…,zl\),for​l​odd;\(∃zl∈ℕ\)¬R\(a,z1,…,zl\),for​l​even\.C\(a,z\_\{1\},\\ldots,z\_\{l\-1\}\)\\quad\\Longleftrightarrow\\quad\\begin\{cases\}\(\\exists z\_\{l\}\\in\\mathbb\{N\}\)\\textrm\{ \}R\(a,z\_\{1\},\\ldots,z\_\{l\}\),&\\text\{ for \}l\\text\{ odd\};\\\\ \(\\exists z\_\{l\}\\in\\mathbb\{N\}\)\\textrm\{ \}\\neg R\(a,z\_\{1\},\\ldots,z\_\{l\}\),&\\textrm\{ for \}l\\text\{ even\}\.\\end\{cases\}By the nine\-unknown refinement of the DPRM theorem\[[35](https://arxiv.org/html/2610.08144#bib.bib35),[31](https://arxiv.org/html/2610.08144#bib.bib31)\]applied to the computably enumerable set\{⟨a,z1,…,zl−1⟩∈ℕ:C⁡\(a,z1,…,zl−1\)\}\\\{\\langle a,z\_\{1\},\.\.\.,z\_\{l\-1\}\\rangle\\in\\mathbb\{N\}:C\(a,z\_\{1\},\.\.\.,z\_\{l\-1\}\)\\\}, there exists a fixed integer\-coefficient polynomialq0​\(n~,x1,…,x9\)q\_\{0\}\(\\tilde\{n\},x\_\{1\},\.\.\.,x\_\{9\}\), wheren~\\tilde\{n\}is a variable, such that

C\(a,z1,…,zl−1\)⇔\(∃\(x1,…,x9\)∈ℕ9\)q0\(⟨a,z1,…,zl−1⟩,x1,…\.,x9\)=0\.C\(a,z\_\{1\},\.\.\.,z\_\{l\-1\}\)\\iff\(\\exists\(x\_\{1\},\.\.\.,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\)\\textrm\{ \}q\_\{0\}\(\\langle a,z\_\{1\},\.\.\.,z\_\{l\-1\}\\rangle,x\_\{1\},\.\.\.\.,x\_\{9\}\)=0\.Defining the polynomialq\(a,z1,…,zl−1,x1,…,x9\):=q0\(⟨a,z1,…,zl−1⟩,x1,…\.,x9\)q\(a,z\_\{1\},\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{9\}\):=q\_\{0\}\(\\langle a,z\_\{1\},\.\.\.,z\_\{l\-1\}\\rangle,x\_\{1\},\.\.\.\.,x\_\{9\}\), we have

C\(a,z1,…,zl−1\)⇔\(∃\(x1,…,x9\)∈ℕ9\)q\(a,z1,…,zl−1,x1,…,x9\)=0\.C\(a,z\_\{1\},\\ldots,z\_\{l\-1\}\)\\iff\(\\exists\(x\_\{1\},\\ldots,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\)\\textrm\{ \}q\(a,z\_\{1\},\\ldots,z\_\{l\-1\},x\_\{1\},\\ldots,x\_\{9\}\)=0\.Ifllis odd, this representation permits \([A\.5](https://arxiv.org/html/2610.08144#A1.E5)\) to be expressed as

a∈A⇔\\displaystyle a\\in A\\iff\(∃z1∈ℕ\)⋯\(∀zl−1∈ℕ\)\(∃\(x1,…,x9\)∈ℕ9\)\\displaystyle\(\\exists z\_\{1\}\\in\\mathbb\{N\}\)\\;\\cdots\\;\(\\forall z\_\{l\-1\}\\in\\mathbb\{N\}\)\(\\exists\(x\_\{1\},\.\.\.,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\)q⁡\(a,z1,…,zl−1,x1,…,x9\)=0\.\\displaystyle q\(a,z\_\{1\},\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{9\}\)=0\.Ifllis even, negation of the defining condition forCCgives

\(∀zl∈ℕ\)R\(a,z1,…,zl\)⇔\(∀\(x1,…,x9\)∈ℕ9\)q\(a,z1,…,zl−1,x1,…,x9\)≠0,\(\\forall z\_\{l\}\\in\\mathbb\{N\}\)\\textrm\{ \}R\(a,z\_\{1\},\\ldots,z\_\{l\}\)\\iff\(\\forall\(x\_\{1\},\\ldots,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\)\\textrm\{ \}q\(a,z\_\{1\},\\ldots,z\_\{l\-1\},x\_\{1\},\\ldots,x\_\{9\}\)\\neq 0,so that \([A\.5](https://arxiv.org/html/2610.08144#A1.E5)\) can be expressed as

a∈A⇔\\displaystyle a\\in A\\iff\(∃z1∈ℕ\)\(∀z2∈ℕ\)⋯\(∃zl−1∈ℕ\)\(∀\(x1,…,x9\)∈ℕ9\)\\displaystyle\(\\exists z\_\{1\}\\in\\mathbb\{N\}\)\(\\forall z\_\{2\}\\in\\mathbb\{N\}\)\\;\\cdots\\;\(\\exists z\_\{l\-1\}\\in\\mathbb\{N\}\)\(\\forall\(x\_\{1\},\.\.\.,x\_\{9\}\)\\in\\mathbb\{N\}^\{9\}\)q⁡\(a,z1,…,zl−1,x1,…,x9\)≠0\.\\displaystyle q\(a,z\_\{1\},\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{9\}\)\\neq 0\.Consequently, regardless of the parity ofll, we have replaced the final quantification\(Ql​zl∈ℕ\)\(Q\_\{l\}z\_\{l\}\\in\\mathbb\{N\}\)in \([A\.5](https://arxiv.org/html/2610.08144#A1.E5)\) sans appending an additional quantifier alternation\. Whenk\>9k\>9, we regardqqas independent of the additional variablesx10,…,xkx\_\{10\},\\ldots,x\_\{k\}\. Define the binary predicateW⊆ℕ2W\\subseteq\\mathbb\{N\}^\{2\}by

W⁡\(a,j\)⇔pj​\(n,z2,…,zl−1,x1,…,xk\)≡q⁡\(a,n,z2​…,zl−1,x1,…,xk\),W\(a,j\)\\iff p\_\{j\}\(n,z\_\{2\},\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{k\}\)\\equiv q\(a,n,z\_\{2\}\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{k\}\),where≡\\equivdenotes that the two polynomials, whose variables aren,z2,…,zl−1,x1,…,xkn,z\_\{2\},\.\.\.,z\_\{l\-1\},x\_\{1\},\.\.\.,x\_\{k\}, have coinciding coefficients; givenaaandjjthis is decidable\. Since\(pe\)e∈ℕ\(p\_\{e\}\)\_\{e\\in\\mathbb\{N\}\}enumerates all integer\-coefficient polynomials inl−1\+kl\-1\+kvariables, the functiont⁡\(a\):=μ​j​\[W⁡\(a,j\)\]t\(a\):=\\mu j\[W\(a,j\)\]is well\-defined and computable\. The preceding equivalences imply that

a∈A⇔t⁡\(a\)∈dl\.a\\in A\\iff t\(a\)\\in d\_\{l\}\.That is,A⩽mdlA\\leqslant\_\{m\}d\_\{l\}, establishingΣl0\\Sigma^\{0\}\_\{l\}\-completeness ofdld\_\{l\}\. By definition ofdld\_\{l\}, the leastn∈ℕn\\in\\mathbb\{N\}satisfyingBe\(l\)​\(n\)B^\{\(l\)\}\_\{e\}\(n\)exists exactly whene∈dle\\in d\_\{l\}\. By Post’s theorem\[[52](https://arxiv.org/html/2610.08144#bib.bib52)\], we havedl⩽T∅\(l−1\)⇔dl∈Δl0d\_\{l\}\\leqslant\_\{T\}\\emptyset^\{\(l\-1\)\}\\iff d\_\{l\}\\in\\Delta\_\{l\}^\{0\}\. Sincedl∈Σl0d\_\{l\}\\in\\Sigma\_\{l\}^\{0\}, this becomesdl⩽T∅\(l−1\)⇔dl∈Πl0d\_\{l\}\\leqslant\_\{T\}\\emptyset^\{\(l\-1\)\}\\iff d\_\{l\}\\in\\Pi\_\{l\}^\{0\}\. But whenever a set belongs toΠl0\\Pi\_\{l\}^\{0\}so too does any set that \(many\-one\) reduces to it; thus ifdl∈Πl0d\_\{l\}\\in\\Pi\_\{l\}^\{0\}, then byΣl0\\Sigma\_\{l\}^\{0\}\-completeness we would haveΣl0⊆Πl0\\Sigma\_\{l\}^\{0\}\\subseteq\\Pi\_\{l\}^\{0\}, contrary to the strictness of the arithmetical hierarchy\. Consequently, we cannot havedl⩽T∅\(l−1\)d\_\{l\}\\leqslant\_\{T\}\\emptyset^\{\(l\-1\)\}\. ∎

When we use the samekkand the same polynomial enumeration, the casel=2l=2givesBe\(2\)​\(n\)=Be​\(n\)B\_\{e\}^\{\(2\)\}\(n\)=B\_\{e\}\(n\)for everyn∈ℕn\\in\\mathbb\{N\}, so thatd2=dd\_\{2\}=d, which recovers Theorem[A\.3](https://arxiv.org/html/2610.08144#A1.Thmtheorem3)\. Moreover, for everyl⩾2l\\geqslant 2, the complement ofdld\_\{l\}isΠl0\\Pi\_\{l\}^\{0\}\-complete, anddld\_\{l\}has the Turing degree of∅\(l\)\\emptyset^\{\(l\)\}\(since∅\(l\)\\emptyset^\{\(l\)\}isΣl0\\Sigma\_\{l\}^\{0\}\-complete by Post’s Theorem\[[52](https://arxiv.org/html/2610.08144#bib.bib52)\]\)\. For each fixedl⩾2l\\geqslant 2ande∈ℕe\\in\\mathbb\{N\}, letne\(l\)n^\{\(l\)\}\_\{e\}be the leastnnfor whichBe\(l\)​\(n\)B^\{\(l\)\}\_\{e\}\(n\)holds, and definere\(l\)=1/\(ne\(l\)\+1\)r^\{\(l\)\}\_\{e\}=1/\(n^\{\(l\)\}\_\{e\}\+1\)\. Bothne\(l\)n^\{\(l\)\}\_\{e\}andre\(l\)r^\{\(l\)\}\_\{e\}are left undefined if there is no suchnn\. Replacingnen\_\{e\}andrer\_\{e\}in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)byne\(l\)n^\{\(l\)\}\_\{e\}andre\(l\)r^\{\(l\)\}\_\{e\}, respectively, gives the same least\-number construction\. The displayed identity\(re\(l\)\+1\)2=\(re\(l\)\)2\+2​re\(l\)\+1\(r^\{\(l\)\}\_\{e\}\+1\)^\{2\}=\(r^\{\(l\)\}\_\{e\}\)^\{2\}\+2r^\{\(l\)\}\_\{e\}\+1remains elementary to establish, while aseevaries, deciding whether the stated definition ofre\(l\)r^\{\(l\)\}\_\{e\}refers to a well\-defined number is aΣl0\\Sigma^\{0\}\_\{l\}\-complete problem\. Accordingly, we have established the existence of presupposition\-resolution problems of unbounded finite arithmetical complexity\.

For the SCI classification of the presupposition resolution problem we have thus far discussed, we use*arithmetic \(computable\) towers*; see\[[15](https://arxiv.org/html/2610.08144#bib.bib15), Definitions 5\.2–5\.6\]for the formal definition\. The input spaceΩ\\Omegaisℕ\\mathbb\{N\}and the output space isℳ=\{0,1\}\\mathcal\{M\}=\\\{0,1\\\}with the discrete metric\. A tower of heighth⩾1h\\geqslant 1for a functionΞ:Ω→\{0,1\}\\Xi:\\Omega\\to\\\{0,1\\\}is given by a bottom\-level computable functionΓ:Ω×ℕh→\{0,1\}\\Gamma:\\Omega\\times\\mathbb\{N\}^\{h\}\\to\\\{0,1\\\}that satisfies

Ξ\(e\)=lims1→∞⋯limsh→∞Γ\(e,s1,…,sh\),\\Xi\(e\)=\\lim\_\{s\_\{1\}\\to\\infty\}\\cdots\\lim\_\{s\_\{h\}\\to\\infty\}\\Gamma\(e,s\_\{1\},\\ldots,s\_\{h\}\),for eache∈Ωe\\in\\Omega\. In particular, each successive limit exists \(for every fixed choice of the outer indices\)\. An arithmetical tower of height zero forΞ\\Xiis simply a computable functionΓ:Ω→\{0,1\}\\Gamma:\\Omega\\to\\\{0,1\\\}withΓ=Ξ\\Gamma=\\Xi\. Given any functionΞ:Ω→\{0,1\}\\Xi:\\Omega\\to\\\{0,1\\\}, we defineSCIA⁡\(Ξ\)\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\)to be the leasth⩾0h\\geqslant 0for which there is an arithmetical tower of heighthhforΞ\\Xi; we defineSCIA⁡\(Ξ\)=\+∞\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\)=\+\\inftywhen no such tower exists\. We also defineΔh\+1A\\Delta^\{\\mathrm\{A\}\}\_\{h\+1\}to denote the class of problemsΞ\\XiwithSCIA⁡\(Ξ\)⩽h\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\)\\leqslant h, for eachh⩾1h\\geqslant 1\.

###### Corollary A\.5\(Unbounded SCI for presupposition resolution\)\.

For eachl⩾2l\\geqslant 2, defineΞdl:Ω→\{0,1\}\\Xi\_\{d\_\{l\}\}:\\Omega\\to\\\{0,1\\\}byΞdl​\(e\)=1\\Xi\_\{d\_\{l\}\}\(e\)=1if and only ife∈dle\\in d\_\{l\}\. Withk⩾9k\\geqslant 9and the enumeration in Theorem[A\.4](https://arxiv.org/html/2610.08144#A1.Thmtheorem4), we have

SCIA⁡\(Ξdl\)=lfor every​l⩾2\.\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\_\{d\_\{l\}\}\)=l\\qquad\\text\{for every \}l\\geqslant 2\.Equivalently, the decision problem for the setdld\_\{l\}lies inΔl\+1A∖ΔlA\\Delta^\{\\mathrm\{A\}\}\_\{l\+1\}\\setminus\\Delta^\{\\mathrm\{A\}\}\_\{l\}\.

###### Proof\.

Fixl⩾2l\\geqslant 2\. Sincedl∈Σl0d\_\{l\}\\in\\Sigma\_\{l\}^\{0\}, we havedl∈ΣlAd\_\{l\}\\in\\Sigma\_\{l\}^\{\\mathrm\{A\}\}\(as the SCI hierarchy generalises the arithmetical hierarchy, as discussed above\)\. This meansSCIA⁡\(Ξdl\)⩽l\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\_\{d\_\{l\}\}\)\\leqslant l\.

On the other hand, ifSCIA⁡\(Ξdl\)<l\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\_\{d\_\{l\}\}\)<l, then there is an arithmetical tower of height0⩽h<l0\\leqslant h<lforΞdl\\Xi\_\{d\_\{l\}\}\. This would give thatdl∈Δh\+10d\_\{l\}\\in\\Delta\_\{h\+1\}^\{0\}\(again using that the SCI hierarchy generalises the arithmetical hierarchy\) and thus alsodl∈Δl0d\_\{l\}\\in\\Delta\_\{l\}^\{0\}sinceh<lh<l\. Butdld\_\{l\}isΣl0\\Sigma\_\{l\}^\{0\}\-complete so cannot lie inΔl0\\Delta\_\{l\}^\{0\}\( elseΣl0⊆Πl0\\Sigma\_\{l\}^\{0\}\\subseteq\\Pi\_\{l\}^\{0\}, contrary to strictness of the arithmetical hierarchy\[[52](https://arxiv.org/html/2610.08144#bib.bib52), Corollary 4\.2\.3, p\. 85\]\)\. This meansSCIA⁡\(Ξdl\)⩾l\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\_\{d\_\{l\}\}\)\\geqslant l\. We conclude thatSCIA⁡\(Ξdl\)=l\\operatorname\{SCI\}\_\{\\mathrm\{A\}\}\(\\Xi\_\{d\_\{l\}\}\)=l, as required\. ∎

#### A\.2\.1\.The problem of resolving ambiguities has SCI=∞=\\infty

Recall Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)andBe​\(n\)B\_\{e\}\(n\)from \([4\.1](https://arxiv.org/html/2610.08144#S4.E1)\)\. Recall that the ambiguity in Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1)– whethernen\_\{e\}is well defined or not – was caused by the following question:

> ‘Is\{n∈ℕ:Be​\(n\)\}\\\{n\\in\\mathbb\{N\}:B\_\{e\}\(n\)\\\}empty or not?

Note that we could have made Example[4\.1](https://arxiv.org/html/2610.08144#S4.Thmtheorem1), and the definition ofnen\_\{e\}, more general yielding an ambiguity caused by the question:

> ‘Is\{n∈ℕ:Be\(l\)​\(n\)\}\\\{n\\in\\mathbb\{N\}:B^\{\(l\)\}\_\{e\}\(n\)\\\}empty or not?

Here,Be\(l\)​\(n\)B^\{\(l\)\}\_\{e\}\(n\)is defined for integersl⩾2l\\geqslant 2in \([A\.4](https://arxiv.org/html/2610.08144#A1.E4)\)\. Note that a trustworthy AI autoformaliser that will always provide an output: either a semantically faithful translation or ‘this statement cannot be translated’ must resolve the above question for eache∈ℕe\\in\\mathbb\{N\}andl⩾2l\\geqslant 2\. However, by Corollary[A\.5](https://arxiv.org/html/2610.08144#A1.Thmtheorem5)– for each fixedll– this problem has SCI=l=l\. Hence, the problem of answering the above question for alle∈ℕe\\in\\mathbb\{N\}andl⩾2l\\geqslant 2has SCI=∞=\\infty\. We can now make sense of our informal statement:

> *Providing semantically faithful AI autoformalisation is harder than any computational problem\.*

By ‘semantically faithful AI autoformalisation’ we mean a trustworthy AI autoformaliser that will always provide an output – as above\. Also, by ‘any computational problem’ we mean any computational problem with finite SCI\. So our statement above – which was made informal for the purpose of readability – means: Every trustworthy semantically faithful AI formaliser \(as above\) must solve problems that are harder than any problem with finite SCI\.

## References

- \[1\]J\. Alper et al\.Leiden Declaration on Artificial Intelligence and Mathematics, 2026\.2 June 2026\.[doi:10\.5281/zenodo\.20302944](https://doi.org/10.5281/zenodo.20302944)\.
- \[2\]L\. Alpöge and T\. Buckmaster\.Blowup for the Euler Equations with Smooth Forcing\.Preprint, 2026\.
- \[3\]A\. Avila et al\.A Severe Misalignment of AI in Mathematics, 2026\.11 September 2026\.[doi:10\.5281/zenodo\.22737750](https://doi.org/10.5281/zenodo.22737750)\.
- \[4\]A\. Bastounis, A\. C\. Hansen, and V\. Vlačić\.The extended Smale’s 9th problem – On computational barriers and paradoxes in estimation, regularisation, computer\-assisted proofs and learning\.arXiv:2110\.15734, 2021\.
- \[5\]J\. T\. Beale, T\. Kato, and A\. Majda\.Remarks on the breakdown of smooth solutions for the 3\-D Euler equations\.Communications in Mathematical Physics, 94\(1\):61–66, 1984\.
- \[6\]J\. Ben\-Artzi, M\. J\. Colbrook, A\. C\. Hansen, O\. Nevanlinna, and M\. Seidel\.Computing spectra – On the solvability complexity index hierarchy and towers of algorithms\.arXiv:1508\.03280v5, 2020\.
- \[7\]J\. Ben\-Artzi, A\. C\. Hansen, O\. Nevanlinna, and M\. Seidel\.New barriers in complexity theory: On the solvability complexity index and the towers of algorithms\.Comptes Rendus Mathematique, 353\(10\):931 – 936, 2015\.
- \[8\]F\. Berto and L\. Hornischer\.Cognitive synonymy: a dead parrot?Philosophical Studies, 180\(9\):2727–2752, 2023\.
- \[9\]L\. Blum, M\. Shub, and S\. Smale\.On a theory of computation and complexity over the real numbers: NP\-completeness, recursive functions and universal machines\.Bulletin of the American Mathematical Society \(New Series\), 21\(1\):1–46, 1989\.
- \[10\]K\. Buzzard\.FLT: Anthropic has beaten me to it\.Xena Project blog, 2026\.4 September 2026\.[Online article](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/)\.
- \[11\]L\. Caffarelli, R\. Kohn, and L\. Nirenberg\.Partial regularity of suitable weak solutions of the Navier–Stokes equations\.Communications on Pure and Applied Mathematics, 35\(6\):771–831, 1982\.
- \[12\]J\. Chen and T\. Y\. Hou\.Stable nearly self\-similar blowup of the 2D Boussinesq and 3D Euler equations with smooth data I: Analysis, 2022\.Preprint; version 4, revised 16 August 2026\.
- \[13\]J\. Chen and T\. Y\. Hou\.Stable Nearly Self\-Similar Blowup of the 2D Boussinesq and 3D Euler Equations with Smooth Data II: Rigorous Numerics\.Multiscale Modeling & Simulation, 23\(1\):25–130, 2025\.
- \[14\]M\. J\. Colbrook, V\. Antun, and A\. C\. Hansen\.The difficulty of computing stable and accurate neural networks: On the barriers of deep learning and Smale’s 18th problem\.Proceedings of the National Academy of Sciences, 119\(12\):e2107151119, Mar\. 2022\.
- \[15\]M\. J\. Colbrook and A\. C\. Hansen\.The foundations of spectral computations via the Solvability Complexity Index hierarchy\.J\. Eur\. Math\. Soc\., 25\(12\):4639–4718, 2022\.
- \[16\]P\. Constantin, C\. L\. Fefferman, and A\. J\. Majda\.Geometric constraints on potentially singular solutions for the 3\-D Euler equations\.Communications in Partial Differential Equations, 21\(3–4\):559–571, 1996\.
- \[17\]D\. Cordoba and L\. Martinez\-Zoroa\.Finite time singularities of smooth solutions for the 2D incompressible porous media \(IPM\) equation with a smooth source\.arXiv:2410\.22920 \[math\.AP\], 2024\.Preprint; version 3, revised 13 February 2025\.
- \[18\]D\. Cordoba, L\. Martinez\-Zoroa, and F\. Zheng\.Finite time blow\-up for the hypodissipative Navier Stokes equations with a force inLt1​Cx1,ϵ∩Lt∞​Lx2L^\{1\}\_\{t\}C\_\{x\}^\{1,\\epsilon\}\\cap L^\{\\infty\}\_\{t\}L\_\{x\}^\{2\}\.Archive for Rational Mechanics and Analysis, 250:38, 2026\.
- \[19\]C\. De Lellis and L\. Székelyhidi, Jr\.The Euler equations as a differential inclusion\.Annals of Mathematics, 170\(3\):1417–1436, 2009\.
- \[20\]P\. Doyle and C\. McMullen\.Solving the quintic by iteration\.Acta Mathematica, 163\(3\-4\):151–180, 1989\.
- \[21\]T\. M\. Elgindi\.Finite\-time singularity formation forC1,αC^\{1,\\alpha\}solutions to the incompressible Euler equations onℝ3\\mathbb\{R\}^\{3\}\.Annals of Mathematics, 194\(3\):647–727, 2021\.
- \[22\]H\. B\. Enderton\.A Mathematical Introduction to Logic\.Academic Press, 2 edition, 2001\.
- \[23\]C\. L\. Fefferman\.Existence and smoothness of the Navier–Stokes equation\.In J\. Carlson, A\. Jaffe, and A\. Wiles, editors,The Millennium Prize Problems, pages 57–67\. Clay Mathematics Institute and American Mathematical Society, 2006\.
- \[24\]H\. Fujita and T\. Kato\.On the Navier–Stokes initial value problem\. I\.Archive for Rational Mechanics and Analysis, 16\(4\):269–315, 1964\.
- \[25\]L\. E\. Gazdag, A\. Bastounis, and A\. C\. Hansen\.Generalised hardness of approximation and the SCI hierarchy – on determining the boundaries of training algorithms in AI\.Foundations of Computational Mathematics, July 2026\.
- \[26\]K\. Gödel\.Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I\.Monatshefte für mathematik und physik, 38\(1\):173–198, 1931\.
- \[27\]T\. Hales\.An argument for controlled natural languages in mathematics, 2019\.Position essay, 20 June 2019\.
- \[28\]A\. C\. Hansen\.On the solvability complexity index, thenn\-pseudospectrum and approximations of spectra of operators\.Journal of the American Mathematical Society, 24\(1\):81–124, 2011\.
- \[29\]T\. Y\. Hou\.Potentially Singular Behavior of the 3D Navier–Stokes Equations\.Foundations of Computational Mathematics, 23:2251–2299, 2023\.
- \[30\]T\. F\. Icard and L\. S\. Moss\.A Simple Logic of Concepts\.Journal of Philosophical Logic, 52:705–730, 2023\.
- \[31\]J\. P\. Jones\.Universal Diophantine equation\.The Journal of Symbolic Logic, 47\(3\):549–571, 1982\.[doi:10\.2307/2273588](https://doi.org/10.2307/2273588)\.
- \[32\]Lean community\.Atlas \(Meta\)\.Zulip discussion in the Autoformalization channel, 2026\.[Discussion thread](https://leanprover.zulipchat.com/#narrow/channel/583336-Autoformalization/topic/Atlas.20.28Meta.29)\. Accessed 18 September 2026\.
- \[33\]J\. Leray\.Sur le mouvement d’un liquide visqueux emplissant l’espace\.Acta Mathematica, 63:193–248, 1934\.
- \[34\]G\. Luo and T\. Y\. Hou\.Potentially singular solutions of the 3D axisymmetric Euler equations\.Proceedings of the National Academy of Sciences, 111\(36\):12968–12973, 2014\.
- \[35\]Y\. V\. Matiyasevich\.Hilbert’s Tenth Problem\.Foundations of Computing\. MIT Press, Cambridge, MA, 1993\.
- \[36\]C\. McMullen\.Families of rational maps and iterative root\-finding algorithms\.Annals of Mathematics, 125\(3\):467–493, 1987\.
- \[37\]C\. McMullen\.Braiding of the attractor and the failure of iterative algorithms\.Inventiones Mathematicae, 91\(2\):259–272, 1988\.
- \[38\]R\. Montague\.Universal grammar\.Theoria, 36\(3\):373–398, 1970\.
- \[39\]R\. Montague\.English as a Formal Language\.In R\. H\. Thomason, editor,Formal Philosophy: Selected Papers of Richard Montague, pages 188–221\. Yale University Press, New Haven, CT, 1974\.Originally published in 1970\.
- \[40\]Y\. N\. Moschovakis\.A logical calculus of meaning and synonymy\.Linguistics and Philosophy, 29\(1\):27–89, 2006\.[doi:10\.1007/s10988\-005\-6920\-7](https://doi.org/10.1007/s10988-005-6920-7)\.
- \[41\]M\. B\. Nathanson\.Cantor polynomials and the Fueter–Pólya theorem\.The American Mathematical Monthly, 123\(10\):1001–1012, 2016\.[doi:10\.4169/amer\.math\.monthly\.123\.10\.1001](https://doi.org/10.4169/amer.math.monthly.123.10.1001)\.
- \[42\]J\. Nečas, M\. Růžička, and V\. Šverák\.On Leray’s self\-similar solutions of the Navier–Stokes equations\.Acta Mathematica, 176\(2\):283–294, 1996\.
- \[43\]W\. V\. O\. Quine\.Meaning and Translation\.In R\. A\. Brower, editor,On Translation, pages 148–172\. Harvard University Press, Cambridge, MA, 1959\.
- \[44\]W\. V\. O\. Quine\.On the Reasons for Indeterminacy of Translation\.The Journal of Philosophy, 67\(6\):178–183, 1970\.
- \[45\]F\. Rabe\.How to identify, translate and combine logics?Journal of Logic and Computation, 27\(6\):1753–1798, 2017\.
- \[46\]A\. Rammal, N\. Patel, F\. Gloeckle, A\. Hayat, J\. Kempe, R\. Munos, C\. Arnal, and V\. Cabannes\.Formalizing mathematics at scale\.[arXiv:2605\.29955](https://arxiv.org/abs/2605.29955), 2026\.
- \[47\]G\. Seregin\.A certain necessary condition of potential blow up for Navier–Stokes equations\.Communications in Mathematical Physics, 312\(3\):833–845, 2012\.
- \[48\]J\. Serrin\.On the interior regularity of weak solutions of the Navier–Stokes equations\.Archive for Rational Mechanics and Analysis, 9:187–195, 1962\.
- \[49\]S\. Smale\.The fundamental theorem of algebra and complexity theory\.Bulletin of the American Mathematical Society, 4\(1\):1–36, 1981\.
- \[50\]S\. Smale\.Complexity theory and numerical analysis\.InActa numerica, 1997, volume 6 ofActa Numer\., pages 523–551\. Cambridge Univ\. Press, Cambridge, 1997\.
- \[51\]S\. Smale\.The work of Curtis T McMullen\.InProceedings of the International Congress of Mathematicians I, Berlin, Doc\. Math\. J\. DMV, pages 127–132\. 1998\.
- \[52\]R\. I\. Soare\.Turing Computability: Theory and Applications\.Theory and Applications of Computability\. Springer, Berlin–Heidelberg, 2016\.[doi:10\.1007/978\-3\-642\-31933\-4](https://doi.org/10.1007/978-3-642-31933-4)\.
- \[53\]E\. M\. Stein\.Singular Integrals and Differentiability Properties of Functions \(PMS\-30\)\.Princeton University Press, 1970\.
- \[54\]Z\.\-W\. Sun\.Ten unknowns for hilbert’s tenth problem over the integers, 2026\.
- \[55\]T\. Tao\.Finite time blowup for an averaged three\-dimensional Navier–Stokes equation\.Journal of the American Mathematical Society, 29\(3\):601–674, 2016\.
- \[56\]A\. Tarski\.The Semantic Conception of Truth: and the Foundations of Semantics\.Philosophy and Phenomenological Research, 4\(3\):341–376, 1944\.
- \[57\]The mathlib Community\.Mathlib\.Order\.Lattice\.Nat: Conditionally complete linear order structure on the natural numbers\.Online API documentation\.[Documentation forNat\.sInf\_defandNat\.sInf\_empty](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice/Nat.html)\. Accessed 18 September 2026\.
- \[58\]A\. M\. Turing\.On Computable Numbers, with an Application to the Entscheidungsproblem\.Proceedings of the London Mathematical Society, S2\-42\(1\):230, 1936\.
- \[59\]J\. van Benthem\.Natural Language and Logic of Agency\.Journal of Logic, Language and Information, 23\(3\):367–382, 2014\.
- \[60\]J\. van Benthem and F\. Liu\.New logical perspectives on monotonicity\.In D\. Deng, F\. Liu, M\. Liu, and D\. Westerståhl, editors,Monotonicity in Logic and Language, pages 1–12, Berlin, Heidelberg, 2020\. Springer Berlin Heidelberg\.
- \[61\]S\. Weinberger\.Computers, Rigidity, and Moduli: The Large\-Scale Fractal Geometry of Riemannian Moduli Space\.Princeton University Press, USA, 2004\.