An important part of reading mathematics is mentally filling in the "correct" interpretation for terms. The optimal amount of detail typically depends on the ta

An important part of reading mathematics is mentally filling in the "correct" interpretation for terms. The optimal amount of detail typically depends on the target audience. Part of that is because making notation fully specified in English is typically cumbersome: If they had written "as their second non-repeating prime", someone could come along saying "shouldn't it say 'second-smallest' or 'in increasing order' as well?". In papers, the use of such terms would typically be accompanied by a formal definition using more precise (but not fully precise, see the talk below) mathematical notation. I mention this not to be pedantic, but because inferring the "invisible" part of mathematics (when it can be done) instead of asking humans to do it explicitly tends to be a big usability improvement in theorem provers. Andrej Bauer has a nice talk about it at https://www.youtube.com/watch?v=wZSvuCJBaFU https://www.youtube.com/watch?v=wZSvuCJBaFU