When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck https://github.com/flyspeck/flyspeck to formally verify his own proof of th

When Hales started in 2003 the Flyspeck project https://github.com/flyspeck/flyspeck https://github.com/flyspeck/flyspeck to formally verify his own proof of the Kepler conjecture he likely didn't know that it would take him (and a team of helpers later) until 2014 to finish. He used hol-light, which is very much geared towards proof automation. Lean is more expressive (being dependently typed) but I am not aware of any real advance in automation over hol-light. Indeed with their focus on code generation (therefore constructive logic) and software verification, proof automation for math is likely harder in Lean. But the expressiveness and good tooling seem to have generated a lot of interests and mathlib has a real active community, which is really good to see.