[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.

[js8]

I just had a similar discussion with a coworker, he was advocating that LLMs are practically useful, but I argued they are kinda bad because nobody knows how they really work. I think it's somewhat return to pre-enlightenment situation where the expert authority was to be taken for their word, there was no way to externally verify their intuitive thought process, and I believe success of science and engineering is based on our formal understanding of the process and externalization of our thoughts.

Similar in mathematics, formalization was driven by this concern, so that we wouldn't rely on potentially wrong intuition.

I am now in favor of formalizing all serious human discourse (probably in some form of rich fuzzy and modal logic). I understand the concern for definition, but in communication, it's better to agree on the definition (which could be fuzzy) rather than use two random definitions and hope for their match. (I am reminded of koan about Sussman and Minsky http://www.catb.org/jargon/html/koans.html)

For example, we could formally define an airplane as a machine that usually has wings, usually flies. This would be translated into a formula in fuzzy logic which would take, for a given object, our belief this object is a machine, has wings and flies, and would return how much it is an airplane under some notion of usually.

I freely admit this approach wouldn't work for dadaist literary writers, but I don't want lawyers or politicians or scientists to be that.

[skybrian]

The project to formalize everything has been tried before and abandoned. Some issues:

https://metarationality.com/sort-of-truth

Formalism isn't the right tool for a lot of semi-factual fields like journalism or law. Even in business, numbers are of course used in accounting, but much of it depends on arbitrary definitions and estimates. (Consider depreciation.)

[lanstin]

Lawyers (here on HN) have said that contracts that specify everything are too expensive to come up with. Better to cover the most common cases and have enough ambiguity so that weird eventuality end up litigated.

[rpcope1]

> 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.

I agree 100% and feel like I have seen a lot of people in physics kind of fall into this trap. The model is not the thing itself.

[KolenCh]

Are you sure you are really talking about Physics? Are you talking about actual research in physics, or physicists applying their way of thinking in other things?

[Ericson2314]

The people that make theorem provers, because they are type theorists and not set theorists doing ZFC derivatives, are very aware of your last point. Painfully aware, from years of people dismissing their work.

Read Andrej Bauer on them many foundations of math, for example. Clearly he is a believer in "no one true ontology".

[lo_zamoyski]

> The people that make theorem provers [...] are very aware of your last point.

> Clearly he is a believer in "no one true ontology".

My point wasn't that you should aim for some kind of fictitious absence of ontological commitments, only that whatever language you use will have ontological commitments. Even the type judgement e:t has ontological implications, i.e., for the term e to be of type t presupposes that the world is such that this judgement is possible.

You can still operate under Fregean/Russellian presuppositions without sets. For example, consider the problem of bare particulars or the modeling of predicates on relations.

[practal]

Indeed, and e:t in type theory is quite a strong ontological commitment, it implies that the mathematical universe is necessarily subdivided into static types. My abstraction logic [1] has no such commitments, it doesn't even presuppose any abstractions. Pretty much the only requirement is that there are at least two distinct mathematical objects.

[1] http://abstractionlogic.com

[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.

[daveguy]

Right tool for the job. Just like formalism is for math.

[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