More Robotics with Terence Tao
Here he is using Lean in the VS Code IDE with GitHub copilot to formally prove a part of the Polynomial Freiman-Ruzsa Conjecture extension blueprint, but the GitHub copilot LLM isn't trained on anything outside Mathlib (14:39), so it can't help with the PFR extensions they will be putting in to Mathlib when the project is finished. He's doing this on his laptop, so the compiler gets a bit slow since the proof is several thousand lines long now.
At 16:13 about sometimes not needing certain hypotheses when proving lemmas. I guess that's because those lemmas are really more general than just this theory, and that's the sort of thing that Category Theory shows: some things are true in a category of which this theory is just is one particular instance. See Terence Tao - Using Claude, ChatGPT to Formalise A Theorem About Magmas in Lean. I think this sheds some light on the proof of the Deduction Theorem in Church's paper "A Formulation of the Simple Theory of Types". The Journal of Symbolic Logic, 5(2):56–68, June 1940. http://www.jstor.org/stable/2266170. It seems to me that there's a Grand Canonical Blueprint "out there" in which the theorems are all proved in "the right order" and the whole of mathematics then appears as a deterministic process resulting from counting from 1 to wherever were up to by now. See from the last paragraph on page 69 of Proofs and Representations.
He also did an example of using Lean (and GitHub copilot) to prove epsilon-delta proofs about limits in analysis. He proves the theorems about sums and differences of limits and they are fairly straightforward, but the one about products of limits gets surprisingly hairy. He thinks this was because, rather than starting with an informal proof-sketch, he let copilot guide the formalisation and then had to help whenever it got stuck, which was quite a frequent event!
Subscribe to Terence Tao.
Comments
Post a Comment