Team Instructor

Wang Shanwen

Associate professor, School of Mathematics

Mingli College innovation education tutor

National-level young talents

Distinguished Scholar Young Scholar of Renmin University of China

His main research interests include number theory and arithmetic algebraic geometry, as well as mathematical logic related to number theory, cryptography, spectrum analysis and other mathematical applications.

Innovative content

It is committed to exploring the use of artificial intelligence to promote the development of mathematical formalization and theorem proving, further improving the efficiency and accuracy of theorem proving, and helping to verify key theorem proving in some related mathematical fields. At the same time, the mathematical logic reasoning ability of artificial intelligence is improved by using mathematical formalized mathematical proof as training data. While this involves the interaction of artificial intelligence with math, as math people we still refer to the project as AI4Math.

Q: What is mathematical formalization?

A: Translating the mathematics expressed in natural language into the language of computers.

Q: What does mathematical logic study?

A: The formal system after symbolizing the two intuitive concepts of proof and calculation.

What can you get here?

1. If you just want to learn how to play around with AI and math, join our AI4Math Research innovation community and experience using Lean to verify mathematical proofs.

Q: What is 'Proof Assistant' Lean?

A: Automatic theorem proving (ATP) is a task that generates proofs for theorems specified in formal logic. But because of its large search space, ATP is challenging. Therefore, interactivity theorem proving (ITP) has become an alternative. In ITP, proofs are generated by mathematicians and interacting with software tools called proof assistants. Lean is a software tool that acts as a proof assistant.

2. If you want to master the skills of using Lean to verify your mathematics, you can attend the popular science lectures organized by our scientific research team every month and practice them.

3. If you are interested in participating in the AI4Math research project, we will provide you with systematic guidance and provide the corresponding topic 'XX Course using Formal Proofs (course name is kept secret for the time being) Automatic Problem Checking System'. In the process, you will also learn from our team the deeper and broader mathematics covered in departmental courses.

4. If you want to learn more about the mathematical principles of AI4Math, we will explore and discuss the principles of AI4Math using mathematical logic, and provide you with relevant project support.

5. If you have mathematical or computer skills and would like to conduct in-depth research on AI4Math at the postgraduate level, we welcome you to join our joint research team with famous universities such as Peking University, Fudan University, and Beijing Normal University.

Currently some team members

Lei Bichang

2020 undergraduate in the School of Mathematics

Research direction is basic Mathematics

Yu Xintao

2023 graduate student in School of Mathematics

Research direction is P-optimal transmission theory and AI4Math

Zhang Lulu

2020 undergraduate from the School of Mathematics

Has been awarded the Excellent Camp of the School of Philosophy of Fudan University

Research direction is Model Theory

Li Zebei

2020 undergraduate student in the School of Mathematics

Research direction is basic mathematics

Wu Yitong

2023 undergraduate of the School of Mathematics

For those of you interested in AI4Math

Welcome to our team

WeChat ID: quizas211