Does the the (,1) conjecture paper in annnals of Math say 7 years between submission and acceptance? Insane
These stories are common in math, e.g. these recently happened to me, a lowly mathematician: 1) Two and a half years with no reply from a journal (not even to emails I sent that I'd like to retract the paper so I could send it somewhere else). Then suddenly they tell me the paper is accepted. 2) One year with no reply. Then, my "anxious" collaborator sends them countless emails and gets redirected from person to pers…
The fall of the theorem economy
51–60 of 127 posts
Re: The fall of the theorem economy
#52Earlier quoted context omitted.
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://git…
Re: The fall of the theorem economy
#53Greg 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…
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.
Re: The fall of the theorem economy
#54Earlier quoted context omitted.
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.
Edit: one better example from modern physics - the path integral formulation, used in both string theory and other areas of QM/QFT, is not fully formalized and formally proven to work. Also, a more concrete example of a widely used but actually still unproven conjecture in string theory is the famous AdS/CFT correspondence.
Re: The fall of the theorem economy
#55I 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…
The motivation behind all this is less "haha I want profit" and more "billions of people need chairs, approximately none of them care about the craftsmanship, so it's in our best interest to make furniture in the most resource- and labor-efficient way possible". Even if the state subsidizes the production of handcrafted chairs, the population is the poorer for it on a resource allocation basis, because we now need a million artisanal chair-makers instead of a bunch of factories.
Re: The fall of the theorem economy
#56People 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
#57This kills me, it is correct, but misses the forest for the trees. Yes, mathematics is a discipline of understanding, but an insular one. The entire field is about trying to understand, but the discipline does not try to be understood. No, that is "your job, not theirs" and that is why this discipline is struggling, struggling in a culture that can barely communicate without emotional morons destroying any constructi…
Eh? I thought this was the main thrust of the argument: Mathematics has in fact always prized conceptual advancement and understanding over proof, despite presenting itself internally and externally as rewarding the latter. The author calls what he’s proposing “rebranding a plurimillenial project”.
Re: The fall of the theorem economy
#58When 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 create ever more abstractions and get lost in solving puzzles on how these abstractions logically relate to each other. But since these abstractions don't have any relevance outside of pure mathematics, it's an entirely self-referential game, like chess. Except that nobody confuses being a professional chess player with being a noble researcher.
Even in philosophy, at least analytic philosophy, that issue of getting lost in your own abstractions doesn't really exist. Because analytic philosophy doesn't analyze its own concepts, it analyzes the concepts that already exist in natural language. Like truth, knowledge, probability, causation, belief, desire, consciousness, rationality and so on. These concepts come from outside of philosophy, and they have independent relevance for non-philosophers.
In contrast, pure mathematics seems to be the part of mathematics that only has relevance to pure mathematicians. Similar to how a game like chess has only relevance to chess players, not to anything entirely unrelated to chess. But again, people who are into mastering some game or sport are fully aware that what they are trying to master is a self-contained game, or sport, not something that increases the amount of human knowledge beyond that.
Re: The fall of the theorem economy
#59Earlier 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…
Re: The fall of the theorem economy
#60Earlier quoted context omitted.
Science is not about results, it is about the transmission of knowledge. So long as those AI-"sciences" are just inside AI, they are "engineering", not science. I am not dismissing engineering (it moves the world we live in), just trying to clarify what science is. Applied fluid dynamics works like that: noone has ever really "verified" that the finite-element method applied to some specific model does converge
So what I’m most curious about is this: if there are axioms and proofs so enormous that a human could never prove them in a lifetime, but a machine can, does that make it engineering? That’s the point I’m really wondering about. I mean, what if a human could follow every single step of the process in principle, but the sheer volume is so vast that a human can never see the whole thing—would that be engineering? But I…
The details could be painful but having a birds eye view is always possible?
And having a machine compress it for human consumption, sounds very plausible (and which I think of as engineering)