Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

In the world of university mathematics, the act of proving a statement is more than just solving a problem; it is a cultural practice. It is a specific way of thinking, writing, and validating ideas that students must learn as they move from high school to higher education. For decades, educators have watched students struggle to bridge the gap between the intuitive, informal arguments they learned earlier and the rigid, explicit standards required at the university level. Recently, a new tool has entered this landscape: the proof assistant. These are computer programs designed to check mathematical arguments with absolute precision, forcing the writer to leave no step unexplained. While some see these tools as a way to make math more rigorous, others worry they might stifle creativity or confuse students who are already struggling. The question is not simply whether these programs help or hinder, but how they change the very nature of how proof is written and understood.

A team of researchers at two French universities decided to look closely at this interaction. They did not just ask if students learned better; they watched how the computer program reshaped the students' thinking process. The study focused on a first-year course where students used a specific type of proof assistant called Verbose Lean. Unlike standard programming languages that look like code, Verbose Lean allows students to write in a controlled form of natural language, making it feel closer to the way mathematicians speak and write on paper. The researchers observed a pair of students working on a classic problem: proving that if a sequence of numbers gets closer and closer to a positive value, the numbers in that sequence must eventually become positive themselves. By recording the students' conversations, their scribbles on paper, their typing on the screen, and the computer's feedback, the researchers created a detailed map of how a mathematical idea travels from a rough thought to a computer-verified fact.

What the researchers found was that the computer did not just check the final answer; it acted as a mirror, revealing hidden assumptions that students usually take for granted. In a normal math class, a student might skip over small details or rely on a "feeling" that a step is obvious. The computer, however, demands that every single object, every condition, and every logical jump be explicitly named and justified. The study showed that this requirement forces a kind of cultural shift. The students had to translate their fluid, intuitive ideas into a rigid structure that the machine could understand. This process was not smooth. It involved a constant back-and-forth between the students' paper notes, their spoken words, the computer's error messages, and the teacher's explanations.

The researchers tracked a specific mathematical expression that appeared throughout the students' work. At first, the students treated this expression as a helpful number to use in their reasoning. However, when they tried to type it into the computer, the program rejected it. The computer did not say the number was wrong mathematically; it said the number was in the wrong place. The students had tried to use it as a label for a position in a sequence, but the computer needed a whole number for that role, while their expression was a fraction. This moment was a turning point. It forced the students to realize that in the world of the proof assistant, the role a number plays is just as important as the number itself. They had to rethink their strategy, moving the expression from one part of their argument to another, where it finally fit the computer's strict rules.

This struggle was not solved by the computer alone. The teacher, working at the blackboard in the same classroom, drew a diagram to explain the concept visually. He described a "window" of size that helped the students see why their number needed to be smaller than the target value. This visual explanation, combined with the computer's rejection of their first attempt, helped the students reorganize their thoughts. They eventually realized that the number they had been fighting with was not the position in the sequence, but the size of the gap they needed to measure. Once they made this switch, the computer accepted their argument. The final proof was not a straight line from idea to solution; it was a complex journey where the meaning of a single symbol changed depending on whether it was being spoken, written on paper, explained by a teacher, or checked by a machine.

The study suggests that proof assistants act as "epistemic revelators," a term the authors use to describe tools that make the invisible visible. They reveal the "unthoughts" of mathematics—the parts of a proof that experts and students usually leave unsaid because they seem obvious. In a traditional classroom, these gaps might go unnoticed. In a classroom with a proof assistant, the computer forces the student to fill every gap, exposing the hidden rules that govern mathematical validity. The researchers argue that this does not mean the computer is better than the human, or that the human is better than the computer. Instead, the two systems work together to create a new space where different ways of thinking about proof collide and merge.

The findings indicate that the introduction of these tools changes the culture of proof in higher education. It is not just about adding a layer of technical rigor; it is about reconfiguring how students understand what it means to be right. The study shows that students do not simply learn to write code; they learn to navigate between different worlds of meaning. They must learn to translate their intuitive understanding into a language that a machine can verify, while also listening to the teacher's human explanation. The computer's error messages are not just obstacles; they are signals that tell the student where their understanding is incomplete. By forcing students to make their implicit assumptions explicit, these tools provide a unique opportunity to study how mathematical knowledge is built and validated.

Ultimately, the paper concludes that proof assistants are not neutral tools. They carry with them specific ideas about what counts as a valid argument. When students use them, they are not just learning math; they are learning a new set of cultural rules for how to think and communicate. The researchers suggest that this shift offers a privileged place to study the continuity and the breaks between the way proof is taught, the way it is practiced by experts, and the way it is checked by machines. The journey of the students in this study, from their initial confusion to their final success, illustrates that learning to prove with a computer is a process of translation. It is a process where the meaning of a mathematical idea is tested, reshaped, and ultimately stabilized through the interaction of human intuition, teacher guidance, and machine precision.