The AI4Math research and innovation team of Minli College Innovation Lab recently launched the Mathematics in Lean science popularization activity, teaching the role of Lean in AI4Math and the basic usage methods for mathematics enthusiasts and students interested in mathematical formalization. From October 22 to November 22, the team coordinated and organized three events, each of which provided two optional times in order to expand the coverage of the event.

Detail of the activity

In the first activity, the team helped students install Lean on their own computers, which laid the foundation for subsequent learning.

In the second activity, the team explained the first two chapters of Mathematics in Lean, which helped students have a deeper understanding of Lean, get familiar with its operation mode, and learn some basic and commonly used tactics, such as rw, exact, ring, etc.

In the last activity, the team explained the third chapter of Mathematics in Lean in depth, and led the students to further learn the logical operations in Lean, how to use logical operations to prove and how to deal with the logical operations involved in the proof.

It is hoped that students can gain a deeper understanding of Lean from this series of science popularization activities, broaden their vision of mathematics learning, and improve their knowledge and skills. At the same time, we also hope that the students can gain like-minded friends in the activity, exchange and discuss with each other, and collision sparks of thinking.

The Innovation Lab will continue to encourage, cooperate and support the innovation teams, organize more meaningful activities, and provide students with a variety of learning and exchange opportunities. Students who are interested in science and technology are welcome to continue to pay attention!

Tutor team

Activity instructor

Wang Shanwen

College of Mathematics

Software installation

Tao Yicheng

Member of the practice Steering group

Group A

Yu Xintao

Zhang Lulu

Wu Yutong

Lin Yijun

Lin Zhi

Group B

Li Zebei

Wu Yutong

Lin Yijun

Lin Zhi