Depends if you include a few decades of improvements in lean itself. Non-AI proof automation is much better than it was even a year ago and so some fiddly results can now be done with `by grind`.

Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.