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

41–50 of 80 posts

Re: Why formalize mathematics – more than catching errors

#41

Post by skybrian »

js8 wrote: post #34
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…

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

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

Re: Why formalize mathematics – more than catching errors

#42

Post by zozbot234 »

dboreham wrote: post #8
constantcrying wrote: post #2

Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding. Computerized mathematics is just another step in that direction.

Imho it was always "computerized", they just didn't have a computer. To me the approaches used in the early 20th century look like people defining a simple VM then writing programs that "execute" on that VM.

> Imho it was always "computerized", they just didn't have a computer.

They had a whole lot of computers, actually. But back then the "computers" were actual people whose job was to do computations with pen and paper (and a few very primitive machines).

Re: Why formalize mathematics – more than catching errors

#43

Post by [deleted] »

dboreham wrote: post #8
constantcrying wrote: post #2

Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding. Computerized mathematics is just another step in that direction.

Imho it was always "computerized", they just didn't have a computer. To me the approaches used in the early 20th century look like people defining a simple VM then writing programs that "execute" on that VM.

[deleted]

Re: Why formalize mathematics – more than catching errors

#44

Post by dkural »

It's good to remind yourself of Bill Thurston's points: https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...

I love the analogy in David Bessis's wonderful book Mathematica (nothing to do with Wolfram). We all know how to tie our shoes. Now, write in words and symbols to teach someone how you tie your shoes. This is what a proof is.

Often even people with STEM degrees confuse what mathematicians do with the visible product of it - symbols and words on a page. While the formalism of mathematics has immense value for precision, and provides a "serialization language" (to borrow a CS analogy), it would be akin to confusing a Toaster with the Toaster manual, or shoelaces with the instructions.

Re: Why formalize mathematics – more than catching errors

#45

Post by KalMann »

Ericson2314 wrote: post #30
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?

Rocq is ancient and has some longstanding UX problems. It is pleasant to try making a new code base. This is kinda like asking, why write Clang when we already had GCC? Or, why making Python if we already have Perl? It's good to have some competition for these things, Rocq I believe felt the heat and has been also doing some good things in recent years.

Why do you keep saying Rocq when he asked about Coq? Are they the same thing?

Re: Why formalize mathematics – more than catching errors

#46

Post by practal »

lo_zamoyski wrote: post #33
Ericson2314 wrote: post #31

Earlier quoted context omitted.

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…

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

Re: Why formalize mathematics – more than catching errors

#47

Post by anon291 »

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…

> How Gödel’s second incompleteness theorem shows that you can prove anything,

That is not at all what it says.

> They both can be useful or harmful,

If a proof is admitted into lean, there is no doubt as to its truth. There is no way in which lean can be construed as harmful.

> The 2009 crash and gaussian copula as an example.

There is nothing mathematical about the economics behind the 2009 crash. Such things are statistical measurements, which admit the possibility of failure, not mathematical conclusions that are demonstrably true.

Re: Why formalize mathematics – more than catching errors

#48

Post by jongjong »

I think the analogy between JavaScript and TypeScript is not 100% because although JavaScript has some quirks in its design, it is fully consistent. My biggest issue with math is symbols that are reused to mean different things in different contexts. It makes maths more time-consuming to learn and makes it difficult to jump between different fields.

Personally, at times, I struggled with the dual nature of mathematics; its extreme precision in meaning combined with vague and inconsistent use of symbols is challenging... Especially frustrating when learning something new and some symbols that you think you understand turn out to mean something else; it creates distrust towards maths itself.

Re: Why formalize mathematics – more than catching errors

#49

Post by Epa095 »

KalMann wrote: post #45
Ericson2314 wrote: post #30

Earlier quoted context omitted.

Rocq is ancient and has some longstanding UX problems. It is pleasant to try making a new code base. This is kinda like asking, why write Clang when we already had GCC? Or, why making Python if we already have Perl? It's good to have some competition for these things, Rocq I believe felt the heat and has been also doing some good things in recent years.

Why do you keep saying Rocq when he asked about Coq? Are they the same thing?

https://en.wikipedia.org/wiki/Rocq

`The Rocq Prover (formerly named Coq) [...] `

Re: Why formalize mathematics – more than catching errors

#50

Post by constantcrying »

dboreham wrote: post #8
constantcrying wrote: post #2

Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding. Computerized mathematics is just another step in that direction.

Imho it was always "computerized", they just didn't have a computer. To me the approaches used in the early 20th century look like people defining a simple VM then writing programs that "execute" on that VM.

Exactly. The step to formalize mathematics through computation is just the logical consequence of the program of the formalizers.

The idea actually goes back to Leibnitz, who was very much overoptimistic about computability, but already conceived of the idea of a logic machine, which could deter the truth value of any statement.

Post reply on HN