[cbondurant]

Lean was a gamechanger for me as someone who has a "hobby" level interest in abstract mathematics. I don't have the formal education that would have cultivated the practice and repetition needed to just know on a gut level the kinds of formal manipulations needed for precise and accurate proofs. but lean (combined with its incredibly well designed abbreviation expansion) gives probably the most intuitive way to manipulate formal mathematical expressions that you could hope to achieve with a keyboard.

It provides tools for discovering relevant proofs, theorems, etc. Toying around with lean has actively taught me math that I didn't know before. The entire time it catches me any time I happen to fall into informal thinking and start making assumptions that aren't actually valid.

I don't know of any way to extract the abbreviation engine that lean plugins use in the relevant editors for use in other contexts, but man, I'd honestly love it if I could type \all or \ne to get access to all of the mathematical unicode characters trivially. Or even extend it to support other unicode characters that I might find useful to type.

[bwfan123]

Bessis [1] argues that formalism - or loosely math writing - is foundational to clarifying intuition/meaning in a way that natural language cannot. Imagine it as a scalpel carving out precise shapes from the blur of images we carry thereby allowing us to "see" things we otherwise cannot.

I am curious to try out lean to understand how definitions in lean are able to operationally capture meaning in an unambiguous manner.

[1] https://www.amazon.com/Mathematica-Secret-World-Intuition-Cu...

[lo_zamoyski]

For mathematics and certain fields, that is true. But the formalism matters, and as some have argued, the Fregean style that came to dominate in the 20th century is ill-suited for some fields, like linguistics. One argument is that linguists using this style inevitably recast natural language in the image of the formalism. (The traditional logical tradition is better suited, as its point of departure is the grammar of natural language itself.)

No formalism is ontologically neutral in the sense that there is always an implied ontology or range of possible ontologies. And it is always important to make a distinction between the abstractions proper to the formalism and the object of study. A common fallacy involves reifying those abstractions into objects of the theory, at least implicitly.

[confidantlake]

It is interesting that you argue for formalism using a metaphor in natural language, rather than use a mathematical/data oriented argument. I find the metaphor pleasing in a way that I suspect a more data driven argument would not be.

[anon291]

I mean, if you understand leans system then you understand the formal manipulation needed for precise and accurate proofs. Most mathematical papers are rather handwavy about things and expect people to fill in the formalism, which is not always true, as we have seen