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

The fall of the theorem economy

davidbessis.substack.com

Post reply on HN
Print view View original

41–50 of 127 posts

Re: The fall of the theorem economy

#41

Post by credit_guy »

People think mathematics is about proving theorems.

I think that's just an accident of history.

When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidence that our battle tested software is correct, mostly. And we tell people that we will never be 100% confident that any software is bug free. But that's a slight lie: if we wanted such confidence, we would start using provers, and create bug-free software. That possibility exists, but it's just extraordinarily expensive.

Well, in math that's the only possibility, and we use it. And it is indeed extraordinarily expensive, but it's also the cheapest among the alternatives. The alternatives are 2: be rigorous and do these proofs, or be sloppy and allow bugs to creep in, and allow an entire school of math to collapse like the Italian school of algebraic geometry [1].

There is one more alternative. If a particular math theorem has some applicability, then you write a program and use it in real life. In time you eliminate the bugs as much as you can, and you get to the steady state of "virtually bug free". At that point you don't have a solid proof that the theorem is correct, but in general you don't really care. Because you feel that a formal proof is just a thing one would pursue for getting academic satisfaction only.

[1] https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...

Re: The fall of the theorem economy

#42

Post by simiones »

credit_guy wrote: post #41

People think mathematics is about proving theorems. I think that's just an accident of history. When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidenc…

This is a bit reductive about what "proof" actually means in mathematics. Even in math, the kind of formal proofs that tools like Coq can automatically verify are an extreme, and lots of accepted and practiced math is not doing that. Proofs are often more abstract and even occasionally hand-wavy (for example not proving "obvious" statements or minor lemmas).

Mathematicians also occasionally build on top of unproven foundations (e.g. all popular asymmetric encryption schemes are built on top the assumption that certain problems such as integer factoring are hard, for which there is no formal proof), or at least explore both possibilities for statements with unknown truth value (e.g. you can find lots of work that explores the consequences of P = NP and/or P != NP).

However, there is a major separation between math and programs that I think mostly invalidates your proposal - most math we're talking about here is simply not applicable directly to the real world in any way. It's only studied for the interest of mathematicians. There is no real world consequence for Fermat's last theorem, for example - it was just a really interesting to prove theorem. In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.

Re: The fall of the theorem economy

#43

Post by RandomLensman »

simiones wrote: post #42
credit_guy wrote: post #41

People think mathematics is about proving theorems. I think that's just an accident of history. When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidenc…

This is a bit reductive about what "proof" actually means in mathematics. Even in math, the kind of formal proofs that tools like Coq can automatically verify are an extreme, and lots of accepted and practiced math is not doing that. Proofs are often more abstract and even occasionally hand-wavy (for example not proving "obvious" statements or minor lemmas). Mathematicians also occasionally build on top of unproven f…

> In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.

What specific areas were you thinking off? I don't recall, e.g., in numerics that things were often just unproven/conjectures, but might be subject matter specific.

Re: The fall of the theorem economy

#44

Post by armchairhacker »

stackbutterflow wrote: post #15

Tangential but this article got me thinking. Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves. Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match o…

> if a computer can match or surpass the collective output of the entire human scientific community the equation will change

Yes, but this is when someone reaches ASI and everything changes. For now, a good researcher can build off their discovery in a way their AI can’t.

Re: The fall of the theorem economy

#45

Post by asdfsa32 »

capnrefsmmat wrote: post #26
asdfsa32 wrote: post #25

Is being pompous and on the nose part of being in mathematics? "I was in Switzerland", "I was invited to a talk", "I started a machine learning company", look at me bro.

Being invited to conference talks around the world is a completely normal part of being an active researcher in almost any academic field, so it doesn't register as pompous to other academics.

Yes, which makes starting with those somewhat strange as they're largely unrelated.

Re: The fall of the theorem economy

#46

Post by dkural »

credit_guy wrote: post #41

People think mathematics is about proving theorems. I think that's just an accident of history. When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidenc…

Your example of the Italian school is well taken, although most of their results were later proven to be correct in the right setting. Severi's example is particularly egregious and I think a major reason this became a thing is Severi's refusal to course-correct and accept that some of the results were not correct. It has echoes of Mochizuki, and I fear, once you dig deeper, some issues around the initial declaration of "We've proven the Classification of Finite Simple Groups". There were many genuine gaps, and a lot of lore taken for granted. The sociology around how this happened is interesting - rushing to announce that it was done was the major mistake, it took away almost all incentive to actually write up the proofs and take them through proper peer-review. Genuine mathematical work was falsely reduced to "write up".

Re: The fall of the theorem economy

#47

Post by dkural »

olooney wrote: post #31

Greg Egan's description of how mathematics evolves into "truth mining" in his novel Diaspora is seeming more and more prescient. It essentially describes what mathematics would look like after formalization records all theorems discovered so far in a huge, collective database and proof assistants can instantly work out the details of a given proof. What remains of mathematics? According to Egan, visualization, intuit…

Spot on! Love Diaspora. This is honestly such a gem of a comment. To some extent, if the AI ever gets "so far ahead" of humans, the most productive aspect will be the frontier visible to humans. We're focused on translating mathematics to lean at the moment, but it'll be as important to translate it to humanese - to the human language of structure, number, geometry. I also completely agree with LLMs being essentially blind to visual reasoning. They really struggle reasoning with Floer Heegard diagrams for example.

Re: The fall of the theorem economy

#48

Post by andai »

credit_guy wrote: post #41

People think mathematics is about proving theorems. I think that's just an accident of history. When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidenc…

It's interesting that mathematics, which is mostly recreational (I received profound disdain at the math department for asking about applications!) has such rigorous standards, but software, which entire civilizations now run on, does not.

Re: The fall of the theorem economy

#49

Post by chongli »

whack wrote: post #16

The core thesis seems to be that the "real value" is not in producing/proving theorems, but in understanding them. AI might be good at producing and proving theorems, but it fails utterly at getting humans to understand them. Even worse, humans have no interest in working on theorems that have already been proven, so we end up with theorems that will never be understood by humans. I can understand why this is a major…

They got into their field because they love the beauty of mathematics… As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology

I have some sad news for you. 99% of the work mathematicians do has no immediate application, nor even an obvious path toward application in the near future. You mentioned cryptography, so for an example consider number theory: no apparent practical applications, going back thousands of years to the time of Euclid and earlier.

It’s been religion, philosophy, and recreation that have provided the motivations to study mathematics all these years, not applications. Applications have almost always followed long after the development of the pure mathematical theory. For number theory, that was the development of cryptography during WW2, millennia after the ancients laid those foundations.

Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.

Re: The fall of the theorem economy

#50

Post by cmrx64 »

dkural wrote: post #47
olooney wrote: post #31

Greg Egan's description of how mathematics evolves into "truth mining" in his novel Diaspora is seeming more and more prescient. It essentially describes what mathematics would look like after formalization records all theorems discovered so far in a huge, collective database and proof assistants can instantly work out the details of a given proof. What remains of mathematics? According to Egan, visualization, intuit…

Spot on! Love Diaspora. This is honestly such a gem of a comment. To some extent, if the AI ever gets "so far ahead" of humans, the most productive aspect will be the frontier visible to humans. We're focused on translating mathematics to lean at the moment, but it'll be as important to translate it to humanese - to the human language of structure, number, geometry. I also completely agree with LLMs being essentially…

i got so inspired by reading diaspora this year that i instantly started working on some polisware. cipherclerk operational: https://github.com/emberian/dregg

topical to the conversation, it is fully formally verified in lean (with some UC security reductions done in isabelle). also did this in HOL4 inspired by some work i did with ramana kumar in 2016, on reflective self-verifying self-modifying systems: https://github.com/emberian/svenvs

Post reply on HN