DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

Meiru Zhang, Philipp Borchert, Milan Gritta +1

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 pr…