Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why formalize mathematics – more than catching errors

rkirov.github.io

Post reply on HN
Print view View original

31–40 of 80 posts

Re: Why formalize mathematics – more than catching errors

#31

Post by Ericson2314 »

lo_zamoyski wrote: post #11
bwfan123 wrote: post #6

Earlier quoted context omitted.

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 mann…

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 o…

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

Re: Why formalize mathematics – more than catching errors

#33

Post by lo_zamoyski »

Ericson2314 wrote: post #31
lo_zamoyski wrote: post #11

Earlier quoted context omitted.

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 o…

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

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

Re: Why formalize mathematics – more than catching errors

#34

Post by js8 »

lo_zamoyski wrote: post #11
bwfan123 wrote: post #6

Earlier quoted context omitted.

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 mann…

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 o…

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.

Re: Why formalize mathematics – more than catching errors

#35

Post by warkdarrior »

eig wrote: post #27

I’m not a mathematician, so could someone explain the difference in usage between Lean and Coq? On a surface level my understanding is that both are computer augmented ways to formalize mathematics. Why use one over the other? Why was Lean developed when Coq already existed?

Lean has a good library of formalized mathematics, but lacks code extraction (you cannot generate a program from the proofs it constructs). So it is more suitable and highly used by mathematicians to prove theorems.

Coq has always focused on proving program correctness, so it sees lots of use by computer scientists. It also does code extraction, so after you prove a program correct in Coq you can generate a fast version of that program without the proof overhead.

Re: Why formalize mathematics – more than catching errors

#36

Post by lordnacho »

Noob question here.

Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation?

If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check?

I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tests don't check what you thought.

Re: Why formalize mathematics – more than catching errors

#37

Post by konne88 »

lordnacho wrote: post #36

Noob question here. Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation? If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check? I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tes…

You don't know. Even with the best theorem provers, your definitions are still trusted. The best way I've found to help with this is to keep your definitions simple, and try to use them to do things (e.g. can you use your definition to solve other problems, does it work on some concrete examples, etc).

Re: Why formalize mathematics – more than catching errors

#38

Post by konne88 »

I have proven quite a few theorems in Lean (and other provers) in my life, and the unfortunate reality is that for any non-trivial math, I still have to figure out the proof on paper first, and can only then write it in Lean. When I try to figure out the proof in Lean, I always get bogged down in details and loose sight of the bigger picture. Maybe better tactics will help. I'm not sure.

Re: Why formalize mathematics – more than catching errors

#39

Post by eynsham »

nyrikki wrote: post #17
anon291 wrote: post #9

Earlier quoted context omitted.

As a a hobbyist mathematician / type theorist, chatgpt et al are great at 'looking up' theorems that you want to exist but that you may not have read about yet. It's also good at connecting disparate areas of math. I don't think lean subsumes AI. Rather, lean allows you to check the AI proof. ChatGPT genuinely does have a knack for certain lines of thought.

LLMs and Lean are orthogonal, neither subsumes either. They both can be useful or harmful, do to their respective strengths and trade offs. PAC/statistical learning is good at needles in the haystack problems assuming that the tail losses, simplicity bias, and corpus representation issues are acceptable and you understand that it is fundamentally existential quantification and control for automation bias etc… Lean is…

> Gödel’s second incompleteness theorem shows that you can prove anything, without that proof being meaningful is a lens into that.

What has Gödel incompleteness to do with that? We can just take any sentence φ as an axiom, and we’ve a trivial proof thereof.

Re: Why formalize mathematics – more than catching errors

#40

Post by Almondsetat »

lordnacho wrote: post #36

Noob question here. Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation? If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check? I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tes…

Being sure that you are proving the right thing is something that can never be formally guaranteed.
Post reply on HN