Programming is becoming increasingly common in mathematics degrees as it is a desirable skill for new graduates. However, research shows that its use is mostly restricted to computational or modelling tasks. This paper reports a study on students' perceptions of and difficulties with Lean, an interactive theorem prover introduced as part of a transition to proof first-year module. The data consist of first-year university mathematics students' questionnaire responses (n = 99) and sections of 37 semi-structured interviews with students from the same cohort. Findings highlight students' difficulties with syntactic and strategic knowledge, in line with similar research on programming, and how conceptual knowledge is discussed in terms of conceptual-mathematics and conceptual-programming. Moreover, some students share how the experience with Lean changed their perception of mathematics by contributing to the epistemological shift from school to university, which is necessary for students to be successful. However, many students failed to engage with Lean due to its difficult syntax and because they perceived programming to be disconnected from the activity of proving and not worth the time investment needed to become proficient with this tool. We conclude with some reflections on the implications of this study for university teaching and suggestions for future research.