Paper deep dive
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
Alexander Bastounis, Fabian Circelli, Anders C. Hansen
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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$). 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.
Tags
Links
- Source: https://arxiv.org/abs/2610.08144v1
- Canonical: https://arxiv.org/abs/2610.08144v1
Trouble viewing inline? Open PDF directly →
Full Text
96,555 characters extracted from source content.
Expand or collapse full text
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. Bastounis Address: Department of Mathematics, King’s College London Email address: alexander.bastounis@kcl.ac.uk , F. Circelli Address: Department of Applied Mathematics and Theoretical Physics, University of Cambridge Email address: fac43@cam.ac.uk and A. C. Hansen* Address: Department of Applied Mathematics and Theoretical Physics, University of Cambridge Email address: a.hansen@damtp.cam.ac.uk 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 =∞=∞). 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 Classification35Q30, 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: (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. (i) 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. 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). Warning: Meeting the success criterion of (i) 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). Another possibility is that both the NL proof and the formal proof are correct, but completely different (see Example 2.2). 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 (i). This is, however, in general an extremely difficult problem, as we discuss in §4. 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. Figure 1. ChatGPT-6 (Astra Ultra) ‘translates’ the wrong NL ‘proof’ in Example 2.1 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 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. Example 2.1 (A correct statement with an incorrect NL proof, and a ‘translation’ to a different, correct Lean proof). Consider the following theorem: Let p(x)=x3−x2−x+1p(x)=x^3-x^2-x+1, where x∈ℝx . Then p(x)⩾0p(x) 0 for x⩾−1x -1. Incorrect NL proof. The roots are −1-1, of multiplicity two, and 11, of multiplicity one. Hence11 1 Note that the ‘hence’ is also dubious without mentioning the leading coefficient of p., p(x)=(x−1)(x+1)2⩾0,p(x)=(x-1)(x+1)^2 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 of p(x)p(x) is wrong too. In the exchange shown in Figure 1, 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. Figure 2. ChatGPT-6 (Astra Ultra) ‘translates’ the correct NL proof in Example 2.2 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: Let A=(aij)A=(a_ij) be a real symmetric n×n× n matrix. Then tr(A2)⩾0tr(A^2) 0. Correct NL proof. Diagonalise A in an orthonormal eigenbasis. Since tr(A2)tr(A^2) is invariant under a change of basis, we may assume A=diag(λ1,…,λn)A=diag( _1,…, _n). Now compute (2.1) tr(A2)=∑i(A2)ii=∑i,jaijaji.tr(A^2)= _i(A^2)_i= _i,ja_ija_ji. As aij=0a_ij=0 for i≠ji≠ j and aii=λia_i= _i, this reduces to ∑iλi2⩾0 _i _i^2 0. ∎ In the exchange shown in Figure 2, 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. 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), keeping the original matrix A: it then uses aji=aija_ji=a_ij to conclude that ∑i,jaijaji=∑i,jaij2⩾0. _i,ja_ija_ji= _i,ja_ij^2 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, 18, 55, 48, 42, 24, 47, 29, 18] (we can only cite a small subset of papers here), dating back to Leray’s fundamental paper from 1934 [33], and was designated a Clay Millennium Prize Problem in 2000 [23]. 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. 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). 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 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. 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 concerns the estimate in Lemma 8.6, equation (8.19), of OpenAI’s Finite time blowup for Navier–Stokes. We compare this estimate with the cited Lean declarations at commit f9e8bc5 (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. With m a nonnegative integer, the comparison in Figure 3 is (3.1) NL paper, equation (8.19): ‖N−1F‖Cym⩽Cm‖F‖Cym+4, \|N^-1F\|_C_y^m C_m\|F\|_C_y^m+4, (3.2) Lean Estimate: ‖N−1F‖Cym⩽Km‖F‖Cym+5. \|N^-1F\|_C_y^m 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×T^2 is a function of parameters in P and a torus variable y∈2y ^2, with 2:=ℝ2/ℤ2T^2:=R^2/Z^2. The non-negative constants CmC_m, KmK_m are independent of F but allowed to depend on m and the fixed direction vtv_t (which defines an operator N=vt⋅∇yN=v_t· _y). Note the above norms only involve torus derivatives. See §3.1.1 for further explanation of the notation. The proof of Lemma 8.6 opens with the following passage (source paper, page 96): “The divisor bound (6.7) gives |vt⋅k|−1⩽C(1+|k|)|v_t· k|^-1 C(1+|k|). Four more derivatives of F than 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): ⬇ theorem norm_derivativeWord_inverse_le (d : Direction) f : Source P (hf : ContDiff ℝ ∞ f) (hp : Periodic f) (w : List Bool) (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 (*@ red+ 5@*)) (slice f p) (x, y)‖ ≤ C) (hsecond : ∀ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, ‖SmoothFourierData.xJet (w.length (*@ red+ 5@*)) (SmoothFourierData.swapFunction (slice f p)) (x, y)‖ ≤ C) : ‖derivativeWord w (slice (inverse d f) p) Y‖ ≤ ParametricTorusInverse.mixedLossConstant w.length * C := by have hbound := SmoothFourierData.coefficient_seminorm_bound (slice_smooth hf p) (hp p) (w.length + 1) hzero (by simpa only [Nat.add_assoc] using hfirst) (by simpa only [Nat.add_assoc] using hsecond) calc _ ≤ ((6 * ‖omega⁻¹‖) * ‖omega‖ w.length) * coeffSeminorm (w.length + 1) (coefficient f p) := inverse_derivativeWord_bound d (SmoothFourierData.rapid_coefficient (slice_smooth hf p) (hp p)) w Y _ ≤ ((6 * ‖omega⁻¹‖) * ‖omega‖ w.length) * ((3 ((w.length + 1) + 4) * C) * ∑’ k : Frequency, (weight k (*@ red4@*))⁻¹) := mul_le_mul_of_nonneg_left hbound (by positivity) _ = _ := by simp only [ParametricTorusInverse.mixedLossConstant, Nat.add_assoc]; ring Source (GitHub permalinks): openai/NavierStokesAndEuler, commit f9e8bc5. File: NavierStokes/SmoothFamilyTorusInverse.lean. Declaration: norm_derivativeWord_inverse_le, lines 1059–1080. 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 are the two hypotheses: ⬇ ‖SmoothFourierData.xJet (w.length (*@ red+ 5@*)) (slice f p) (x, y)‖ ≤ C) (hsecond : ∀ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, ‖SmoothFourierData.xJet (w.length (*@ red+ 5@*)) (SmoothFourierData.swapFunction (slice f p)) (x, y)‖ ≤ C) which 22 2 The parameter set P are 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, | ∂^m+5F(y_1,y_2)∂ y_1^m+5 | C, | ∂^m+5F(y_1,y_2)∂ y_2^m+5 | C, for every y=(y1,y2)∈2y=(y_1,y_2) ^2, and the conclusion ⬇ ParametricTorusInverse.mixedLossConstant w.length * C which33 3 Strictly speaking, w in 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 the y1y_1 coordinate and each ‘true’ entry a derivative in the y2y_2 coordinate. should be interpreted as |∂|w|N−1F(y1,y2)∂w|⩽K|w|⋅C, | ∂^|w|N^-1F(y_1,y_2)∂ w | K_|w|· C, with C the same constant as in the hypotheses, and where w is 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-indices w with |w|⩽m|w| m 44 4 This is not explicitly done as part of norm_derivativeWord_inverse_le., thereby obtaining ‖N−1F‖Cym⩽K^m‖F‖Cym+5, \|N^-1F \|_C^m_y K_m \|F \|_C^m+5_y, with K^m=max(K0,K1,…,Km) K_m= (K_0,K_1,…c,K_m). This estimate is then strictly weaker than equation (8.19) due to the extra derivative on the right-hand side. Remark 3.2 (Consistent mismatch between m+4m+4 and m+5m+5 derivatives). Similar estimates as (3.2) can be seen throughout OpenAI’s Lean code: for example, inverse_finiteJets and mixedJet_inverse_bound ://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/SmoothFamilyTorusInverse.lean#L865-L875\, and \, ://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/ParametricTorusInverse.lean#L654-L680 each contain a similar m+5m+5 derivative requirement, rather than the expected m+4m+4 derivatives from the NL paper, as in (3.1). 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 _k ^2 1 (1+|k| )^3 by using m+4m+4 derivatives. In contrast, the Lean code displayed above for (3.3) norm_derivativeWord_inverse_le ://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/NavierStokes/SmoothFamilyTorusInverse.lean#L1059-L1080 employs the series ∑k∈ℤ21(1+|k1|+|k2|)4 _k ^2 1(1+|k_1|+|k_2|)^4 (see the exponent ‘4’ highlighted in red in the code (3.3) above) and thus uses m+5m+5 derivatives instead. Tracing the proof of (3.3) we find that the series arises from applying the Lean theorem coefficient_seminorm_bound, just as Figure 3 mentions. Consequently, the Lean results discussed in this section are weaker 55 5 In fact, some such Lean results are actually incomparable with (3.1), due to the mismatch in the type of derivative. For example, the Lean theorem inverse_finiteJets uses mixed derivatives, not just torus derivatives. Note however that these results are still using m+5m+5 derivatives. than (3.1) in the NL proof. 3.1.1. Explanation of the notation and technical information The variable y=(y1,y2)y=(y_1,y_2) belongs to a two-dimensional torus 2=ℝ2/ℤ2T^2=R^2/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=( 2-1,1), N=v_t· _y=( 2-1) _y_1+ _y_2. The subscript t is specified in equation (6.2) of the source paper. Here F:2→ℂF:T^2 is smooth, with zero normalized Haar mean: ∫[0,1]2F(y)y=0 _[0,1]^2F(y)\,dy=0. The notation N−1FN^-1F denotes the unique smooth zero-mean solution φ of Nφ=FN =F. The zero-mean requirement assures this solution is uniquely specified (else any solution, via addition of a constant, yields another). For smooth G:2→ℂG:T^2 and a nonnegative integer r, the following norm is defined: ‖G‖Cyr:=maxsupy∈2a,b⩾0a+b⩽r|∂y1a∂y2bG(y)|,a,b∈ℕ.\|G\|_C_y^r:= _ subarrayca,b 0\\ a+b r subarray _y ^2| _y_1^a _y_2^bG(y)|, a,b . The subscript y means that other variables are held fixed. This is relevant in the case G is of the form G(y)=F(p,y)G(y)=F(p,y) for some F:P×2→ℂF:P×T^2 and some fixed p. 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 in §2. In the following example the AI autoformalisation results in a Lean proof of a different bound obtained by a substantively different mathematical argument. 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 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 concerns the estimate in equation (10.19) of OpenAI’s Finite time blowup for Navier–Stokes. We compare this estimate, together with its proof, with the cited Lean declaration at commit f9e8bc5. 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: with R⩾1R 1, the comparison in Figure 4 is (3.4) NL, equation (10.19): |∫πw⋅∇χR|⩽CTR[(BR+1)BR1/2+R−3/4BR3/4], for a.e. t∈(0,T), | π\,w·∇ _R | C_TR [(B_R+1)B_R^1/2+R^-3/4B_R^3/4 ], for a.e. t∈(0,T), (3.5) Lean estimate: |∫πw⋅∇χR|⩽CT[(BR1/2+1)(ARR+1R2)+R−7/4BR3/4],∀t∈(0,T), | π\,w·∇ _R | C_T [(B_R^1/2+1) ( A_RR+ 1R^2 )+R^-7/4B_R^3/4 ],∀ t∈(0,T), where both the left hand side and the right hand side of both (3.4) and (3.5) depend on t; see below for explanation of the notation. The NL paper’s bound is stated purely in terms of BRB_R, whereas the Lean estimate additionally depends on ARA_R. Here CTC_T is a finite nonnegative constant, allowed to depend on T (which itself is the maximum timescale for which the bounds are considered) and the norm conventions, but not on R. Although equation (10.17) in the NL paper bounds BRB_R above using ARA_R, it cannot be used to eliminate ARA_R from the Lean estimate to recover (10.19); the two bounds in (3.4) and (3.5) are therefore hard to compare. 66 6 In fact, the purpose of the lemma is to establish that w=0w=0 and hence the (equal to 00) bound on the right hand side of (3.4) is stricter than the (non-zero) bound on the right hand side of (3.5). However, this is only established after completing the entire proof of Lemma 10.5. The closest Lean code to (10.19) (equation (3.4) in our paper) is the following result: ⬇ p q : PressureField (H : PressureRecovery.Hypotheses T u v p q) (M(*@ _0@*) U(*@ _0@*) G(*@ _0@*) : ℝ (hM(*@ _0@*) : 0 ≤ M(*@ _0@*)) (hU(*@ _0@*) : 0 ≤ U(*@ _0@*)) (hG(*@ _0@*) : 0 ≤ G(*@ _0@*)) (hM : ∀ t ∈ Icc 0 T, MemLp (fun x => (u - v) (t, x)) 2 volume ∧ comparisonLpNorm 2 (fun x => (u - v) (t, x)) ≤ M(*@ _0@*)) (hU : ∀ t ∈ Icc 0 T, MemLp (fun x => u (t, x)) 3 volume ∧ comparisonLpNorm 3 (fun x => u (t, x)) ≤ U(*@ _0@*)) (hG : ∀ t ∈ Icc 0 T, ∀ i j : Fin 3, Integrable (tensorDiff u v t i j) volume ∧ comparisonLpNorm 1 (tensorDiff u v t i j) ≤ G(*@ _0@*)) : ∃ CP : ℝ, 0 ≤ CP ∧ ∀ R : ℝ, 1 ≤ R → ∀ t ∈ Ioo 0 T, |(*@ @*) x, (p - q) (t, x) * fderiv ℝ (ComparisonCutoffs.weight R) x ((u - v) (t, x))| ≤ CP * ((cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t (1 / 2 : ℝ) + 1) * (dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + 1 / R 2) + R (-(7 / 4 : ℝ)) * cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t (3 / 4 : ℝ)) := by obtain (*@ @*)CP, hCP, hbound(*@ @*) := exists_uniform_canonicalCutoffFlux_bound M(*@ _0@*) U(*@ _0@*) G(*@ _0@*) hM(*@ _0@*) hU(*@ _0@*) hG(*@ _0@*) refine (*@ @*)CP, hCP, ?_(*@ @*) intro R hR t ht have ht’ : t ∈ Icc 0 T := Ioo_subset_Icc_self ht have hu := NavierStokes.PeriodicUniqueness.spatial_smooth H.smooth_u ht’ have hv := NavierStokes.PeriodicUniqueness.spatial_smooth H.smooth_v ht’ exact(actual_flux_integrable_and_le_canonicalNorm H ht (zero_lt_one.trans_le hR) hu hv).2.trans (hbound R hR u v t hu hv (hM t ht’).1 (hU t ht’).1 (fun i j => (hG t ht’ i j).1) (hM t ht’).2 (hU t ht’).2 (fun i j => (hG t ht’ i j).2)) Source (GitHub permalinks): openai/NavierStokesAndEuler, commit f9e8bc5. File: NavierStokes/R3/PressureFlux.lean. Declaration: exists_uniform_actual_pressure_flux_bound, line 576. Note that similar bounds (which are nonetheless distinct from (3.5)) appear in exists_uniform_canonicalCutoffFlux_bound and canonicalCutoffFlux_bound77 7 In addition, there is a similar argument that appears in the file NavierStokes/R3StressPressureEstimate.lean as part of the definition of regularized_flux_Bound. Once again the bound established there is different from the one in (3.4), 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) is given in the following Lean code, taken from that of exists_uniform_actual_pressure_flux_bound, Line 576. ⬇ ((cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t (1 / 2 : ℝ) + 1) * (dissipationRoot (ComparisonCutoffs.cutoff R) (u - v) t / R + 1 / R 2) + R (-(7 / 4 : ℝ)) * cutoffL6 (ComparisonCutoffs.cutoff R) (u - v) t (3 / 4 : ℝ)) The discrepancy in (3.5) 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)). 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) The Lean proof does not rely on the boundedness of the Riesz transform as a map from L3/2→L3/2L^3/2→ L^3/2; it instead invokes Sobolev embedding to move to L2L^2 and uses the boundedness of the Riesz transform in L2L^2. The additional derivative involved in the Sobolev embedding is why (3.5) features ARA_R. (2) The Lean proof applies Hölder’s inequality with different exponents, which changes the bounds at the end. (3) In the Lean proof, the left hand integral in (3.4) is explicitly shown to be continuous in time. This ensures that the statement for almost every t∈(0,T)t∈(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 chooses 0⩽φ⩽10 1 to be smooth, compactly supported and equal to one on the unit ball. For R⩾1R 1, they write φR(x)=φ(x/R) _R(x)= (x/R) and χR=φR8 _R= ^8_R. Continuing, the NL paper states: ‘Let RiR_i be the Riesz transform with Fourier multiplier operator iξi/‖ξ‖2i _i/\|ξ\|_2.’ The NL proof of Lemma 10.5 begins by assuming that (v,P)(v,P) and (u,p)(u,p) are two solutions – with v (respectively u) the velocity and P (respectively p) the pressure – to a constructed Navier Stokes problem. The NL proof defines w:=v−uw:=v-u and π:=P−pπ:=P-p and proceeds to establish the vanishing of w88 8 The Lean proof actually uses w=u−vw=u-v and π=p−Pπ=p-P, with the sign difference carried through in further definitions.; the estimate (10.19) is a stepping stone towards this result. Note that v,u,wv,u,w all depend on a time parameter t as well as spatial parameters; the time parameter is suppressed throughout the remaining discussion. The proof also defines a distribution π∗=∑i,jRiRjgij _*= _i,jR_iR_jg_ij where Ri,RjR_i,R_j are Riesz transforms, and where g=(gij)i,j∈1,2,3g=(g_ij)_i,j∈\1,2,3\ with gij=vivj−uiuj=wiwj+wiuj+uiwjg_ij=v_iv_j-u_iu_j=w_iw_j+w_iu_j+u_iw_j. As indicated in Figure 4, using the NL paper’s notation, AR:=(∫χR|∇w|2)1/2,BR:=‖φR4w‖L6,A_R:= ( _R|∇ w|^2 )^1/2, B_R:=\| _R^4w\|_L^6, so that ARA_R is a localized L2L^2 gradient norm and BRB_R a localized L6L^6 velocity norm. The purpose of defining π∗ _* is that it is an attempt to get an explicit approximation for π in terms of the velocity fields; hence instead of directly analysing the integrand in (10.19), one replaces π in this term by π∗ _*99 9 A large part of the NL proof of Lemma 10.5 addresses this issue; ultimately, it suffices to show that ∇π=∇π∗∇π=∇ _* in the sense of distributions.. The integrand is then factored into a product of two terms: φR4π∗ _R^4 _* and another test function containing φR3 _R^3. The Lean proof differs here, in that it splits the integral into φR2π∗ _R^2 _* and another test function containing φR5 _R^5; we shall see the consequences of this change later. The NL proof now tries to bound φR4π∗ _R^4 _*. The strategy here is to move φR4 _R^4 into the argument of the Riesz transformations in the definition of π∗ _*; doing so ensures that these Riesz transforms are being applied to functions with compact support in LpL^p spaces. In doing so one must pay a penalty, since aRib≠RiabaR_ib≠ R_iab in general for functions a,ba,b. Hence (10.18) in the NL paper establishes that (3.6) φR4π∗=∑i,jRiRj(φR4gij)+∑i,j[φR4,RiRj]gij _R^4 _*= _i,jR_iR_j( _R^4g_ij)+ _i,j[ _R^4,R_iR_j]g_ij where [⋅,⋅][·,·] 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 _R^2 instead of φR4 _R^4. Mathematically, the Lean argument is the following calculation 1010 10 Lean takes the real parts of many terms in this bound, but this is not especially important for our exposition. ∫πw⋅∇χR π w·∇ _R =∑i,j∈1,2,3∫gijRiRj(w⋅∇φR8)=∑i,j∈1,2,3∫gijRiRj(w⋅8φR2φR5∇φR) = _i,j∈\1,2,3\ g_ijR_iR_j(w·∇ _R^8)= _i,j∈\1,2,3\ g_ijR_iR_j(w· 8 ^2_R ^5_R∇ _R) (3.7) =8∑i,j∫φR2gijRiRj(w⋅φR5∇φR)+8∑i,j∫gij[RiRj,φR2](w⋅φR5∇φR) =8 _i,j _R^2g_ijR_iR_j(w· _R^5∇ _R)+8 _i,j g_ij[R_iR_j, _R^2](w· _R^5∇ _R) where the first equality is the Lean code actual_flux_eq_canonicalCutoffFlux, the second equality is contained in the Lean code multiplier_r_eq_weight_deriv, as well as the code in cutoffTest and cutoffTest_flux_identity and the third equality uses the Lean codes given by the Lean theorem pressurePair_decomposition and norm_cutoff_pressurePair_le_local_commutator. Both the NL proof and Lean proof then attempt to bound the first term in (3.6) and (3.7) respectively1111 11 We 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 an L3/2L^3/2 bound on the first term. It uses Hölder’s inequality to show that φR4gij∈L3/2 _R^4g_ij∈ L^3/2 and the L3/2→L3/2L^3/2→ L^3/2 boundedness of the Riesz transforms (which is established by citing [53]) to get a bound of the form ‖RiRj(φR4gij)‖3/2⩽C‖φR4gij‖3/2⩽C′(‖φR4w‖6+1)‖w‖2⩽C′(BR+1)\|R_iR_j( ^4_Rg_ij)\|_3/2 C\| ^4_Rg_ij\|_3/2 C (\| ^4_Rw\|_6+1)\|w\|_2 C (B_R+1), where C,C′,C′C,C ,C are all (potentially different) constants that can depend on T. By contrast, the Lean proof does not rely on the above citation[53]. Instead, it begins by using Hölder’s inequality (with Hölder conjugates 66 and 6/56/5) to obtain |∫φR2gijRiRj(w⋅φR5∇φR)|⩽∥φR2gij∥6/5∥RiRj(w⋅φR5∇φR)∥6. | _R^2g_ijR_iR_j(w· _R^5∇ _R) | \| _R^2g_ij\|_6/5\|R_iR_j(w· _R^5∇ _R)\|_6. We will first look at how the Lean argument bounds the right hand term ∥RiRj(w⋅φR5∇φR)∥6\|R_iR_j(w· _R^5∇ _R)\|_6 (as in the lean code lpNorm_six_rieszTest_le and riesz_rTest_bound). First, a Sobolev embedding theorem (bounding the L6L^6 norm by a multiple of the L2L^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. Next, an interchange of derivatives with the Riesz transform (which comes from the Fourier multipliers) as stated in both pderiv_rieszTest and partial_rieszTest is employed to move the gradient operator inside the transform. Finally, the argument uses the boundedness of the Riesz operators from Schwartz functions in L2L^2 to functions in L2L^2 (which follows easily from considering the Fourier multipliers of these operators) as in each of integral_norm_sq_rieszTest_le, lpNorm_two_fderiv_rieszTest_le and rieszTest_memLp_and_l2_bound. 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, \|R_iR_j(w· _R^5∇ _R)\|_6 C\|∇ R_iR_j(w· _R^5∇ _R)\|_2 C \|R_iR_j∇(w· _R^5∇ _R) \|_2 C \|∇(w· _R^5∇ _R)\|_2, where C is a constant from the Sobolev inequality and C′C is another constant. In norm_fderiv_r_le_raw, the Lean proof then bounds (using the product rule), for x∈ℝ3x ^3 (and fixing the time parameter) ∥∇(w⋅φR5∇φR)(x)∥ℓ2⩽ \|∇(w· _R^5∇ _R)(x)\|_ _2 φR5(x)‖∇φR(x)‖ℓ2‖∇w(x)‖op+φR5‖∇2φR(x)‖op‖w(x)‖ℓ2 \, ^5_R(x)\|∇ _R(x)\|_ _2\|∇ w(x)\|_op+ _R^5\|∇^2 _R(x)\|_op\|w(x)\|_ _2 +5φR(x)4‖∇φR(x)‖ℓ22‖w(x)‖ℓ2. +5 _R(x)^4\|∇ _R(x)\|^2_ _2\|w(x)\|_ _2. Some further simplification is done (see for example norm_fderiv_r_le_amplitude), but ultimately this expression leads to the AR/R+1/R2A_R/R+1/R^2 term present in (3.5). When φR(x) _R(x) was defined, it was done so that φR(x)∈[0,1] _R(x)∈[0,1], ‖∇φR(x)‖ℓ2⩽C/R\|∇ _R(x)\|_ _2 C/R and ‖∇2φR(x)‖op⩽C2/R2\|∇^2 _R(x)\|_op C_2/R^2. The ARA_R term comes from moving φR4 _R^4 inside the norm in ‖∇w(x)‖op\|∇ w(x)\|_op. Finally, we note that the BR1/2+1B_R^1/2+1 term that appears in the Lean statement (3.5) comes from using the definition of gij=wiwj+wiuj+uiwjg_ij=w_iw_j+w_iu_j+u_iw_j to bound ‖φR2gij‖6/5\| _R^2g_ij\|_6/5. Indeed, |φR2gij|⩽2|u||w|+|φRw|2| _R^2g_ij| 2|u||w|+| _Rw|^2 is established pointwise1212 12 Technically, the Lean theorem norm_weighted_tensorDiff_le establishes the result |s2gij|⩽2|u||w|+|sw|2|s^2g_ij| 2|u||w|+|sw|^2 for any 0⩽s⩽10 s 1, which can then be applied with s=φR(x)s= _R(x) for each x. in norm_weighted_tensorDiff_le. The Lean proof bounds ∥|φRw|2∥6/5⩽∥φRw∥12/52 | _Rw|^2 _6/5 _Rw _12/5^2, and then an interpolation inequality cutoff_interpolation_twelve_fifths is used to get (3.8) ‖φRw‖12/5⩽‖w‖23/4‖φR4w‖61/4⩽CBR1/4.\| _Rw\|_12/5 \|w\|_2^3/4\| ^4_Rw\|_6^1/4 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 gives ‖|u||w|‖6/5⩽‖u‖3‖w‖2⩽C\||u||w|\|_6/5 \|u\|_3\|w\|_2 C. This argument is also distinct from the NL proof, as no 12/512/5 interpolation like the one present in (3.8) is contained in the proof of Lemma 10.5. Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations. Thus, a pertinent question becomes: are there more examples of mistranslations, and how can one find them in the most efficient way? For a preliminary answer to this question, the reader may consult the following experiment (click to view) aimed at finding other mistranslations in OpenAI’s Navier-Stokes proof. 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 ℝ3R^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, 16, 34, 21, 12, 13, 2, 19, 17]. 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 translation X′X of an NL theorem X and an alleged NL proof Y of X. while no proof of X′X has been verified do The AI revises Y′Y using Y as a guide (that is, the AI attempts a ‘translation’ of Y into Y′Y ) The AI checks if Y′Y is a valid Lean proof of X′X . end while Output: the verified proof Y′Y . The acceptance criterion tests whether Y′Y proves X′X in Lean. It does not check whether the reasoning in Y has 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. Remark 3.5 (Why AI cannot just translate the correct Lean proof back to English/LaTeX). It is natural to ask whether these mistranslation issues could be avoided by simply back-translating the produced Lean proof into NL and comparing with the original NL proof. It then remains, however, to establish both that the back-translation semantically faithfully represents the formal proof, and that its reasoning corresponds to the original argument. That is, back-translation requires further checks to ensure correspondence; it does not escape the objections raised in this section. In other words, we reach the same issue of semantic faithfulness not present in the outline for (i) but available only with autoformalisation in (i) above, just going in the reverse direction. In summary, this approach is as difficult as type (i). 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, 27, 30, 8, 59, 38, 39, 43, 44, 56, 45, 60]. For standard background on formal languages, interpretations and deductive systems, see [22, 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,…N=\0,1,2,…\, as in Lean’s Nat. 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) pee∈ℕ\p_e\_e of polynomials in k+1k+1 variables with integer coefficients. Later on, they write down a particular value of e, and define nen_e to be the least natural number n for which pe(n,x1,…,xk)=0p_e(n,x_1,…,x_k)=0 has no solution in natural numbers x1,…,xkx_1,…,x_k. They then define the real number re=1/(ne+1)r_e=1/(n_e+1) and make the claim that it is obvious that (re+1)2=re2+2re+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+2re+1(r_e+1)^2=r_e^2+2r_e+1 is elementary to establish in Lean. The problem is the following: For Lean to prove that (re+1)2=re2+2re+1(r_e+1)^2=r_e^2+2r_e+1, then rer_e must be well-defined as a rational number. In particular, it must be established whether or not there exists an n such that pe(n,x1,…,xk)=0p_e(n,x_1,…,x_k)=0 has no natural-number solution x1,…,xkx_1,…,x_k. This issue causes an ambiguity: can Example 4.1 be faithfully translated to Lean at all? The answer is as follows: yes, if rer_e is well defined, and no if rer_e is not well defined (when nen_e does not exist). An AI autoformaliser aiming to translate Example 4.1 preserving the semantics is faced with the problem of resolving this ambiguity. If rer_e is not well-defined, the AI autoformaliser should not attempt to translate in order to make Lean accept the translation. Remark 4.2 (A semantic preserving AI autoformaliser must refrain from translating in certain cases). Note that if the AI autoformaliser attempts to ‘translate’ Example 4.1 when rer_e is not well defined – and Lean accepts the ‘translation’ – the ‘translation’ cannot be semantically faithful, it must be a mistranslation. This begs the following question: Can an AI autoformaliser resolve the ambiguity in Example 4.1 in general? That is, given e∈ℕe , can an AI autoformaliser determine when rer_e is well defined? The answer to this problem comes from Hilbert’s 10th problem [35] when k⩾9k 9: No, such an AI autoformaliser can never exist, even if one could solve the Halting problem. See Appendix A and Theorem A.3 for a detailed explanation of this statement. Example 4.1 shows why semantic preservation in mathematics is hard. In general, an AI cannot determine when a statement is ambiguous – and thus cannot be translated – and when a statement is not ambiguous and can be faithfully translated. Moreover, the above result can be strengthened and informally stated as follows: Providing semantically faithful AI autoformalisation is harder than any computational problem. See Appendix A.2.1 for a precise statement. Example 4.3 (A natural attempt to resolve Example 4.1). 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 above: Input: Example 4.1 and e∈ℕe (recall that e uniquely defines the claim in Example 4.1). while no translation of Example 4.1 has been verified by Lean do The AI revises an attempted translation Y′Y of Example 4.1 into Lean. The AI checks if Y′Y is accepted by Lean. end while Output: the accepted translation Y′Y . At face value, it seems like this methodology would only accept a translation when nen_e is defined, and thus all choices of e for which the claim that (re+1)2=re2+2re+1(r_e+1)^2=r_e^2+2r_e+1 in Example 4.1 is a true unambiguous statement would ultimately be resolved. 4.2. Why the algorithm in Example 4.3 cannot solve the problem There is once again a problem with this approach. The AI could easily produce an attempted translation Y′Y which uses a Lean definition that supplies a default value, when nen_e does not exist, in its proof that (re+1)2=re2+2re+1(r_e+1)^2=r_e^2+2r_e+1. In particular, for a fixed e∈ℕe , write for n∈ℕn the predicate Be(n)B_e(n) as follows: (4.1) Be(n)⟺∀(x1,…,xk)∈ℕk,pe(n,x1,…,xk)≠0.B_e(n)\; \;∀\,(x_1,…,x_k) ^k, p_e(n,x_1,…,x_k)≠ 0. With this predicate, a ‘translation’ of Example 4.1 in the case where k=2k=2 and (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 of e and thus pep_e. In particular, suppose an AI suggested the following ‘translation’ Y′Y of Example 4.1 into Lean: ⬇ def p_e (n x1 x2 : Int) : Int := x1 + x2 - n def B_e (n : Nat) : Prop := forall (x1 x2 : Nat), p_e (n : Int) (x1 : Int) (x2 : Int) != 0 noncomputable def n_e : Nat := sInf n : Nat | B_e n noncomputable def r_e : Rat := 1 / (n_e + 1) theorem example_3_1 : (r_e + 1) 2 = r_e 2 + 2 * r_e + 1 := by ring Here sInf returns the least element of a nonempty set of natural numbers, but returns 00 when the set is empty; see Nat.sInf_def and Nat.sInf_empty in [57]. Thus, if no natural number satisfies BeB_e, the code silently assigns ne=0n_e=0 and re=1r_e=1. However, for the polynomial in (4.2), every n∈ℕn admits the natural-number root (x1,x2)=(n,0)(x_1,x_2)=(n,0), since pe(n,n,0)=n+0−n=0p_e(n,n,0)=n+0-n=0. Hence, Be(n)B_e(n) is false for every n, and n∈ℕ:Be(n)=∅.\n :B_e(n)\= . 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 using sInf; Warning: With the above ‘translation’ Y′Y (in the grey box) the algorithm in Example 4.3 will halt and produce a mistranslation. In this case the semantics of the definition of nen_e have been completely changed. Indeed, if the above ‘translation’ into Lean had actually been semantically faithful, it would have implied that there is an n∈ℕn such that pe(n,x1,x2)=x1+x2−np_e(n,x_1,x_2)=x_1+x_2-n has no roots (x1,x2)∈ℕ2(x_1,x_2) ^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 reiterates the message in §4.2: 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 and Theorem A.3. 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]. These claims were, however, swiftly refuted by the Lean community in the discussion quoted below [32]. (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.’ (i) 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.’ (i) 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]. 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 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, 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. Remark 5.1. The crucial issue is that – as pointed out in Remark 4.2 – a semantic preserving AI formaliser must refrain from doing a translation in certain cases. The example in §4 and Theorem A.3 show that no AI autoformaliser can determine when it must refrain from translating and when it should translate. Thus, the big question is how to design AI autoformalisers that preserve semantics. Current AI based approaches are typically based on the ‘guessing and checking’ algorithm in Example 4.3, which is doomed to mistranslate because no AI can determine when it should or should not provide a suggested translation Y′Y (recall the notation from Example 4.3). 5.2. Semantics-preserving autoformalisation and the future of AI in mathematics The Leiden Declaration from June 2026 [1] 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] 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. (i) 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 A The 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, explaining why no AI can resolve it for all e∈ℕe . The basic framework we use is that of the Solvability Complexity Index (SCI) hierarchy initiated in [28] and further developed in [7, 6, 15, 25, 14, 4]. The SCI hierarchy is closely connected to S. Smale’s [49, 50] program on the foundations of computational mathematics and scientific computing. This program motivated the early investigations of polynomial root-finding by C. McMullen [36, 37, 51] and P. Doyle & C. McMullen [20]. 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]. Although some of the mathematics underlying the SCI hierarchy can be traced back to K. Gödel [26] and A. Turing [58], 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, 14] 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 Ω (where each element of Ω specifies a problem instance), a metric space (ℳ,d)(M,d) of candidate solutions, and a solution map Ξ:Ω⇉ℳ : 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 Λ specifying which information about the problem instances may actually be accessed by an algorithm. This will not be relevant 1313 13 For the computational problems discussed in this appendix, each problem instance in Ω is specified entirely by a single natural number, so Λ amounts to containing only an identity map. for this appendix. A computational problem is often specified simply as Ξ,Ω\ , \, when ℳM and Λ are understood. The SCI of a computational problem is defined as the minimal number of limits 1414 14 This is formalised by the notion of towers of algorithms. required to solve that problem (+∞+∞ if no finite number of limits suffices). The mainstay classes of the hierarchy are the Δmα _m^α classes, which are defined for each m⩾0m 0. Here α is related to the model of computation, as explained below. Informally, we have the following description. Given a collection C of computational problems: (i) Δ0α ^α_0 is the set of problems that can be computed in finite time, so that they satisfy SCI =0=0; (i) Δ1α ^α_1 is the set of problems that can be computed using one limit (they satisfy SCI ⩽1 1) with control of the error, i.e., there is a sequence of algorithms Γn\ _n\ with d(Γn(A),Ξ(A))⩽2−n,∀A∈Ωd( _n(A), (A)) 2^-n,\,∀ A∈ ; (i) Δ2α ^α_2 is the set of problems that can be computed using one limit (again SCI ⩽1 1) but sans error control, i.e., there is a sequence of algorithms Γn\ _n\ with limn→∞Γn(A)=Ξ(A),∀A∈Ω _n→∞ _n(A)= (A),\,∀ A∈ ; (iv) Δm+1α ^α_m+1, for m⩾1m 1, is the set of problems that can be computed by using m limits, (in other words, SCI ⩽m m), i.e., there is a family of algorithms Γnm,…,n1\ _n_m,…,n_1\ with limnm→∞…limn1→∞Γnm,…,n1(A)=Ξ(A),∀A∈Ω. _n_m→∞… _n_1→∞ _n_m,…,n_1(A)= (A),\,∀ A∈ . In general, this hierarchy can only be refined further, beyond these classes, if the metric space ℳ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α⊊…. _0^α _1^α _2^α … ^α_m …. Depending on the collection C of computational problems, however, the hierarchy (A.1) may terminate for a finite m or continue for arbitrary large m. Definition A.1 (The SCI Hierarchy (totally ordered set)). Given the setup above, suppose in addition that ℳ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∈Ω, split ^α_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∈ \, split where ↗ and ↘ denotes convergence from below and above respectively, as well as, for m∈ℕm , Σ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∈Ω. split ^α_m+1&=\\ , \∈ _m+2^α\ |\ ∃\ height m+1 tower \ _n_m+1,…,n_1\ for \ , \ s.t. _n_m+1(A) (A)\ \,∀ A∈ \,\\ ^α_m+1&=\\ , \∈ _m+2^α\ |\ ∃\ height m+1 tower \ _n_m+1,…,n_1\ for \ , \ s.t. _n_m+1(A) (A)\ \,∀ A∈ \. split See [6] for the formal definition of the towers of algorithms used to define Σm+1α _m+1^α and Πm+1α _m+1^α 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,1M=\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α @inpgf@ignorespaces _0^αΠ1α @inpgf@ignorespaces _1^αΠ2α @inpgf@ignorespaces _2^αΔ0α @inpgf@ignorespaces _0^αΔ1α @inpgf@ignorespaces _1^αΣ1α∪Π1α @inpgf@ignorespaces _1^α∪ _1^αΔ2α @inpgf@ignorespaces _2^αΣ2α∪Π2α @inpgf@ignorespaces _2^α∪ _2^αΔ3α @inpgf@ignorespaces _3^α⋯ @inpgf@ignorespaces·sΣ0α @inpgf@ignorespaces _0^αΣ1α @inpgf@ignorespaces _1^αΣ2α @inpgf@ignorespaces _2^α====⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ ⊊ Note that the Σ1α _1^α and Π1α _1^α 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, Section 3]. We also use standard facts about the arithmetical hierarchy and oracle computability, for which we refer the reader to [52, Chapter 4]. The α in the Δmα _m^α classes can refer to any model of computation (e.g. the classical Turing model [58] or the Blum-Shub-Smale model [9]). Hereon, we will take α=Aα=A where A refers to the arithmetic model of computation. This means the algorithms are all Turing machines i.e. the classical Turing model. Remark A.2 (SCI hierarchy generalises the arithmetical hierarchy). We note that the arithmetical hierarchy becomes a special case of the SCI hierarchy [6, Proposition A.8]. More precisely, with α=Aα=A and ℳ=0,1M=\0,1\, if we restrict to computational problems asking about membership in a subset of ℕN, we have ΣmA=Σm0 _m^A= _m^0, ΠmA=Πm0 _m^A= _m^0 and ΔmA=Δm0 _m^A= _m^0 for every m⩾0m 0 [6, Proposition A.8]. Here, Σm0 _m^0, Πm0 _m^0 and Δm0 _m^0 are the classical classification classes from the arithmetical hierarchy. We will make use of this fact in the following results. Notation (Reducibility). For sets A,B⊆ℕA,B , we write A⩽mBA _mB if there is a total computable function f:ℕ→ℕf:N such that (∀n∈ℕ)[n∈A⇔f(n)∈B].(∀ n )[n∈ A f(n)∈ B]. In this case we say A is many-one reducible to B, witnessed by f. We write A⩽TBA _TB if there is an oracle Turing machine which, with B on the oracle tape, computes the characteristic function of A. In this case we say A is Turing reducible to B. The Turing degree of a set A⊆ℕA is the set of all C⊆ℕC that simultaneously satisfy A⩽TCA _TC and C⩽TAC _TA. We say A is Σn0 _n^0-complete if A∈Σn0A∈ _n^0 and also C⩽mAC _mA for every C∈Σn0C∈ _n^0. Similarly, A is Πn0 _n^0-complete if A∈Πn0A∈ _n^0 and C⩽mAC _mA for every C∈Πn0C∈ _n^0. We fix an integer-coefficient polynomial pairing function ⟨ , ⟩:ℕ2→ℕ , :N^2 given by ⟨x,y⟩=(x+y)(x+y+1)+2y, for (x,y)∈ℕ2, x,y =(x+y)(x+y+1)+2y, for (x,y) ^2, which is a computable injection, by [41, Section 1, p. 1001]. By iteration, for each n⩾2n 2 we also obtain and hereon fix an n-ary pairing function ⟨ ,…, ⟩:ℕn→ℕ ,..., :N^n , which is also an integer-coefficient polynomial. A.2. Resolving ambiguities is hard Recall the condition defining nen_e in Example 4.1. For an enumeration (pe)e∈ℕ(p_e)_e of integer-coefficient polynomials in the variables n,x1,…,xkn,x_1,…,x_k, write (A.3) Be(n)⇔(∀(x1,…,xk)∈ℕk) pe(n,x1,…,xk)≠0.B_e(n) (∀(x_1,…,x_k) ^k) p_e(n,x_1,…,x_k)≠ 0. Then nen_e is defined to be the least n∈ℕn for which Be(n)B_e(n) holds, provided such an n exists, and is undefined otherwise. Completeness throughout this subsection refers to completeness under many-one reductions. Theorem A.3. Fix k⩾9k 9. For any computable enumeration (pe)e∈ℕ(p_e)_e of all polynomials with integer coefficients in k+1k+1 variables, let BeB_e be as in (A.3). Then the set d:=e∈ℕ:(∃n∈ℕ) Be(n)d:=\e :(∃ n ) B_e(n)\ is Σ20 ^0_2-complete. In particular, no AI can always determine whether the number nen_e specified in Example 4.1 is well-defined, even with an oracle for the Halting problem. Proof. We use the usual μ notation for minimum search [52]. By the assumption that the enumeration e↦pee p_e is computable and the assumption that pep_e has integer coefficients, there exists an algorithm that decides if pe(n,x1,…xk)=0p_e(n,x_1,… x_k)=0 given inputs n,x1,…,xkn,x_1,…c,x_k. The condition defining membership in d is thus given by the quantifiers (∃n∈ℕ)(∀x1∈ℕ)…(∀xk∈ℕ)(∃ n )(∀ x_1 )...(∀ x_k ) over a decidable relation, so we have d∈Σ20d∈ ^0_2. To obtain Σ20 ^0_2-completeness, fix a standard effective enumeration (Pe)e∈ℕ(P_e)_e of all Turing machines. For e,n∈ℕe,n , write Pe(n)↓P_e(n) when Pe(n)P_e(n) halts and Pe(n)↑P_e(n) when Pe(n)P_e(n) does not halt. Recall that a Diophantine set [35] is a set A⊆ℕA that can be represented using a finite number of unknowns, in the sense that there exists an integer s⩾1s 1 and an integer-coefficient polynomial p(n,x1,…,xs)p(n,x_1,...,x_s) in s+1s+1 variables with: n∈A⇔(∃(x1,…,xs)∈ℕs) p(n,x1,…,xs)=0.n∈ A (∃(x_1,…,x_s) ^s) p(n,x_1,…,x_s)=0. The Davis–Putnam–Robinson–Matiyasevich (DPRM) theorem [35] states that the Diophantine sets are precisely the computably enumerable sets. The nine-unknown refinement [31] of the DPRM theorem permits every computably enumerable relation over ℕN to be represented using nine unknowns. Applying this to the computably enumerable set K1=⟨e,n⟩∈ℕ:Pe(n)↓K_1=\ e,n :P_e(n) \, we find there exists a fixed integer-coefficient polynomial q0(n~,x1,…,x9)q_0( n,x_1,...,x_9), where n~ n is a variable, such that ⟨e,n⟩∈K1 e,n ∈ K_1 if and only if q0(⟨e,n⟩,x1,…,x9)q_0( e,n ,x_1,...,x_9) admits a root (x1,…,x9)∈ℕ9(x_1,...,x_9) ^9. Defining the polynomial q(e,n,x1,…,x9):=q0(⟨e,n⟩,x1,…,x9)q(e,n,x_1,...,x_9):=q_0( e,n ,x_1,...,x_9), we have for each e,n∈ℕe,n : Pe(n)↓⟺(∃(x1,…,x9)∈ℕ9) q(e,n,x1,…,x9)=0.P_e(n) (∃(x_1,…,x_9) ^9) q(e,n,x_1,…,x_9)=0. For k>9k>9, regard q as independent of the additional variables x10,…,xkx_10,…,x_k. Define the binary predicate W⊆ℕ2W ^2 by W(e,j)⇔pj(n,x1,…,xk)≡q(e,n,x1,…,xk),W(e,j) p_j(n,x_1,...,x_k)≡ q(e,n,x_1,...,x_k), where ≡ denotes that the two polynomials, whose variables are n,x1,…,xkn,x_1,...,x_k, have coinciding coefficients; given e and j this is decidable. Since (pe)e∈ℕ(p_e)_e enumerates all integer-coefficient polynomials in k+1k+1 variables, the function t(e):=μj[W(e,j)]t(e):=μ j[W(e,j)] is well-defined and computable. By the definitions of d and q, we have t(e)∈d⟺(∃n∈ℕ) Pe(n)↑t(e)∈ d (∃ n ) P_e(n) In other words, t is a computable many-one reduction from NTOT:=e∈ℕ:(∃n∈ℕ) Pe(n)↑NTOT:=\e :(∃ n ) P_e(n) \ to d. Since NTOTNTOT is Σ20 ^0_2-complete, so is d. By Post’s theorem [52, Chapter 4], we have d⩽T∅′⇔d∈Δ20d _T d∈ _2^0. Since d∈Σ20d∈ _2^0, we have d⩽T∅′⇔d∈Π20d _T d∈ _2^0. But whenever a set belongs to Π20 _2^0 so too does any set that (many-one) reduces to it; thus if d∈Π20d∈ _2^0 then by Σ20 _2^0-completeness we would have Σ20⊆Π20 _2^0 _2^0, contradicting strictness of the arithmetical hierarchy [52, Corollary 4.2.3, p. 85]. Consequently, we cannot have d⩽T∅′d _T . Since d is exactly the set of e for which nen_e in Example 4.1 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. We first generalise the predicate Be(n)B_e(n). For l⩾2l 2, consider an enumeration (pe)e∈ℕ(p_e)_e of integer-coefficient polynomials in the l−1+kl-1+k variables n,z2,…,zl−1,x1,…,xk.n,z_2,…,z_l-1,x_1,…,x_k. Let QjQ_j denote ∃ for odd j and ∀ for even j. We omit z2,…,zl−1z_2,…,z_l-1 when l=2l=2. Define Be(l)(n)B^(l)_e(n) by the following two cases. For even l, again omitting z2,…zl−1z_2,… z_l-1 when l=2l=2, we have (A.4a) Be(l)(n)⇔ B^(l)_e(n) (Q2z2∈ℕ)⋯(Ql−1zl−1∈ℕ)(∀(x1,…,xk)∈ℕk) (Q_2z_2 )\;·s\;(Q_l-1z_l-1 )\;(∀(x_1,…,x_k) ^k) pe(n,z2,…,zl−1,x1,…,xk)≠0, p_e(n,z_2,…,z_l-1,x_1,…,x_k)≠ 0, For odd l⩾3l 3, (A.4b) Be(l)(n)⇔ B^(l)_e(n) (Q2z2∈ℕ)⋯(Ql−1zl−1∈ℕ)(∃(x1,…,xk)∈ℕk) (Q_2z_2 )\;·s\;(Q_l-1z_l-1 )\;(∃(x_1,…,x_k) ^k) pe(n,z2,…,zl−1,x1,…,xk)=0. p_e(n,z_2,…,z_l-1,x_1,…,x_k)=0. Note that (using the same k and polynomial enumeration) Be(2)(n)B^(2)_e(n) is Be(n)B_e(n). As in [52], we write ∅(0)=∅ ^(0)= and ∅(j+1) ^(j+1) for the Halting problem relative to ∅(j) ^(j), for j∈ℕj . Theorem A.4 (Presupposition resolution at arbitrary arithmetical levels). Fix l⩾2l 2 and k⩾9k 9. Fix a computable enumeration (pe)e∈ℕ(p_e)_e of all integer-coefficient polynomials in l−1+kl-1+k variables, and let Be(l)B^(l)_e be as in (A.4). Then dl:=e∈ℕ:(∃n∈ℕ) Be(l)(n)d_l:=\e :(∃ n ) B^(l)_e(n)\ is Σl0 _l^0-complete. In particular, no algorithm can always determine whether the least n for which Be(l)(n)B^(l)_e(n) holds is well-defined, even with an oracle for ∅(l−1) ^(l-1). Proof. Fix l⩾2l 2. By its definition, Be(l)(n)B^(l)_e(n) is a Πl−10 ^0_l-1 predicate. Indeed, it begins with l−2l-2 alternating quantifiers - the first being a universal quantifier – and the subsequent k quantifiers are all either existential or all universal; the affected predicate therein, namely pe(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∈ _l^0. For Σl0 _l^0-hardness, let A⊆ℕA be any Σl0 _l^0 set. By definition, there exists a computable relation R⊆ℕl+1R ^l+1 such that (A.5) a∈A⇔(Q1z1∈ℕ)⋯(Qlzl∈ℕ) R(a,z1,…,zl).a∈ A (Q_1z_1 )\;·s\;(Q_lz_l ) R(a,z_1,…,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,…,z_l-1) cases(∃ z_l ) R(a,z_1,…,z_l),& for l odd;\\ (∃ z_l ) R(a,z_1,…,z_l),& for l even. cases By the nine-unknown refinement of the DPRM theorem [35, 31] applied to the computably enumerable set ⟨a,z1,…,zl−1⟩∈ℕ:C(a,z1,…,zl−1)\ a,z_1,...,z_l-1 :C(a,z_1,...,z_l-1)\, there exists a fixed integer-coefficient polynomial q0(n~,x1,…,x9)q_0( n,x_1,...,x_9), where n~ 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) (∃(x_1,...,x_9) ^9) q_0( a,z_1,...,z_l-1 ,x_1,....,x_9)=0. Defining the polynomial q(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( a,z_1,...,z_l-1 ,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,…,z_l-1) (∃(x_1,…,x_9) ^9) q(a,z_1,…,z_l-1,x_1,…,x_9)=0. If l is odd, this representation permits (A.5) to be expressed as a∈A⇔ a∈ A (∃z1∈ℕ)⋯(∀zl−1∈ℕ)(∃(x1,…,x9)∈ℕ9) (∃ z_1 )\;·s\;(∀ z_l-1 )(∃(x_1,...,x_9) ^9) q(a,z1,…,zl−1,x1,…,x9)=0. q(a,z_1,...,z_l-1,x_1,...,x_9)=0. If l is even, negation of the defining condition for C gives (∀zl∈ℕ) R(a,z1,…,zl)⇔(∀(x1,…,x9)∈ℕ9) q(a,z1,…,zl−1,x1,…,x9)≠0,(∀ z_l ) R(a,z_1,…,z_l) (∀(x_1,…,x_9) ^9) q(a,z_1,…,z_l-1,x_1,…,x_9)≠ 0, so that (A.5) can be expressed as a∈A⇔ a∈ A (∃z1∈ℕ)(∀z2∈ℕ)⋯(∃zl−1∈ℕ)(∀(x1,…,x9)∈ℕ9) (∃ z_1 )(∀ z_2 )\;·s\;(∃ z_l-1 )(∀(x_1,...,x_9) ^9) q(a,z1,…,zl−1,x1,…,x9)≠0. q(a,z_1,...,z_l-1,x_1,...,x_9)≠ 0. Consequently, regardless of the parity of l, we have replaced the final quantification (Qlzl∈ℕ)(Q_lz_l ) in (A.5) sans appending an additional quantifier alternation. When k>9k>9, we regard q as independent of the additional variables x10,…,xkx_10,…,x_k. Define the binary predicate W⊆ℕ2W ^2 by W(a,j)⇔pj(n,z2,…,zl−1,x1,…,xk)≡q(a,n,z2…,zl−1,x1,…,xk),W(a,j) p_j(n,z_2,...,z_l-1,x_1,...,x_k)≡ q(a,n,z_2...,z_l-1,x_1,...,x_k), where ≡ denotes that the two polynomials, whose variables are n,z2,…,zl−1,x1,…,xkn,z_2,...,z_l-1,x_1,...,x_k, have coinciding coefficients; given a and j this is decidable. Since (pe)e∈ℕ(p_e)_e enumerates all integer-coefficient polynomials in l−1+kl-1+k variables, the function t(a):=μj[W(a,j)]t(a):=μ j[W(a,j)] is well-defined and computable. The preceding equivalences imply that a∈A⇔t(a)∈dl.a∈ A t(a)∈ d_l. That is, A⩽mdlA _md_l, establishing Σl0 ^0_l-completeness of dld_l. By definition of dld_l, the least n∈ℕn satisfying Be(l)(n)B^(l)_e(n) exists exactly when e∈dle∈ d_l. By Post’s theorem [52], we have dl⩽T∅(l−1)⇔dl∈Δl0d_l _T ^(l-1) d_l∈ _l^0. Since dl∈Σl0d_l∈ _l^0, this becomes dl⩽T∅(l−1)⇔dl∈Πl0d_l _T ^(l-1) d_l∈ _l^0. But whenever a set belongs to Πl0 _l^0 so too does any set that (many-one) reduces to it; thus if dl∈Πl0d_l∈ _l^0, then by Σl0 _l^0-completeness we would have Σl0⊆Πl0 _l^0 _l^0, contrary to the strictness of the arithmetical hierarchy. Consequently, we cannot have dl⩽T∅(l−1)d_l _T ^(l-1). ∎ When we use the same k and the same polynomial enumeration, the case l=2l=2 gives Be(2)(n)=Be(n)B_e^(2)(n)=B_e(n) for every n∈ℕn , so that d2=d_2=d, which recovers Theorem A.3. Moreover, for every l⩾2l 2, the complement of dld_l is Πl0 _l^0-complete, and dld_l has the Turing degree of ∅(l) ^(l) (since ∅(l) ^(l) is Σl0 _l^0-complete by Post’s Theorem [52]). For each fixed l⩾2l 2 and e∈ℕe , let ne(l)n^(l)_e be the least n for which Be(l)(n)B^(l)_e(n) holds, and define re(l)=1/(ne(l)+1)r^(l)_e=1/(n^(l)_e+1). Both ne(l)n^(l)_e and re(l)r^(l)_e are left undefined if there is no such n. Replacing nen_e and rer_e in Example 4.1 by ne(l)n^(l)_e and re(l)r^(l)_e, respectively, gives the same least-number construction. The displayed identity (re(l)+1)2=(re(l))2+2re(l)+1(r^(l)_e+1)^2=(r^(l)_e)^2+2r^(l)_e+1 remains elementary to establish, while as e varies, deciding whether the stated definition of re(l)r^(l)_e refers to a well-defined number is a Σl0 ^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, Definitions 5.2–5.6] for the formal definition. The input space Ω is ℕN and the output space is ℳ=0,1M=\0,1\ with the discrete metric. A tower of height h⩾1h 1 for a function Ξ:Ω→0,1 : →\0,1\ is given by a bottom-level computable function Γ:Ω×ℕh→0,1 : ×N^h→\0,1\ that satisfies Ξ(e)=lims1→∞⋯limsh→∞Γ(e,s1,…,sh), (e)= _s_1→∞·s _s_h→∞ (e,s_1,…,s_h), for each e∈Ωe∈ . In particular, each successive limit exists (for every fixed choice of the outer indices). An arithmetical tower of height zero for Ξ is simply a computable function Γ:Ω→0,1 : →\0,1\ with Γ=Ξ = . Given any function Ξ:Ω→0,1 : →\0,1\, we define SCIA(Ξ)SCI_A( ) to be the least h⩾0h 0 for which there is an arithmetical tower of height h for Ξ ; we define SCIA(Ξ)=+∞SCI_A( )=+∞ when no such tower exists. We also define Δh+1A ^A_h+1 to denote the class of problems Ξ with SCIA(Ξ)⩽hSCI_A( ) h, for each h⩾1h 1. Corollary A.5 (Unbounded SCI for presupposition resolution). For each l⩾2l 2, define Ξdl:Ω→0,1 _d_l: →\0,1\ by Ξdl(e)=1 _d_l(e)=1 if and only if e∈dle∈ d_l. With k⩾9k 9 and the enumeration in Theorem A.4, we have SCIA(Ξdl)=lfor every l⩾2.SCI_A( _d_l)=l every l 2. Equivalently, the decision problem for the set dld_l lies in Δl+1A∖ΔlA ^A_l+1 ^A_l. Proof. Fix l⩾2l 2. Since dl∈Σl0d_l∈ _l^0, we have dl∈ΣlAd_l∈ _l^A (as the SCI hierarchy generalises the arithmetical hierarchy, as discussed above). This means SCIA(Ξdl)⩽lSCI_A( _d_l) l. On the other hand, if SCIA(Ξdl)<lSCI_A( _d_l)<l, then there is an arithmetical tower of height 0⩽h<l0 h<l for Ξdl _d_l. This would give that dl∈Δh+10d_l∈ _h+1^0 (again using that the SCI hierarchy generalises the arithmetical hierarchy) and thus also dl∈Δl0d_l∈ _l^0 since h<lh<l. But dld_l is Σl0 _l^0-complete so cannot lie in Δl0 _l^0 ( else Σl0⊆Πl0 _l^0 _l^0, contrary to strictness of the arithmetical hierarchy [52, Corollary 4.2.3, p. 85]). This means SCIA(Ξdl)⩾lSCI_A( _d_l) l. We conclude that SCIA(Ξdl)=lSCI_A( _d_l)=l, as required. ∎ A.2.1. The problem of resolving ambiguities has SCI =∞=∞ Recall Example 4.1 and Be(n)B_e(n) from (4.1). Recall that the ambiguity in Example 4.1 – whether nen_e is well defined or not – was caused by the following question: ‘Is n∈ℕ:Be(n)\n :B_e(n)\ empty or not? Note that we could have made Example 4.1, and the definition of nen_e, more general yielding an ambiguity caused by the question: ‘Is n∈ℕ:Be(l)(n)\n :B^(l)_e(n)\ empty or not? Here, Be(l)(n)B^(l)_e(n) is defined for integers l⩾2l 2 in (A.4). 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 each e∈ℕe and l⩾2l 2. However, by Corollary A.5 – for each fixed l – this problem has SCI =l=l. Hence, the problem of answering the above question for all e∈ℕe and l⩾2l 2 has SCI =∞=∞. 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. Remark A.6. The requirement that k⩾9k 9 represents the current state of literature on the DPRM theorem; this is an active area of research with a recent refinement [54] lowering the bound from k⩾11k 11 to k⩾10k 10 in the case where x∈ℤkx ^k (in our theorem and proof we work with x∈ℕkx ^k, where the best known bound for Σ20 _2^0 completeness of d is k⩾9k 9). References [1] J. Alper et al. Leiden Declaration on Artificial Intelligence and Mathematics, 2026. 2 June 2026. doi: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. [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. [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 I: 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 in Lt1Cx1,ϵ∩Lt∞Lx2L^1_tC_x^1,ε∩ L^∞_tL_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 for C1,αC^1,α solutions to the incompressible Euler equations on ℝ3R^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, the n-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. [32] Lean community. Atlas (Meta). Zulip discussion in the Autoformalization channel, 2026. Discussion thread. 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. [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. [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, 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. In Acta numerica, 1997, volume 6 of Acta Numer., pages 523–551. Cambridge Univ. Press, Cambridge, 1997. [51] S. Smale. The work of Curtis T McMullen. In Proceedings 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. [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 for Nat.sInf_def and Nat.sInf_empty. 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.