If anybody's interested in learning more about Lean, he's been posting his experiences with the project over at @tao@mathstodon.xyz