> Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

Absolutely none of them. I have some experience formalizing math by hand in the pre-LLM era. I never started with making the formal proof. It is way too difficult. I don't think I've ever heard of any mathematician starting with a formal proof vs writing a natural language proof. Starting with a formal proof vs a natural language proof is putting the cart before the horse.

Without a natural language proof, or at least an idea of how to write the natural language proof, it is very difficult to write a formal proof. It's flying blind. I can blindly apply tactics, but without some larger plan to guide my formal proof, it's near impossible to make progress on all but the most trivial proofs. I don't think it has ever happened that a major proof was formalized before its natural language proof was written.

I don't think people appreciate just how labor-intensive it previously was to write a formal proof. It takes easily 10-1000x as much time for a human to write a formal proof vs a natural language proof. Even just formalizing a single undergraduate math textbook for certain subjects by hand was considered a multi-year project for a professional mathematician to undertake.

Formalizing a new paper, even if it was building on previously already formalized theorems, could be months of work just by itself, even with the natural language proof in hand.

It is no surprise that OpenAI releases natural language proofs before they release formal proofs. Presumably the same difficulty difference applies to LLMs as well.