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 https://groups.google.com/d/msgid/metamath/497b8063-c743-4dd6-950f-306d91b8fca9%40googlegroups.com.