The Application of Coq in Mathematics Teaching

The proof of mathematical theorems has the characteristics of being clever and difficult, which makes it difficult for students to learn and the teaching process is dull and boring. Firstly, this paper explains the interactivity, readability and intelligence of Coq by listing several simple theorems of Morse-Kelley axiomatic set theory. Then through the group teaching experiment of proving the classic Russell’s paradox, we synthesize the characteristics of Coq in teaching mathematics. Finally, teaching effectiveness has shown that Coq can better assist students in understanding mathematical concepts and theorems, enabling more rigorous and standardized mathematical proofs. And positive feedback during interaction cultivated logical reasoning skills and confidence. It is hoped that the use of Coq in teaching assistance can be promoted, providing new ideas for innovative teaching method.