AI RESEARCH
DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems
arXiv CS.AI
•
ArXi:2510.10815v4 Announce Type: replace Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathematical knowledge and its corresponding formal representation in languages like Lean.