@whenning There is enough data to get LLMs to be able to write some short Lean proofs with reasonable accuracy, see e.g., the benchmark datasets at https://leandojo.org/ , but the corpus is certainly smaller than that of major programming languages or LaTeX (and also there is the technical complication that there was a recent transition from Lean3 to Lean4, which is not backwards compatible). I think there will be more adequate sources of data in the future (e.g., including synthetic Lean data), and more efficient ways to train, so the situation should improve.
