Re: Andrej Bauer gave an extraordinarilly clear talk

[Tim Daly]

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 <avigad@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 <axiomcas@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
>>
>