3 papers
cs.AI2026
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…
cs.CL2025
Conjecturing: An Overlooked Step in Formal Mathematical Reasoning
Jasivan Alex Sivakumar, Philipp Borchert, Ronald Cardenas +1
Autoformalisation, the task of expressing informal mathematical statements in formal language, is often viewed as a direct translation process. This, however, disregards a critical…
cs.CL2025
TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition
Yupei Li, Philipp Borchert, Gerasimos Lampouras
Large Language Models (LLMs) excel at both informal and formal (e.g. Lean 4) mathematical reasoning but still struggle with autoformalisation, the task of transforming informal int…