Theorem proving with large language models has recently gained substantial attention as a direction for developing trustworthy and verifiable AI reasoning. This talk gives a brief introduction to the proof assistant Lean, which provides the verification layer for formal theorem proving, and reviews recent trends in LLM-based theorem proving. These methods rely increasingly on natural-language descriptions of mathematical arguments, which brings renewed attention to the relationship between informal mathematical language and formal representations. I will discuss the gap between natural-language mathematical expressions and the formal representations, and explain why the high level of abstraction in existing formal structures can be a limitation for natural-language–driven methods. This motivates the need for more human-oriented forms of formalization. As one approach, I will present a rule-based method for autoformalization. This talk is based on the work done at the 2025 KIAS winter school on Mathematics and AI.