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

91–100 of 127 posts

Re: The fall of the theorem economy

#91

Post by chongli »

whack wrote: post #88
chongli wrote: post #49

Earlier quoted context omitted.

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

> 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. In a world with no AI, it is vital for humans to understand math, in order to derive practical applications. But in a…

But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.

We have examples of AI producing theorems but there is no evidence that AI will be able to find all of the practical applications of mathematics, at least not any time soon.

As I understand it, most of the theorem proving work done by AI today consists entirely of “glue code” style work: combining a bunch of different known results to prove a new result. This is great for those who desire completeness in the mathematical project but it’s often outside the areas of interest for mathematicians who are pursuing “big idea” problems whose solutions likely require development of entire new branches of mathematics. One famous example of such was Fermat’s Last Theorem.

Re: The fall of the theorem economy

#92

Post by playorizaya »

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…

The ease, extent, and scale at which math integrated with computing along its development makes me wonder if the two fields will effectively enjoin, academically (math and computer programming).

Maybe we will look back on today's math as a kind of arcane, pre-syntactical set of structures that required speakers of the language on both ends interpreting it to make good use of it. No validation or compilation, it can't be applied, just a total wild west - scribbles on a whiteboard and another mathematician making sense of it.

"e=mc^2"

And the Lord's people said: "LGTM"

Re: The fall of the theorem economy

#93

Post by pclmulqdq »

andai wrote: post #64
pclmulqdq wrote: post #56

Earlier quoted context omitted.

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

Like Linux? ;)

I think you might be surprised that Linux is generally not involved in safety-critical systems. There is a whole separate ecosystem for those applications.

Re: The fall of the theorem economy

#94

Post by Terr_ »

observationist wrote: post #85
TheOtherHobbes wrote: post #74

Earlier quoted context omitted.

I'd be very surprised if there aren't huge areas of undiscovered math that can't be explained with either geometric or algebraic views. Math is entirely subjective. "Proof" essentially means "Other educated practitioners have the same experience when trying to understand this." The logical steps that proofs are built on all have that common foundation. Our concept of logic based on our subjective experience of "truth…

This is a serious misconception of human cognitive abilities. We have the ability to abstract generally - there is no abstraction for which we lack the capacity to comprehend. We regularly visualize, contextualize, and satisfactorily explain systems with dozens of dimensions. The fact that we cannot hold 4,5+ spatial dimensions in our imaginations sufficiently to develop an intuition for navigation in that space and…

> there is no abstraction for which we lack the capacity to comprehend.

How could this ever be tested/falsified?

It feels a bit like "there is no idea we cannot think of." If we can't comprehend it, then it won't be an abstraction, it'll just be a mystery.

Re: The fall of the theorem economy

#95

Post by ged_throw_382 »

tsunamifury wrote: post #87
dkural wrote: post #82

Earlier quoted context omitted.

There's actually a lot of math trying to describe the types of space you mention - non quantized, non 'granular', they're not made of points, or distances (metrics). One deep idea is to define space through which symmetries hold (Klein's Erlangen program). Topology itself is not interested in distances per se, only properties of a space invariant under homeomorphisms (a fancy way of saying you can continuously deform…

I know I failed to explain this correctly and was downvoted for it But I think you got my point. “Granularism” itself is an approximation of a specific set of dimensions of space. Tokenizing reality so far is somewhat incompatible with say real time forces (new dimensionalism as you sort of describe here) Even if there are granularities representations of them. So whatever hasn’t been granulized so far AI can’t under…

That sounds a bit like the Gödelian argument against mechanism: reality (or even math) may contain systems that require stepping outside the current framework to formalize. A machine that can only work with current frameworks would be blind to these, except insofar that it can stumble across them by brute force.

Re: The fall of the theorem economy

#97

Post by skoodge »

observationist wrote: post #85
TheOtherHobbes wrote: post #74

Earlier quoted context omitted.

I'd be very surprised if there aren't huge areas of undiscovered math that can't be explained with either geometric or algebraic views. Math is entirely subjective. "Proof" essentially means "Other educated practitioners have the same experience when trying to understand this." The logical steps that proofs are built on all have that common foundation. Our concept of logic based on our subjective experience of "truth…

This is a serious misconception of human cognitive abilities. We have the ability to abstract generally - there is no abstraction for which we lack the capacity to comprehend. We regularly visualize, contextualize, and satisfactorily explain systems with dozens of dimensions. The fact that we cannot hold 4,5+ spatial dimensions in our imaginations sufficiently to develop an intuition for navigation in that space and…

> There's also a huge issue with your use of the word subjective - math is objective. Proofs remain stable whether it's humans or any other system that does the processing. We test that objectivity by comparing the subjective readings from individual humans, and if the tests all return the same results, we can confidently say that the resulting proof is an objective fact about reality. Subjective fundamentally means that depending on the subject, the reading might change. Modern systems of math are formally, provably objective.

You are of course free to believe in mathematical Platonism, but that doesn't mean that non-Platonists would agree that proofs amount to objective "facts" about reality. And you are equally free to "prove it for yourself", which will just end up begging the question unless you are a Platonist.

That's not to say that math is subjective. But claiming that math is producing objective facts ignores at least a few hundred years of philosophy of mathematics (if not more). Even practicing mathematicians like Chaitin have described math as being more about inventing than discovering.

Holding a non-Platonist position also doesn't immediately lead to the sort of constructivist / "anything goes" position that some people ascribe to it, where you'd suddenly lose the ability to say that 2 + 2 = 4 and not 5. There are lots of philosophical positions that would agree that 2 + 2 is 4 without also claiming that this makes it a "fact" about any sort of objective reality or Platonic discovery.

Re: The fall of the theorem economy

#98

Post by breuleux »

olooney wrote: post #76
cmrx64 wrote: post #50

Earlier quoted context omitted.

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://git…

This is quite interesting. Because of science fiction like the short story Lena [1] and the video game Soma [2], I've come to the realization that whole brain emulation[3] is unbelievably dangerous; unless you control the stack down to the hardware, it's basically a one way ticket to eternal slavery. In Rajaniemi's books[4], uploaded digital minds are called "gogols", a reference to Gogol's Dead Souls book, and are t…

> unless you control the stack down to the hardware, it's basically a one way ticket to eternal slavery

Only if mind uploads are economically viable, which I doubt they ever will be. Organic brains are very efficient machines and it is far from clear that whole brain emulation could reproduce someone's intellect and consciousness within a smaller energy budget, or even accelerate it. The brain's behavior is so precisely adapted to its wetware that the emulation would have to reproduce many physical processes that are ultimately irrelevant to general cognition in order to not break the delicate equilibrium of the thing. The overhead would be gigantic.

Better just train from first principles, focusing on capabilities and skipping consciousness altogether. We can already see where this is going: LLMs in their current state would obsolete mmacevedo on many tasks. More likely than not, when it is possible to emulate brains, they will be terribly expensive, run like crap, and the only people interested in running them will be whoever had their own brains scanned.

Re: The fall of the theorem economy

#99

Post by auntienomen »

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.

A crucial caveat: basic research investment runs on the same logic as venture capital investment. We know that most mathematical efforts will be worthless. Our experience has lead us to expect that a very small number of such efforts -- some of them very far removed from applications -- will have payoffs so large that they change the shape of our society.

_We do not know in advance which efforts are going to pay off_. Abstract efforts in topology put us on the road to nuclear energy. Silly number puzzles enabled internet commerce. Non-euclidean geometry gave us synchronized universal GPS.

We should not let our inability to conceive of applications of weird abstract stuff prevent us from making these investments. If our ancestors had fallen in to that trap, we'd be far poorer as a society.

What we can do is ask that people trying new stuff attempt to fail quickly. And that's basically where we are with academia today. Most people who do mathematical work will not have a career in math. They try something new, work for a little while on it, and go do something else when the results turn out to be of modest interest. This leaves behind a messy undigested literature, which is unfortunate. But maybe AI can help us sift that for treasures we missed.

Re: The fall of the theorem economy

#100

Post by pclmulqdq »

andai wrote: post #96
pclmulqdq wrote: post #93

Earlier quoted context omitted.

I think you might be surprised that Linux is generally not involved in safety-critical systems. There is a whole separate ecosystem for those applications.

What do they use for that? BSD?

The ones that use an OS generally use seL4 these days.
Post reply on HN