Company research post: ~13M lines of Lean over 11 days; Kevin Buzzard calls it an extraordinary autoformalization achievement.