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

61–70 of 127 posts

Re: The fall of the theorem economy

#61

Post by christina97 »

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…

I thought this comment would go in a slightly different direction: the body of work that is mathematics has plenty of “bugs”; proofs with mistakes or other human errors. Yet we take the body to be correct (we believe it “works”) in aggregate, partly because the intuition of mathematicians tells us that these bugs are solvable and don’t bring down the whole. Of course the less intuitive/more surprising/more central the statement, the stricter the standard for proof and more eyes that have walked through it.

Re: The fall of the theorem economy

#62

Post by dboreham »

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…

One thing I've realized after quite a long life of learning and contemplation is that: mathematics and software are essentially the same thing. Add to that that it might be the case that Physics is the same thing too. We'll see on that one, but there are signs...

Re: The fall of the theorem economy

#64

Post by andai »

pclmulqdq wrote: post #56
andai wrote: post #48

Earlier quoted context omitted.

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.

If a piece of software is in safety-critical applications these days, it is often required to have a proof of correctness.

Like Linux? ;)

Re: The fall of the theorem economy

#65

Post by seanhunter »

simiones wrote: post #54
RandomLensman wrote: post #43

Earlier quoted context omitted.

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

Well, it's not exactly engineering, but physics often uses quite informal math. For a pretty modern example, the Dirac delta "function" was used long before it was formally described; and I have heard it said that even today String theory uses some math that is not fully formalized - though I can't say I know what specifically, so I may be wrong. Newton expressed calculus in terms of inifinitesimals (the dx notation…

Newton didn't use dx/dy. That's Leibniz' notation. Newton's notation for the derivative is just to pot a dot above the letter so ṙ would be Newton's symbol for speed (dr/dt) and two dots would be acceleration (d^2r/dt^2) in Leibniz' notation. Physicists still use Newton's notation but only for derivatives with respect to time these days.

The part of Newton's theory that was troublesome is his fluxions don't have the Archimedian property. It took until the 1960s before Newton's notion of fluxions became rigorously formalized with Non-standard analysis. https://en.wikipedia.org/wiki/Nonstandard_analysis

Re: The fall of the theorem economy

#66

Post by TimorousBestie »

vatsachak wrote: post #53
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…

LLMs sure, but AlphaZero had no visual cortex yet can smash Magnus Carlsen easily. I think that we're not that far away from AI that can be superhuman at all facets of theorem proving. I think that we're far away from an AI that can create good abstractions and construct a theory to prove theorems.

> LLMs sure, but AlphaZero had no visual cortex yet can smash Magnus Carlsen easily.

Chess does not require a visual cortex to play. People have been playing by mail with algebraic notation for centuries.

Re: The fall of the theorem economy

#67

Post by TimorousBestie »

rramadass wrote: post #39
guelo wrote: post #20

When math is so divorced from science and engineering that there's no conceivable way that it will ever be applied in the real world then it is just a complex puzzle game that a tiny group of people play. It doesn't really matter much. If the 200,000 line Mathslop proof has no real world application and it doesn't help the puzzle solvers then it is double useless.

Right; this is my viewpoint too. All the "pure mathematicians" have a bleak future where AI can do all the puzzle solving better and faster. They existed in their own world elevating "theorem proving within a formal system" as the central aspect of "proper" mathematics and everything else as ancillary. It always felt wrong to me that while the scientific method iterated starting with the "real world" viz. Observe, Me…

> pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality.

You’re describing a very small fragment of total current mathematical labor. Very few people work solely on “formalization” and even e.g. model theory or type theory have real consequences.

Re: The fall of the theorem economy

#68

Post by TimorousBestie »

Staross wrote: post #17

I thought it was very interesting, but maybe also incredibly naive politically ? it's like he's re-discovering alienation under capitalism. A wood-worker could do the same argument, there's the "official" wood-working word of perfect joinery and beautifully finished tables one can buy, but behind it there's the "secret" messy human element, the art, the craft, the mistakes and hard-ships, the elevation of human skill…

> I thought it was very interesting, but maybe also incredibly naive politically ? it's like he's re-discovering alienation under capitalism.

To be fair, a number of professional politicians and political scientists don’t understand alienation under capitalism.

Re: The fall of the theorem economy

#69

Post by hlynurd »

TimorousBestie wrote: post #66
vatsachak wrote: post #53

Earlier quoted context omitted.

LLMs sure, but AlphaZero had no visual cortex yet can smash Magnus Carlsen easily. I think that we're not that far away from AI that can be superhuman at all facets of theorem proving. I think that we're far away from an AI that can create good abstractions and construct a theory to prove theorems.

> LLMs sure, but AlphaZero had no visual cortex yet can smash Magnus Carlsen easily. Chess does not require a visual cortex to play. People have been playing by mail with algebraic notation for centuries.

This feels like a non sequitur

Re: The fall of the theorem economy

#70

Post by Feathercrown »

rjsw wrote: post #36
aleph_minus_one wrote: post #23

Earlier quoted context omitted.

> to share the load with every brain on the planet willing to give a try at science This is what a lot of scientists love to tell themself or talk about in celebratory speeches. The truth is: a lot of science is kept behind journal paywalls, so that only "officially approved" (in the sense of: working at a university or an governmental research institute) scientists can easily access it.

People are working on using LLMs to regenerate experimental data from the text of journal papers.

Surely you understand that this is impossible in the general case?
Post reply on HN