In this blog I will describe the blueprint of developing agentic systems for autoformalization of research-level mathematics.
AI4MathLean
Author:timechess
Read more →I'm a phD student at Gaoling School of Artificial Intelligence, Renmin University of China under the supervision of Hongteng Xu. My research interests lie in the applications of AI for mathematics, especially formal mathematics. I'm working to create systems that can assist working mathematicians with advanced AI tools and eventually boosting the mathematical reasoning capacities of AI models.
Latest Blogs
View All PostsIn this article, we will go through the basic concepts of Lean 4 to understand the simplest proof.
Lean
Author:timechess
Read more →Latest Publications
View All PublicationsPublished in 2nd AI for Math Workshop @ ICML 2025. Hornoable Mention Award.
AI4MathPremise SelectionLeanInformation Retrieval
Authors:Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu