{"id":"arxiv:2506.07047","kind":"preprint","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","authors":["Yu Xuejun","Jianyuan Zhong","Zijin Feng","Pengyi Zhai","Roozbeh Yousefzadeh","Wei Chong Ng","Haoxiong Liu","Ziyi Shou","Jing Xiong","Yudong Zhou","Claudia Beth Ong","Austen Jeremy Sugiarto","Yaoxi Zhang","Wai Ming Tai","Huan Cao","Dongcai Lu","Jiacheng Sun","Qiang Xu","Shen Xin","Zhenguo Li"],"author_count":20,"year":2025,"published":"2025-06-08","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2506.07047","nct_id":null,"source_url":"https://arxiv.org/abs/2506.07047","archive_url":"https://space-kitty.com/papers/arxiv:2506.07047","updated":"2025-06-08","pmid":null,"pmcid":null,"openalex_id":"W4417126526","pdf_url":"https://arxiv.org/pdf/2506.07047","abstract":"Recent advances in large language models show strong promise for formal reasoning. However, most LLM-based theorem provers have long been constrained by the need for expert-written formal statements as inputs, limiting their applicability to real-world problems expressed in natural language. We tackle this gap with Mathesis, the first end-to-end theorem proving pipeline processing informal problem statements. It contributes Mathesis-Autoformalizer, the first autoformalizer using reinforcement learning to enhance the formalization ability of natural language problems, aided by our novel LeanScorer framework for nuanced formalization quality assessment. It also proposes a Mathesis-Prover, which generates formal proofs from the formalized statements. To evaluate the real-world applicability of end-to-end formal theorem proving, we introduce Gaokao-Formal, a benchmark of 488 complex problems from China's national college entrance exam. Our approach is carefully designed, with a thorough study of each component. Experiments demonstrate Mathesis's effectiveness, with the autoformalizer outperforming the best baseline by 22% in pass-rate on Gaokao-Formal. The full system surpasses other model combinations, achieving 64% accuracy on MiniF2F with pass@32 and a state-of-the-art 18% on Gaokao-Formal.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.AI"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}