I thought his example of linear behavior to be about as clear of a proof construction as any I've ever seen. You could look at his LEAN notation and almost understand it even if you never saw it before. In fact, his LEAN construction is almost Axiom code.
I found his comment that "you're going to learn a lot of mathematics you thought you knew" as being accurate. Every time I think I know something I end up on a journey learning math I thought I knew. Sigh. My head is much too small a place to do mathematics. The LEAN website ought to have a link to that talk. He made the comment that the programming community is one of the largest consumers of the type technology. But my experience is that the LEAN community is not particularly interested in the programming community. I don't find many tools or much effort focused on proving actual programs correct. The focus is more toward the math community, probably because Buzzard is pushing hard. Once I figure out how to get the proof checker running in hardware on an FPGA I'll move back to the LEAN level. I'm making good progress on this. It turns out that it is possible to inject C++ code into the FPGA build stream. If I were smarter I could just grab the LEAN sources. I really want LEAN to focus on program generation from a proof. I want to point at the proof of the GCD, press a button, and have running Lisp code, as well as the list of axioms and definitions for a specification. My current effort of "working backward" from the program to the proof is clearly the wrong way to go. I think I might have to focus on LEAN code generation when I have working hardware. Building Axiom from the LEAN proofs would change the whole world. Tim Where are the graduate students when you need them? :-) On 6/26/21, Jeremy Avigad <avi...@cmu.edu> wrote: > Thanks for pointing this out to me -- I had heard about it. The Scholze > post was huge for us. > > Best wishes, > > Jeremy > > > On Sat, Jun 26, 2021 at 5:47 PM Tim Daly <axiom...@gmail.com> wrote: > >> Andrej Bauer gave an extraordinarilly clear talk >> "The Dawn of Formalized Mathematics" >> https://vimeo.com/567049015 >> >> It is, of course, painfully obvious to us but I think >> it might be a good introduction for a class on Lean. >> >> Tim >> >
