Juho Kupiainen (Jan 03 2020 at 21:22):
The aim of Lean is for math to help programmers and for programmers to help math. What are the most beautiful realizations of this?
Kevin Buzzard (Jan 03 2020 at 22:22):
I think that Gouezel's discovery of an error in the published math literature was quite an interesting realization (using Isabelle/HOL not Lean though).
Last updated: Aug 03 2023 at 10:10 UTC