Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
Zixuan Xie, Xinyu Liu, Shangtong Zhang
The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those success…
cs.LO2026
MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
Xinyu Liu, Zixuan Xie, Amir Moeini +5
While the ecosystem of Lean and Mathlib has enjoyed celebrated success in formal mathematical reasoning with the help of large language models (LLMs), the absence of many folklore…