3 papers
math.NA2026
A Unified Framework for Formalizing Matrix Decomposition Proofs
Wanli Ma, Zichen Wang, Zaiwen Wen
Existence proofs for many matrix decompositions share a recursive routine: a local transformation prepares the matrix, a slice is selected, a recursive solution is obtained, and th…
cs.AI2026
M2F: Automated Formalization of Mathematical Literature at Scale
Zichen Wang, Wanli Ma, Zhenyu Ming +3
Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is larg…
cs.AI2025
SITA: A Framework for Structure-to-Instance Theorem Autoformalization
Chenyi Li, Wanli Ma, Zichen Wang +1
While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structur…