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.
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 geometry does not logically extend to human brains lacking the wiring or hardware for systems of thinking that are beyond our capacity.
We do have limitations in scope, in both memory and speed. Both of these can be overcome with augmentation and interfacing with UI or direct neural connections, and intuitive, comprehensive, deep understanding of systems can be learned.
You could very well know the underlying theory of how your 8086 processor works, how it interfaces with all the elements of the motherboard, how electricity and physics interact at each level of abstraction from transistors to the pixels representing the spreadsheet you're using to do your taxes. You won't be able to simulate that in your head to any significant degree of resolution.
We will require similar levels of system thinking to acquire intuition and deep understanding of complex new theories and models. AI can assist with that by providing UI for useful levels of abstraction and segmenting theories into chunks we're capable of consuming. BCI and augmentation will definitely allow a more total, holistic understanding, and I think it's the augmentation path that will keep us competitive with AI.
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. That's how and why things are the way they are; if they weren't, people would experience radically different individuated realities, or there would be clusters of results shared across some measurable characteristic of the universe. That's not the case, so you can confidently say that the foundations of our math and logic are sound.
You can even prove it for yourself - the abductive chain of logic that allows you to contrast your own consciousness and subjective experience, determine that it comes about because your brain is wired to "do" consciousness, like all the other humans, and compare your subjective reporting of phenomenal experience with all the other reporting of phenomenal experience, and achieve a ridiculously high level of certainty, in the Bayes sense, that you and other humans are conscious; from that footing, you can confidently navigate the rest of enlightenment rationality and formal logic and mathematics.
At any rate, Egan's mistake is one of kind, but of scale - I am certain that as we formalize and start creating any sort of universal proof library, we will find that useful and interesting things are of necessity a tiny fraction of all possible valid formulations of any framework of logic and math. Crude attempts, such as OpenCyc and other formal ontological reasoner systems, would need trillions of low level rules to have a rough approximation of the world model as complex as that of a human child. AI with trillions of parameters could probably start getting to the point where there's parity with human scale, but even if you turned the entire planet earth into computronium and turned it toward the task of understanding all the theory and science of the universe, there will always be far more left to explore and understand than the sum total of all knowledge.
All that to say, humans will be fine with ergonomic interfaces that map to human capabilities, even for extraordinarily complex and hyperdimensional systems.
How could this ever be tested/falsified?
It feels a bit like "there is no idea we cannot think of."
> 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.
I continue to think extensively about truth, but currently I disagree. There are senses in which truth can be well established, and those are quite important. I think the basic essence of truth is how we can make a statement (or a model), and have a system for measuring either reality or just mathematical/abstract objects, and verify the statement through this measurement.
As you note, for current mathematics it seems like all of it (all things we call mathematics at the moment) can in principle be formalized in a logic that is machine-verifiable, that is, essentially objective. We're well on our way to demonstrating this for most of mathematics (already most undergraduate curriculum). I think that's because almost the definition of math is that is has this property: in my opinion mathematics has distinguished itself as being the "science of certainty" as applied to language and abstract thought. The way this certainty is achieved is through agreeing on some fundamental assumptions and how certain rules (which are also assumptions themselves) can act on those assumptions to constitute theorems. Theorems are not necessarily physical-world truths/properties (at least not in a simple way in the universe we currently inhabit), you can study alternate physical laws that aren't compatible with our (approximately) Newtonian world, for example. They are logical/abstract-world truths that result from your assumptions. Pretty much by definition (and in a somewhat limited), then, mathematics (at least as far as things like truth of theorems in certain axiomatic systems) is inherently objective, machine-verifiable even.
What's left to be subjective, I would say, isn't really the notion of truth in mathematics, it's which assumptions we should elect to investigate, and which theorems should we elect to prove within those assumptions. Some mathematicians also have some notion of "absolute truth", and tend to reject systems of assumptions (axioms) that don't match what they regard as true -- basically going in reverse and searching for assumptions that can enable a theorem (which effectively acts as an additional assumption).
This activity needs certain basic premises to make sense, for example if a set of assumptions proves that a property holds, and also that a property doesn't hold; or if they predict a certain value X is the result of a dynamical model, and also predict that a different value Y is the result of such a model/equation, then we reject those premises. In a certain sense we are most interested in premises that have, even if a very weak, correspondence to reality.
I think it's more informative to recognize that it's not that everything is subjective[1], it's that everything is experimental. For example, the claim above that measurements and correct predictions can only have a singular valid value, corresponds to our experience with reality, in which in a certain way is singular; there are not multiple realities; objects have definite positions. Even if you think of quantum mechanics, in which we may say particles follow a distribution instead, we still say then there's a singular distribution a particle might have at any single time. Logic itself isn't random, it's connected to empirical observations about reality, which tends to increase the chance that conclusions for logic (which is made to share some properties with reality) tend to be valid in the physical world, of course often dependent on what additional statements you pile on top.
There is also another interesting lens that mathematics is artistic (and I think this will become increasingly important) -- making maths and learning maths is a kind of satisfying cognitive activity in its own right, and we also tend to chose what to explore mathematics on those grounds (in fact historically, pre-18th century say, this might be one of the main drivers of mathematical development, I believe[2]). But of course this is again just a reflection of the actual real properties of human cognition, and also this interest and satisfaction often becomes connected, if sometimes faintly, with the ability of math to represent reality (in a particularly satisfying way) and its objects of interest (for example patterns in nature). Another description for this aspect is maths as being hobby-like, about solving puzzles, or like a (hopefully enjoyable) game.
Note that for this particular "game", the objectivity (or if you prefer, machine-objectivity or consensus-machine-verifiability) of the rules and their application is a significant bonus, it makes the game much more interesting, increases its potential when everyone can agree and the rules and not "capricious" (simply dependent on whims of other people and judges); this gives practitioners safety and security and enables a wide social reach -- most games strive to have objective rules.
Arguably this kind of activity is valuable for the cognitive and subjective development of people that has lasting importance.
> 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?
Well, this happens sometimes. In cases where there are phenomena like universality. For example, in any computation machine model (state machines, pushdown automata, etc.) has limitations that we can say makes them less powerful then Turing Machines. But then Turing machines can simulate any other machine, becoming a kind of ultimate or last stage (at least in terms of abstract capability) machine. It may be that our cognition has some bounded universality properties (I think it's likely it does).
---
In summary, I still think mathematics has a lot of human potential in terms of (1) high level human guidance, (2) an internal artistic/subjective sensibility to the subject, (3) safeguarding human understanding of the world and associated individual intellectual development.
[1] Again, I just argued that there is a strong sense in which for example mathematics isn't subjective at all, but sure I do believe in a weak sense everything is subjective in the sense that everything is known or filtered or sensed through our minds which have limitations and aren't simple deterministic machines.
[2] For example, I believe for the Greeks geometry was intimately connected to philosophy/aesthetics (e.g. Platonism) and very little to applications. In ancient times and middle ages maths developed a lot from astronomical observations that had some applications but I think were largely cultural and ritualistic. In the late middle ages European aristocracy would fund mathematics largely for its inherent interest as an intellectual activity, and many nobleman enjoyed mathematics as a past time and would challenge each other to puzzles. Japan had Sangaku, in which mathematics was made for fun, aesthetic purposes and possibly bragging rights. No one actually needed to build say spheres in obtuse constructions with certain radii :)
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"
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://github.com/emberian/svenvs
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
And you can't control the stack down to the hardware. Even if you are rich enough to fund a group of people to start from sand and end up at a simulation platform for you, you are also rich enough to have attracted enough attention that either one of those people could corrupt the platform, or someone may attack the organization to corrupt it with nation-state level resources.
No matter how you secure the computation, you can still corrupt the input and output streams. And as a $RICH_DYING_GUY it doesn't even matter if someone produces a proof of some software program somewhere's safety, because you have no way of knowing that it corresponds to the software that is running on the hardware.
Before you go with "yeah but I could...", I agree that a single individual could theoretically develop the skills that might permit validation of any particular small portion of the process. What I'm saying is no human can develop the skills to be able to validate the entire stack from top to bottom, hardware and software, in way that it couldn't be corrupted, especially in a world of more and vastly smarter AI agents. The probability that you will truly own and have full sovereignty over your computational substrate is zero.
(Whether I have full "sovereignty" over my current computational substrate would be a definitional matter, but I'm fairly confident that at least nobody else has the ability to just reach in and start mucking with neural weights directly or something.)
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.
AI so far has almost no way to interact with non definitional non quantitized reality. So novel space is still deeply out of its domain.
Recombination of known spaces it will probably continue to make pure war dial breakthroughs in though.
I wish we’d tackle a post Mathematics world where we’d account for number theory not being accurate abstraction of reality (I.e. there is no 123 only 1ish 2ish 3ish with many sub properties of any given unit we are ignoring)
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 understand because it would need to verify in reality through observation if the new units of granularity align with outcomes.
This is of course possible to some degree but runs into a paradox if it is a portion of reality than is irreducible or works in a fundamentally “non granular” way.
I have no proof of this but of course already at the quantum level we are running into to “non granular” realities
Chess does not require a visual cortex to play. People have been playing by mail with algebraic notation for centuries.