We are AI4M Team, BICMR@PKU, a research team from Peking University's Beijing International Center for Mathematical Research. Our team brings together diverse expertise spanning pure mathematics, applied mathematics, and computer science.
Our long-term goal is to push the boundaries of LLMs and AI agents to accelerate progress in modern mathematics and turn this vision into reality. Through formalization methods, we aim to develop AI agents specialized in mathematics and formal reasoning—capable of tackling cutting-edge algebraic conjectures. Since our team’s founding, we have remained committed to research-level mathematical reasoning and automated theorem proving. We are passionate about supporting the formalization and mathematics communities by building powerful AI tools that advance their work.At the core of our mission is the symbiotic relationship between AI and mathematics: while mathematics provides the theoretical foundation for AI development, AI tools can accelerate mathematical research itself. We work on formalizing mathematical concepts in languages like Lean, creating machine-readable datasets that embody mathematical rigor, and developing AI systems that can assist in cutting-edge mathematical exploration. Both formal theorem proving and semantic retrieval are areas where we maintain active development.