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

101–110 of 127 posts

Re: The fall of the theorem economy

#101

Post by gjm11 »

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.

A convolutional neural network is really somewhat like a visual cortex. Obviously AlphaZero doesn't literally have a visual cortex -- actual literal visual cortices are features of actual literal brains made out of meat -- but it definitely has something that does something akin to visual processing, in a way that LLMs don't. Or at least they don't on the face of it; maybe well trained large enough LLMs have effectively implemented something kinda-visual-cortex-like on top of the transformer architecture.

(I bet there are people at all the big AI labs working on ways to incorporate something more CNN-like into LLMs somehow.)

Re: The fall of the theorem economy

#102

Post by atq2119 »

Terr_ wrote: post #94
observationist wrote: post #85

Earlier quoted context omitted.

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.

It could potentially be falsified by an encounter with really weird aliens.

But I find it quite plausible because it feels like it's fundamentally "just" a restatement or a minor variation of the Church-Turing thesis.

Re: The fall of the theorem economy

#103

Post by observationist »

Terr_ wrote: post #94
observationist wrote: post #85

Earlier quoted context omitted.

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.

In principle - if you're able to scale appropriately, using technology to augment capacity, then in principle, there's no abstraction for which we lack the capacity to comprehend, because calculation is calculation. Turing Computers can calculate anything which can be calculated given enough time and memory. Brains are Turing complete.

It's not just a tautology, it's a feature of the universe- if it can be computed, it's comprehensible. Even quantum physics is just computation - truth tables and counterintuitive operators interacting over time in ways that are strange to our embodied norms, but nonetheless following rules and limits strictly defined by mathematics.

But again, that's in principle. It might be completely impractical - taking a million years for an individual human - to hold a particular idea in their head, while an advanced AI can have such thoughts many times a day. Such things would remain mysteries, but in principle, an augmented human, or a series of interfaces with the relevant abstraction levels of such an idea, theory, or system, would in principle give us comprehension.

In practice, we'll never run out of mystery or ignorance or mistakes.

Re: The fall of the theorem economy

#104

Post by tsunamifury »

ged_throw_382 wrote: post #95
tsunamifury wrote: post #87

Earlier quoted context omitted.

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.

Seems easily provable as 1 does not contain information about blue. It’s useful but not complete.

Re: The fall of the theorem economy

#105

Post by [deleted] »

atq2119 wrote: post #102
Terr_ wrote: post #94

Earlier quoted context omitted.

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

It could potentially be falsified by an encounter with really weird aliens. But I find it quite plausible because it feels like it's fundamentally "just" a restatement or a minor variation of the Church-Turing thesis.

[deleted]

Re: The fall of the theorem economy

#106

Post by radokirov »

andai wrote: post #48
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.

It is because you can precisely define what would make the whole mathematical endeavor collapse (not following the rules of logic or showing inconsistency), while even defining precisely what would be undesirable for software requires bringing in the whole physical world. If you can't define the outcome you want, you can't have rigorous standards to follow.

Re: The fall of the theorem economy

#107

Post by vatsachak »

tacomonstrous wrote: post #72
vatsachak wrote: post #51

Earlier quoted context omitted.

I've had a paper unrejected from Duke. The publication process sucks

How does unrejection work exactly?

You get a fields medalist to email the reviewer to say "wait that paper is really good actually"

Re: The fall of the theorem economy

#108

Post by 2snakes »

UltraSane wrote: post #83
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…

Math is the least subjective thing. Logic has nothing to do with subjective experience. Are you aware of Lean 4 and mathlib?

Said like a true formalist. Mathematical insight is a pretty creative act of consciousness. The formalization of it tends to come after.

Re: The fall of the theorem economy

#109

Post by 2snakes »

chongli wrote: post #91
whack wrote: post #88

Earlier quoted context omitted.

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

It is like an idiot savant, just really widely read enough to seem creative when it tries some obscure thing. see First Proof though if you haven’t.

More divergent type than convergent like ramanujan.

Re: The fall of the theorem economy

#110

Post by UltraSane »

2snakes wrote: post #108
UltraSane wrote: post #83

Earlier quoted context omitted.

Math is the least subjective thing. Logic has nothing to do with subjective experience. Are you aware of Lean 4 and mathlib?

Said like a true formalist. Mathematical insight is a pretty creative act of consciousness. The formalization of it tends to come after.

You have a point about insight and creativity but I feel you are discounting the value of formal proofs too much. Modern math has a kind of reproducibility crisis in that the number of people who can actually verify recent proofs is often less than 10. There are thousands of proofs that were verified by a few people who are now dead. Should we consider them to still be proven?

Most recent proofs are just as much of a black box to nearly all mathematicians as a 200,000 line Lean proof is.

Post reply on HN