Imagine asking an AI to solve a simple math problem like “What’s 0.6 repeating times 6?” You might be surprised to learn that even the most advanced AI systems often stumble with these seemingly basic calculations. This highlights a significant challenge in the field of Artificial Intelligence: autoformalization, the process of converting natural language into the precise, symbolic language of computer programs and mathematical proofs. While large language models (LLMs) have shown promise in tackling complex problems, a frustrating gap exists between their ability to sometimes get the right answer and their consistency in doing so. New research explores this intriguing discrepancy and offers a potential solution. Researchers have observed that when an LLM generates multiple attempts at formalizing a mathematical statement, the correct formalization is often hidden within these variations, even if the top-ranked answer is wrong. This suggests that LLMs possess the fragmented knowledge necessary for successful autoformalization, but lack a reliable method for selecting the best output. To address this, researchers have developed a framework that leverages two key ideas: *symbolic equivalence* and *semantic consistency*. Symbolic equivalence checks if different formalizations are logically the same, even if they use different symbols. Imagine two programs that arrive at the same answer through different routes—they are symbolically equivalent. Semantic consistency ensures the translated formal statement still means the same thing as the original natural language by “back-translating” the formalization into natural language and comparing it to the original. These two methods, acting in concert, provide a way to score and rank the different formalizations produced by an LLM. The most consistent formalization is then selected. Experiments show this new approach drastically improves accuracy, boosting performance across a variety of LLMs and mathematical problem types. This suggests a future where AI could handle complex mathematical reasoning with greater reliability. However, challenges remain. LLMs sometimes hallucinate non-existent mathematical concepts or misapply rules. The researchers also note that current automated theorem provers, essential tools for checking logical equivalence, aren't always powerful enough for the task. Ultimately, human oversight remains necessary, highlighting the ongoing evolution of this exciting field.