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
The Gowers-Green-Manners-Tao proof of Marton's polynomial Freiman-Ruzsa conjecture terrytao.wordpress.com/2023/11/13/on-… has now been completely formalised by a team led by Tao. It took three weeks! The project was run on the Lean Zulip; here's Tao's announcement leanprover.zulipchat.com/#narrow/stream… .