This is so cool. I think I had read that some mathematicians were trying to formalize all(?) known math in Lean. Expecting it to be a long term project. And I was recently wondering how long it would be before they turned LLMs loose on the problem.

Seems like plenty of people are already on the path. So cool.