Kevin Buzzard (@xenaproject) has just launched his five-year project to formalize the proof of Fermat's Last Theorem #FLT in #Lean4: see his blog post at https://leanprover-community.github.io/blog/posts/FLT-announcement/ and the blueprint at https://imperialcollegelondon.github.io/FLT/blueprint/index.html . As discussed in the blog post, the target is to be able to reduce the proof of FLT to "claims which were known to mathematicians by the end of the 1980s". Hopefully this project will develop many of the foundational theories of modern number theory, and also provide real-world lessons about how to organize a genuinely large-scale formalization project, in particular whether the project is sufficiently modular that many people can make meaningful contributions to the project without having to master all the mathematical prerequisites needed to understand the proof of FLT.
The difference between FFI design in #haskell in #lean4
In Haskell all the heavy lifting happens in haskell. I.e. you allocate and free memory, peek and poke data from/to C structures etc. As a result, C part known almost nothing about haskell.
In lean it's other way around: C functions get lean objects as arguments, convert them into C data, create new lean objects and return them. As a result, lean's C API is big, complicated and unstable.
I wrote a C0 (subset of C) to Wasm compiler in #Lean4 that can be ran in the browser. You can try it out here: https://theabrick.com/c0/
While the end goal is to completely verify it, only part of that is completed as of right now.
I am also working on tooling and other somewhat tangential features. One of these tools that I wrote that was particularly cool/interesting is a Lean inductive definition to LaTeX'd inference rule converter.
Essentially you can encode inference rules in Lean (see first image) and with minimal configuration, the tool will output a corresponding typeset inference rule (see second picture). I've posted the static semantics that I've been able to generate for C0 so far here: https://theabrick.com/c0/statics.pdf
I see this having a couple of benefits. Number one being that I think it is much easier to double check inference rules for correctness than to read lines of code (and likewise the reader doesn't need to know Lean to understand the rules). I also find typesetting inference rules to somewhat difficult and tedious, but writing them in Lean is much easier (likewise this also removes potential typos between the two different versions of the rules).
I still need to flesh out and cleanup the converter before I would consider it generally usable. I just couldn't resist showing it off right now though : ) Hopefully I will have it finished soon!
The #Lean4 project to formalize the proof of the Polynomial Freiman-Ruzsa conjecture has succeeded after three weeks, with the dependency graph completely covered in a lovely shade of green: https://teorth.github.io/pfr/blueprint/dep_graph_document.html , and the Lean compiler reporting that the conjecture follows from standard axioms.
The #Lean4 formalization of the proof of the PFR conjecture has uncovered an extremely minor error in the paper itself; see https://github.com/teorth/pfr/pull/53 . The issue is that in Lemma 5.2, the hypothesis that (G) is a vector space over (F_2) (which is actually true throughout the paper) was omitted in the statement of this lemma, but is a needed hypothesis (in the proof one wants to rewrite (X-Y-Z) as (X+Y+Z), and this is only possible in characteristic 2). Thanks to Floris van Doorn for uncovering this issue. The fix is immediate (just put this omitted hypothesis back in), but it does show (for the second time, in my case) that formalization can uncover (small) errors in the original proof being formalized.
Finally completed the #Lean4 formalization of my Maclaurin-type inequality paper at https://github.com/teorth/symmetric_project . Specifically, if (s_k) denotes the (k^{th}) symmetric mean of (n) real numbers, the inequality
[ |s_l|^{1/l} \leq C \max ( (l/k)^{1/2} |s_k|^{1/k} ] [, (l/(k+1))^{1/2} |s_{k+1}|^{1/(k+1)})]
is established for ( 1 \leq k < l \leq n). In fact as a byproduct of the formalization I now get the explicit value (C = 160 e^7) for the constant (C).
Was surprisingly satisfied to get the blue "No goals" message in the Lean infoview.
In the end it took perhaps a hundred hours of effort, spread out over a month. It was about 20x slower to formalize this paper than it was to write it in LaTeX. Initially this was due to my own inexperience with Lean, though near the end I was hitting the limitations of existing Lean tools, as well as the speed of the Lean compiler (though this was in part due some inefficiencies in my coding). However, Lean is a living language still in development, and several helpful people provided me during this project with upgraded Lean tactics (such as an improved positivity tactic that could handle finite sums and products, a rify tactic to easily convert natural number inequalities to real number ones, and a rw_ineq tactic to implement the rewriting of inequalities I had noted was previously missing). These definitely helped expedite the formalization process, particularly in the last week or so. 1/3
I've been really enjoying Terence Tao's live-tooting his process of learning #Lean4. To do so, he's been formalizing a recent paper, which is rad way to learn a language.
However, if you are like me, you maybe have found this to be slightly inaccessible bc of being unfamiliar with lean. Luckily, I re-found this splendid "game" for learning to use it (or lean 3 anyway). Its just an absolute delight https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
My #Lean4 formalization project is reaching the final stretch; roughly speaking only the final two pages of the final section of my paper https://arxiv.org/pdf/2310.05328.pdf need to be formalized, and this is "just" manipulation of various inequalities involving powers and a maximum ( \max_{k'=k,k+1} ) operation, plus some routine estimation. My formalization multiplier for this type of math seems to be about 20x or so currently: each line in the paper such as "this can be rearranged as" is currently taking me about 20 minutes to formalize properly.
But I am belatedly realizing some ways to make things a bit more efficient. Firstly, I am realizing that creating even very simple lemmas can be helpful. In particular, I just created a lemma to the effect that if (a,b,c,d,e) are positive reals with ( a \leq bc ) and ( dc \leq e ), then ( ad \leq be ). This has a two line proof in Lean, but this type of "move" occurs multiple times in my argument and was becoming tedious to write out (particularly because in my application the quantities (a,b,c,d,e) are themselves rather complicated). These "mid-level" lemmas would be considered too trivial to even mention in a "high-level" proof of the form one sees in Mathematical English, but are a useful bridge between the "low-level" tools one is provided in Lean (e.g., the fact that if (a \leq b) and ( d \geq 0), then ( ad \leq bd)) and the slightly higher level task of concatenating and rearranging more intricate inequalities.
This part of formalization reminds me of unscrambling a Rubik's cube. To solve a cube, it helps to formalize "mid level moves" consisting of a small number of face rotations to achieve targeted tasks.
Finally managed to formalize in #Lean4 the repaired version of the arguments in Section 2 of my paper. It was more tedious than I expected, with each line of proof taking about an hour to formalize. In the first week of my project, the bottleneck was my own ignorance of the syntax and tools available in Lean; but currently the bottleneck was rather the tools themselves, which are not yet as advanced as the tools one might see in a computer algebra package. For instance, in one line of my paper I state that the inequality
[ |s_n|^{-1/n} \leq \max_{k'=k,k+1}] [(2n)^{\frac{1}{2} \log \frac{n-1}{n-k'-1}} (|s_{k'}|/|s_n|)^{1/(n-k')} ]
can be rearranged as
[ |s_n|^{1/n} \leq \max_{k'=k,k+1} ][ (2n)^{\frac{n-k'}{2k'} \log \frac{n-1}{n-k'-1}} |s_{k'}|^{1/k'},]
assuming all denominators are positive. This is a reasonably quick task on pen and paper, and can also be done fairly readily in any standard computer algebra package (perhaps after treating (\max) operators manually). However, while Lean does have very useful automated tools for field identities and linear arithmetic, it does not currently have tools to automatically simplify complex expressions involving exponentials, and instead one has to work step by step with the laws of exponentiation (e.g., ((x^y)^z = x^{yz}), ( x^z/y^z = (x/y)^z), etc.) as well as the other operations appearing above. Each such law is provided by Lean, but sequencing them together is time-consuming.
One step that stumped me for a while was a numerical verification ( 2e - 2 \leq 8(e-2) ). This is immediate from a calculator, but to prove it rigorously I ended up having to use the inequality ( e \geq 1 + 1 + \frac{1}{2!} ).
Terence Tao live-blogging his discovery of a small but non-trivial mistake while formalizing one of his theorems in order to learn #Lean4 is a pretty epic moment in #PL posting history imo
As a consequence of my #Lean4 formalization project I have found a small (but non-trivial) bug in my paper! While in the course of formalizing the arguments in page 6 of https://arxiv.org/pdf/2310.05328.pdf , I discovered that the expression ( \frac{1}{2} \log \frac{n-1}{n-k-1} ) that appears in those arguments actually diverges in the case ( n=3, k=2)! Fortunately this is an issue that is only present for small values of (n), for which one can argue directly (with a worse constant), so I can fix the argument by changing some of the numerical constants on this page (the arguments here still work fine for ( n \geq 8), and the small (n) case can be handled by cruder methods).
Enclosed is the specific point where the formalization failed; Lean asked me to establish ( 0 < n - 3 ), but the hypothesis I had was only that ( n > 2 ), and so the "linarith" tactic could not obtain a contradiction from the negation of ( 0 < n-3).
I'll add a footnote in the new version to the effect that the argument in the previous version of the paper was slightly incorrect, as was discovered after trying to formalize it in Lean.
I've been pondering how to work with O() notation #Lean4. Lean4 does already supports a version (f = O(g) ) of this notation when comparing two functions (f,g) of some parameter (n) (and one also needs to specify a filter on the parameter space, but never mind that for now). However, in many analysis applications one actually works with expressions such as ( f(n) = g(n) + O(h(n))), ( f(n) \leq g(n)+O(h(n)) + O(k(n))), etc., where (a) the parameter (n) has been made explicit, and (b) the O() notation is applied to one or more terms, but not necessarily to the entire right-hand side. A typical usage:
( (n+1)^{e^{1/n}} = (n+1)^{1 + O(1/n)})
=exp((log𝑛+𝑂(1/𝑛))(1+𝑂(1/𝑛))
( = \exp( \log n + O(\log n/n) ) )
( = n (1 + O(\log n/n)) )
( = n + O(\log n) )
as (n \to \infty).
In principle, (a) can be dealt with in Lean by function extensionality ((f=g) iff (f(n)=g(n)) for all (n)) and (b) can be dealt with by opening and closing existential quantifiers, but this would be quite tiresome; for instance, formalizing the above calculation this way would definitely be unpleasant, as one would have to open and close quantifiers and functions incessantly.
It occurs to me that what one could do instead in many situations is replace the implied constants by explicitly named constants (C_1, C_2, C_3, \dots), with each constant defined (possibly nonconstructively, for instance using the Exists.choose routine in lean) from preceding ones. This is usually slightly painful to do in Mathematical English - but mostly because it forces one to write out the details in the proof that one would write anyway when formalizing. So it may be the path of least resistance.
Finished formalizing in #Lean4 the proof of an actual new theorem (Theorem 1.3) in my recent paper https://arxiv.org/abs/2310.05328 : https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/jensen.lean . The proof in my paper is under a page, but it the formal proof uses 200 lines of Lean. For instance, in the paper, I simply asserted that ( t \mapsto \log(e^t + a) ) was convex on the reals for any ( a > 0 ) as this was a routine calculus exercise, and then invoked Jensen's inequality but writing out all the details took about 50 lines of code. But it seems there are tools in development to automate such exercises.
The ability of Github copilot to correctly anticipate multiple lines of code for various routine verifications, and inferring the direction I want to go in from clues such as the names I am giving the theorems, continues to be uncanny.
Lean's "rewrite" tactic of being able to modify a lengthy hypothesis or goal by making a targeted substitution is indispensable, allowing one to manipulate such expressions without having to always type them out in full. When writing out proofs in LaTeX, I often crudely simulated such a tactic by cutting-and-pasting the lengthy expression I was manipulating from one line to the next and making targeted edits, but this sometimes led to typos propagating themselves for multiple lines in the document, so it is nice to have this rewriting done in an automated and verified fashion. But the current tools still have some limitations; for instance, rewriting expressions that involve bound variables (e.g., the summation variable in a series) is not always easy to accomplish with current tactics. Looking forward to when one can simply ask an LLM in natural language to make such transformations...
Am slowly learning to trust in #Lean4's ability to work with "holes" - missing hypotheses or variables in a tool that I did not explicitly supply in advance, making my code be much less clunky and flow better. Many thanks to the pull requesters who demonstrated this ability in their contributed code.
For instance, suppose I had to prove ( a / c = b / c ) for some real numbers ( a,b,c). The tool div_left_inj' proves this equation is equivalent to ( a = b ), but only under the hypothesis ( c \neq 0 ) [which we need even if we define division by zero, as discussed earlier]. If I were to have done this a few days ago, I would have first established the hypothesis ( c \neq 0) by some argument (using the Lean code have h : c \neq 0 := by <argument>, and then applied the tool as rw [div_left_inj' h]. A little later I learned how to combine these two lines by rw [div_left_inj' (show c \neq 0 by <argument>)] or even (in some cases) rw [div_left_inj' <argument>]. But now I also realize that one can just write rw [div_left_inj'] (or just field_simp) with no hypothesis whatsoever, and Lean will still reduce to (a=b), but also tack on ( c \neq 0) to the queue of goals to be proved. This removes the need to manually state these sorts of side hypotheses at all, and can lead to cleaner code.
As a small example of this, here is a proof I recently wrote that the function ( g : x \mapsto e^x + a ) is differentiable over the reals. I just apply the existing tools that addition and exponentiation preserve differentiability, and that the identity and constant functions are differentiable, and the proof more or less matches the one one would give in Mathematical English.
In my previous #Lean4 proof of Maclaurin's inequality ( s_k(x)^{1/k} \geq s_\ell(x)^{1/\ell} ), I had assumed that the variables (x_1,\dots,x_n) were strictly positive. I spent several hours today extending this inequality to the case when the variables were merely non-negative. In the analyst's dialect of Mathematical English, this is a one-line proof, namely "by the standard limiting argument". Unpacking this into a formal proof required me to go through a fair bit of the Mathlib documentation on continuous functions, with two main tasks: firstly, to show that the function
was continuous at the origin within the positive real axis ( { \varepsilon > 0} ), and secondly that the origin was in the closure of the positive real axis. The second fact is presumably somewhere in MathLib, but I ended up doing the undergraduate real analysis exercise of proving it from first principles. The first task looked daunting initially as I was contemplating a first-principles approach, but the Mathlib routines made this part actually quite easy. The final argument is at https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/maclaurin.lean
Working with functions (in which everything depended on a (\varepsilon) parameter) ended up being fairly smooth. It has made me more relaxed about the need to work with asymptotic notation in the later parts of my paper.
I managed to prove the Maclaurin inequality in #Lean4 (proof is at https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/maclaurin.lean ). I tried to do this more systematically by writing a proof on pen and paper first, then in LaTeX, then writing a Lean skeleton, then filling in all the sorries in Lean, and timed myself. It took about 10 mins to get a pen and paper proof (in large part because I took a wrong turn for the first five minutes, and had to correct myself), 5 mins to convert that sketch to LaTeX, 33 mins to write the Lean skeleton, and then 3.5 hours to write the Lean code. So my previous estimate of a 25x slowdown to formalize is still basically accurate for me.
This time I did not experience major obstacles, but lots of minor ones. There are some technical issues with matching the real exponentiation operation x^y (where x,y are both real) with the algebraic exponentiation operation x^n (where x is real and n is a natural number), which I had to hack out by inelegant ad hoc methods.
I found the apply? tactic to be very useful when I was at the very end of establishing some intermediate result, it often gave exactly the right step needed to close it off.
My next goal is to prove an inequality from my paper (Theorem 1.3), which will use a little bit of calculus and complex number arithmetic, as well as the triangle inequality, but these look manageable to formalize for me. (The rest of the paper uses asymptotic notation, which I am a little more worried about, but I will cross that bridge when I get to it.)
It's been about eight days since I started learning #Lean4. Some thoughts on the process so far:
With the available online documentation and tools (including AI tools), it is possible to reach a "Turing complete" capability in Lean within a few days, in that most reasonable small formalization tasks can be done in principle. However, there is a lot of folklore knowledge about how to formalize efficiently and intelligently, and how to fully exploit the existing tools. So far, it seems that this knowledge can really only be obtained by interaction with existing human experts; AI tools for instance may provide some working solution to any given problem, but not necessarily the one that represents best practices.
Compiling a phrasebook for myself at https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo was extremely helpful for me, though perhaps for idiosyncratic reasons, and writing/updating it was as educational for me as reading it. Each person may have their own bottleneck to learning this language that may require a different solution.
So far, the high level steps of a mathematical argument have been relatively straightforward to formalize; it is the "obvious" low level details that keep tripping me up. But, thanks in large part to interactions with human experts, I am learning how to resolve these. But perhaps as the tools develop (in particular AI tools and StackOverflow type Q&A sites) it will become easier to get around these hurdles.
I estimate my initial formalization speed as being roughly 100x slower than writing an informal mathematical proof in a reasonably detailed fashion. It's improving to something more like 25x now, but certainly not anywhere close to 1x. Which would be a gamechanger...
Continuing to make progress on my #Lean4 formalization project. Thanks to a tip from a follower here, I was able to complete the proof that the derivative of a polynomial that splits of the reals, also splits over the reals, and as such I have finished the proof of the first non-trivial lemma of my paper (Lemma 2.1). From this I hope to derive the Newton inequalities fairly readily.
As before, it is the minor "obvious" facts that are often the hardest to formalize. Here was a surprisingly challenging proof of the result that if a polynomial ( \sum_{k=0}^n a_k z^{n-k} ) vanishes, then all of the coefficients (a_0,\dots,a_n) vanish. (Though I have found on the Zulip chat that many of my proofs can be condensed by a factor of 5x or more by the experts.)
Continuing my journaling of my #Lean4 project. Progress is slower than expected. After several hours of work, I was able to establish the Pascal identity
though for technical Lean reasons it was convenient for me to asssume one had an infinite sequence ( x_0, x_1, \dots ) of real variables to prove this, even though only the first (n+1) of these variables are actually used.
I am finding though that it is not the mathematically interesting portions of the argument that are difficult to formalize, but rather the "obvious" steps. For instance, I had thought that to get from this identity to the generating function identity
would be a routine induction, since it is "obvious" from the Pascal identity (plus some easier identities to handle boundary cases) that the two polynomials
had the same coefficients. I invested several hours into this and was only able to make partial progress, in large part due to the nasty nature of the subtraction operation ( -: {\bf N} \times {\bf N} \to {\bf N} ) Lean defines on the natural numbers, which actually evaluates to( (a,b) \mapsto \max(a-b,0) ) to keep the output inside the natural numbers. (See for instance the ridiculously complicated proof enclosed that I had to come up with to establish the "obvious" fact that
( \sum_{k \leq n} 1_{n-k = l} f(k) = 1_{l \leq n} f(n-l) ).)
I now appreciate Scott's previous advice to rewrite the generating function identity in a way that does not use natural number subtraction.
Learning #Lean4 reminds me of learning a natural language that is closely related to a natural language that one is already fluent in; in this case, the fluent language is Mathematical English. As such, I am finding it useful to compile a sort of "phrasebook" that takes typical sentences in Mathematical English (and the contexts in which they would be used) and describes a rough Lean equivalent (or at least close enough that I can then look up documentation or perform trial and error to get an exact translation). I have started such a document at https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit?usp=sharing and plan to keep updating it as I keep learning (though perhaps eventually I will outgrow the need for it). I wonder if similar such resources already exist in the Lean community (or whether there should be some crowdsourced effort to make one).
Incidentally, #GPT4 has a decent ability to supply any given line of this phrasebook, though I am finding that several of its responses are more suited for Lean3 than Lean4 (even when explicitly pressed to only discuss Lean4 syntax). I suspect this could be due to the cutoff date for GPT4's training, which may predate the widespread replacement of Lean3 with Lean4.