Terence Tao on Nostr: My #Lean4 formalization project is reaching the final stretch; roughly speaking only ...
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.
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.