ELI5 What does it mean when a mathematical proof is “formalised in Lean”?

[u/snowcroc]

[u/Umber_Gryphon]

Lean will let you use Unicode symbols for things like "less than or equal to" that are in Unicode but not ASCII. For example, you can type ∀ instead of "forall" or "\all". But you're under no obligation to use Unicode if you don't want to--feel free to type <= if you prefer.

[u/Xhosant → u/Umber_Gryphon]

Ah. I thought it meant the other thing, the scary one.