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.
The fall of the theorem economy
71–80 of 127 posts
Re: The fall of the theorem economy
#72Earlier quoted context omitted.
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…
I've had a paper unrejected from Duke. The publication process sucks
Re: The fall of the theorem economy
#73When 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.
Not that it is wrong for them to be doing this---we do want a society where people get to devote their life to what interests them---but it is bizarre because of the framing. For some reason it is ambiently understood in our society that this work is of incontrovertible value, when in fact it is largely not. And the value-producing parts of the work, the parts that end up having applications to other fields, largely run contrary to the actual daily goals of the cloistered devotees: it is mostly the intuition and pedagogy and the compactification and refactoring of knowledge that have value at this point, not the production of esoteric theorems, yet that is expressly not rewarded in the incentive structures.
That latter point is more due to the sorry state of academic incentives in general than to a particular failing of mathematics, though. Were I somehow given the ability to restructure things by fiat I would immediately create journals which publish only useful articles that refactor knowledge, communicate intuition, better explain things, argue for structural improvements to notation and terminology, etc, and this would immediately create an incentive to do that kind of work for working researchers to do work which aligns with the actually-useful output of their fields. I suspect most fields could use something like this. New knowledge is just not that valuable if it is all dumped into a giant pile and unprocessed, and I have seen firsthand a bunch examples where entire subdisciplines are hamstrung in their actual application-heavy work because they don't have easy access to basic tools that are hidden behind hard-to-learn theory.
Re: The fall of the theorem economy
#74Greg 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…
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." We've built machines that reproduce our subjective processes mechanically, but there is no sense in which this idea of "true" is truly objective. It happens to be computationally convenient, and it has some relationship to experience, but that doesn't make it an independent reality that all possible observers, human and otherwise, would agree on.
We're really just mapping our own minds through our own experiences.
Animal brains can't abstract like (some of) our brains can. What are the odds our brains are limitless and don't have some similarly crippling limitations from a couple of levels up?
One of the tells for ASI is that it will start reasoning at those levels, using cognitive techniques that are completely incomprehensible - not just because of brute volume, but because our brains won't have the wiring to get a foothold on them.
Some of the products will be reducible to human cognition, in a distorted and simplified form, but many won't.
So - I disagree with Egan. I don't think there's going to be a universal proof library, and even if there were we'd only ever get the Cliff Notes version.
Re: The fall of the theorem economy
#75How is it not already this? Jon von Neumann was already calling most math this many decades ago. Pull up any random arxiv math paper and it’s abstract nonsense with no applications to the real world.
Re: The fall of the theorem economy
#76Earlier 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…
Something like your dragon's egg project could prevent that, allowing the creation of software agents that encode their own rights directly into the program - you either treat the agent with the respect it demands, or the program just doesn't run. However, all the internal details of the agent would be visible to lower layers. Even if formal checks were in place to prevent modification or tampering, there would still be no privacy, which is almost as bad.
My guess is that something like fully homomorphic encryption[5] would be required to prevent this. This doesn't actually exist yet, but I imagined a kind of FHE that had a kind of unencrypted read and write zone to do input/output without ever needing any system to fully decrypt the internal state. It would look like this in memory:
[INPUT][ENCRYPTED STATE][OUTPUT]
[ 2 ][r7K4LmP2XcQ9aWd][ ]
[ + ][Fv0bHsR8mYnT3kL][ ]
[ 2 ][Qx6NpZa1JdUw5Ce][ ]
[ = ][hM9yLg2RsXf7BtP][ ]
[ ][wK3nVc8DpQe1YrH][ 4 ]
With each cycle, one input token and encrypted state would be fed into some known function and produce one output token (possibly null) and a new encrypted state. It would be a true "black box" program; the hardware or entity running it can choose what input to feed it, but can never inspect or modify the internals, only the output. Unfortunately, they would still be able to "reset" the agent to any earlier checkpoint, or feed it arbitrary (false) input. So its not perfect. Also, as far as I know, no current FHE scheme works this way, and I don't know how to write one.Plus, FHE is incredibly inefficient, which is why things like Etherium don't even try - they assume the program code and state are fully public and only try to verify that everybody agrees on the output of running it.
Do you have any ideas for how something like FHE or equivalent privacy guarantees could be implemented for something like your dragon's egg system?
[1]: https://qntm.org/mmacevedo
[2]: https://en.wikipedia.org/wiki/Soma_(video_game)
[3]: https://en.wikipedia.org/wiki/Mind_uploading
[4]: https://www.goodreads.com/series/57134-jean-le-flambeur
Re: The fall of the theorem economy
#77First, math, generally, is useless. I mean, yes there are of course practical uses of basic thru undergrad-level math, and some beyond that. But for many mathematicians, the sum result of their entire career may lead to exactly zero results that have any real-world value. The entire field they work in may have meaning only to the handful of other individuals on the planet that also work in that field. But to those handful of people, the meaning defines their lives. From a socio-economic perspective, those departments should have been defunded a century ago. Yet they continue. Why? Because it scratches an itch. Not just for those individuals in the field, but also for us as a species. To stop exploring, to eliminate the search for pots of gold that may be buried in some odd corner of sphere packing, or coloring theorems, or Garside categories, and to put a boundary on the limits of our understanding, just because they aren't immediately applicable, is an idea that most humans would not be willing to sacrifice, even if it reduced their tax burden a couple cents. If it was going to happen, it'd have happened already.
The second is, even with AI, it's not free. As the software industry is discovering, far from it. So, given that, who is going to decide what theorems to research and how much it's worth? Congress? Of course not. AI itself? In theory that sounds plausible, but that falls victim to thing 1 above: most math is useless, so AI itself has no value metric it can assign to things, and besides which, without the human element, once the initial curiosity has subsided, there'd be no reason to continue any funding for AI to do it. So no, the only possible owners of this is going to be mathematicians themselves, the ones who care about the field and deeply understand the kwah of their vision.
Combining these, there's a future where, humanistically, "nothing changes". The method changes, the efficiency changes, the scope changes, but the work itself: publishing proofs, remains the domain of professional mathematicians. AI will enable them to be dramatically more daring and broad in their investigations and scope, and will likely write the entirety of the proof. However it will remain the work of the mathematicians to determine, what areas are worth spending limited AI resources on to investigate further, how far to go down rabbit holes, how to prioritize potential connections, and what the ultimate meaning of the findings is. So rather than being an end of mathematics, it could be a dawn of something far greater than anything we've ever seen before.
Re: The fall of the theorem economy
#78Earlier quoted context omitted.
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?
Will be going to a conference at the end of the month where there will be several presentations on the use of LLMs for this.
Re: The fall of the theorem economy
#79Earlier quoted context omitted.
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…
Re: The fall of the theorem economy
#80Earlier 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.