Kevin Buzzard
@XenaProject
Mathematician learning Lean and trying to teach it to others. Now gone to Mathstodon (March 2023). No longer reading or replying to mentions.
21-05-2019 21:44:04
3,9K Tweets
9,0K Followers
0 Following
Oh, weird coincidence! Two flagship Lean math projects finish within 24 hours of each other. This one (Kummer's 1850 proof of FLT for regular primes) took two years, partly because of the upgrade from Lean 3 to Lean 4 during that time. See leanprover.zulipchat.com/#narrow/stream… for more.