I concur with one of the other replies: very few or none.

This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.

More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.

Fully agree on the potential for Lean as a generic programming language.