Junqi Liu

Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require complex mathematical reasoning, current systems seldom succeed in their initial attempt, necessitating iterative adjustments to their proof strategies. Existing approaches for handling failed attempts typically either iteratively fix errors within the proof or discard the entire proof and regenerate it from scratch. The former leads to progressively longer contexts, which degrade the model's ability to attend to the remaining unresolved subproblems, while the latter is inefficient, as it may abandon mostly correct reasoning due to localized errors. To address this dilemma, we present _MechMath_, an agent system centered on a Sorrifier-driven formal decomposition paradigm. By leveraging the `sorry` placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, MechMath extracts each failed subproblem into a clean, self-contained context and resolves it independently. This avoids both the waste of full regeneration and the excessive context length induced by repeated repairs. Experimental results on challenging mathematical competition benchmarks, including IMO 2025, Putnam 2025, miniF2F, and a subset of ProverBench, demonstrate that our agent achieves significant advantages in proving efficiency.

Geometry problems constitute a crucial testbed for AI reasoning. Most existing geometry solving systems rely on domain-specific formal languages that cannot integrate with other mathematical fields, and their dependence on graphical intuition makes rigorous verification particularly challenging. To address these limitations, we introduce \textbf{LeanGeo}, a unified formal framework for expressing and proving competition-level geometry problems within the Lean~4 theorem prover. LeanGeo provides a comprehensive library of 260 high-level geometric theorems grounded in Lean's foundational logic, enabling rigorous proof verification and seamless integration with Mathlib. We further present \textbf{LeanGeo-Bench}, a benchmark of 122 formally verified geometry problems ranging from foundational exercises to International Mathematical Olympiad (IMO) challenges. Our evaluation of state-of-the-art Large Language Models on this benchmark reveals both capabilities and fundamental limitations in automated geometric reasoning. We open-source the theorem library and benchmark at \url{https://github.com/project-numina/LeanGeo}.