I was very interested in FOMM 2020, but as there is no transcript I'm 
forced to look at slides and read some second hand impressions. In case 
someone missed it and as it's to some extent related to subject:

"Mario Carneiro talked about metamath 0. I wish I could say more about his 
work, but it is too foundational for me to understand it properly. All I 
know is that we had a proof of Dirichlet’s theorem on primes in an AP in 
metamath and then Mario pressed a button and we had one in Lean, and it had 
been written by a computer and was incomprehensible. Scary?"

That were Kevin Buzzard's impressions :)

BTW, in those slides the line was drawn between verification and synthesis. 
I think this is important too.

You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 

Reply via email to