Terence Tao on Nostr: Finished formalizing in #Lean4 the proof of an actual new theorem (Theorem 1.3) in my ...
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...
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...