3 accepted papers
Recent formal reasoning systems achieve IMO-level performance, but create a fragmented landscape: algebra and number theory use Lean, while geometry relies on domain-specific languages with limited formal guarantees. This fragmentation increases the trusted computing base and hinders unified model d…
Autoformalization aims to translate natural-language mathematical statements into a formal language. While LLMs have accelerated progress in this area, existing methods still suffer from low accuracy. We identify two key abilities for effective autoformalization: comprehensive mastery of formal-lang
Recent advancements, such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B, demonstrate a prevailing trend in leveraging reinforcement learning (RL)-based large-scale training for automated theorem proving. Surprisingly, we discover that even without any training, careful neuro-symbolic coor…