Comment by tossandthrow

You are right. I am imprecise.

Languages allow a certain flexibility in their grammars - you can read a sentence without that adhering it exactly to the grammar.

Games and programming languages (including lean) does not allow this flexibility.

A very intelligent person would likely also reason in terms of probably outcomes before correcting a statement to adhering entirely to the grammar.

Certainly it must be like that, otherwise reviews in math was rendered moot.

Do we blame research mathematicians for not adhering to the grammar?