A majority of these proofs have not been formally verified yet, I think people are overstating how important lean is to the success of LLMs in mathematics.
[1] https://github.com/openai/math/blob/main/preprints/An-Almost... [2] https://github.com/openai/math/blob/main/lean/ComparatorChal...