<p>Interactive theorem provers such as Lean are increasingly used in mathematics research and are now introduced into university mathematics teaching. One widely used resource for the introduction to Lean, one such interactive theorem prover, is the Natural Number Game. This gamified learning environment introduces formal proof writing in Lean through interactive exercises (levels) based on statements about natural numbers. However, little is known about undergraduate students’ proof activity in this environment and its key characteristics. In this paper, we adopt the instrumental approach to analyse video-recorded, task-based interviews with two undergraduate mathematics students as they go through the Natural Number Game. This approach allows us to characterise two distinct ways of interacting with the tool, illustrating contrasting perspectives and approaches which may support learning mathematics in different ways. Our findings have implications for students’ use of interactive theorem provers as part of mathematics learning at university and the understanding of mathematical proof.</p>