Mathematical reasoning is one of the most advanced forms of human intelligence. Humans develop formal languages for rigorously describing mathematical problems and deriving mathematical knowledge. The machine learning community has endeavored to develop neural models with mathematical reasoning capabilities as humans. On the other hand, a shared vision in the community is that the models collaborate with humans for mathematical discoveries. The goal of this workshop is to bring together researchers working on various domains to discuss the progress and the future of applying AI technologies to mathematics. As mathematics is fundamental for almost all modern sciences (including computer science), a vast range of related topics are also within our scope. To this end, this workshop focuses on several crucial yet underexplored problems. Specifically, we are expecting attendants from various backgrounds, institutions, and disciplines to discuss areas related to the following: * Autoformalization and the reversed auto-informalization: How can we develop methods that improve the precision of the autoformalization process from natural language proof to formal proof, and as a dual process describing a formal proof in natural language?* Automated theorem proving: How do build consistent theorem proving? How do we relieve or solve the intermediate step errors in proving? * Automated theorem generation: Can neural models generate new and practically valid theorems? How do we take full advantage of such generated new theorems? * Code augmentation and auxiliary for mathematical reasoning: How can the handy and plentiful code data facilitate the models to conduct mathematical reasoning? * Formal verification and code generation: How can progress made in AI for Math help or be directly deployed to the field of formal verification? What are the common technical difficulties? How can AI systems be able to write provably correct code, given any (formal) specifications?In addition to the problem areas above, we also welcome research work related to the following topics:* Measurement: How do we measure autoformalization?* Reasoning in related areas: program synthesis, software verification, neurosymbolic reasoning, logical reasoning.* Applications: Applying mathematical reasoning techniques to sciences, finance, education, etc. Our workshop also includes an innovative challenge with three tracks for related mathematical reasoning problems:* Challenge/Track 1: Autoformalizaiton.* Challenge/Track 2: Automated theorem generation and proving.* Challenge/Track 3: Automated optimization problem-solving with code.