Something that always bugged me about Lean is how unreadable and unwritable. Math uses extremely heavy notation to make statements concise. It's hard to learn the notation without a visual reference guide, sync the symbols don't have guessable names, but once you know what the symbols mean, it's readable. Java is incredibly verbose but you can make out what it's saying word by word Lean is line noise. It's like assem…
Do you have an example Lean statement you struggle with? I would have posed that they're "just" using standard math notation that should be explained in the relevant textbook for the math you're trying to formalize, but perhaps they are indeed cooking...