FIMO: A Challenge Formal Dataset for Automated Theorem Proving (2023 · 53 citations)
Neural provers built on large language models still rarely solve olympiad-grade problems. Formal data is scarce and costly to produce, existing benchmarks contain few truly hard items, and most formal datasets lack natural-language counterparts. The authors address this with FIMO, a Lean benchmark drawn from the IMO…
Process-Driven Autoformalization in Lean 4 (2024 · 33 citations)
Translating natural-language mathematics into formal code (autoformalization) has mostly been studied for languages with large online corpora, such as Lean 3. The newer and fast-changing Lean 4 lacks suitable training and evaluation data. The authors address this with two contributions.
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification (2025 · 17 citations)
Chain-of-Thought reasoning in LLMs often contains hidden errors. Widely used verification approaches, for example process reward models (PRMs) or self-consistency, output scores that come with no checkable justification. The authors propose Safe, a framework that checks each reasoning step using the formal language…

Co-authors here

12 of 22 co-authors with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

Papers of our library cite their works 91 times (of the 149,439 papers whose bibliographies we read); 42 citing papers with a page here →.

Updated 3 November 2026