Imagine a world where complex mathematical proofs are effortlessly translated into computer code, paving the way for automated theorem proving and revolutionizing scientific research. Large Language Models (LLMs) like GPT-3.5, GPT-4, and Gemini Pro hold immense potential for autoformalization—converting informal mathematical statements into formal, computer-verifiable code. But how close are we to this reality? A new study using Lean4, a powerful mathematical programming language, puts these LLMs to the test with a benchmark of 101 mathematical statements across diverse topics like algebra, topology, and category theory. The results reveal a mixed bag. While LLMs show promise in some areas like information theory and logic, they struggle with more complex domains like category and model theory. This suggests that the prevalence of these topics online might influence LLM performance, highlighting the challenge of formalizing concepts that are difficult to express even in natural language. The study uses a novel "correction effort" metric, grading the LLMs on a scale of 0 (perfect autoformalization) to 4 (requiring as much effort as starting from scratch). Interestingly, Gemini Pro, designed with multimodal capabilities and recent training on Lean4 data, shows a slight edge in reasoning tasks. However, both GPT-4 and Gemini Pro sometimes produce outputs requiring significant correction, indicating that even the most advanced LLMs are not yet ready to replace human mathematicians. This research provides a crucial benchmark for future LLM development in autoformalization, highlighting the need for further refinement to unlock the full potential of AI in mathematical research and beyond. The Lean4 benchmark offers a valuable testing ground for pushing the boundaries of AI's mathematical prowess, bringing us closer to a future where complex mathematical reasoning can be automated and verified with unprecedented speed and accuracy.