Comment by olooney
1 day ago
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, intuition, and insight.
One of the most fruitful approaches in mathematics is to flip back and forth between geometric and algebraic views of a problem. I think this works so well because these are actually handled by two different parts of the brain on a physical level; spatial reasoning is separate from language processing. Cytoarchitecture shows these regions have different "textures;" the local details of the way neurons are wired together are simply different in these different regions of the brain, in the same way a CNN and a transformer have different topologies. Thus, by flipping problems from geometry to algebra and vice versa, we're able to bring an entirely different cognitive style to bear on a problem. For example, the proof of Monge's Theorem by moving to 3D and visualizing not three circles, but three spheres sitting on a table with a book on top of them and then pointing out that the intersection of two planes is a line. What is pages of unintuitive symbol pushing turns into something a child can understand. Going the other way, things like the angle addition formulas or the quadratic formula, which are quite hard to prove geometrically, become quite simple if you use a little algebra.
Current-gen LLMs are still relatively weak at visual reasoning; see the Vision Language Models are Blind paper, for example, or the ARC-AGI benchmark. So that's one way humans can stay ahead of the agents, at least for now.
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." 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.
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 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.
> 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.
2 replies →
> 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.
4 replies →
>> 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.
I thought CyC was a heroic attempt doomed to failure but not because it was rule-based. IIUC it used (custom) first-order logic and that's as expressive as expressive can be. There's no reason why a sufficiently large first-order rule-base could not capture every human concept. There's also no reason why "trillions of parameters" would be any better at that than "trillions of rules". It really comes down to what those rules or parameters are encoding.
What doomed CyC to failure, I think, is that its rule-base was mainly manually encoded. CyC was basically the world's biggest ever expert system, and it came with the biggest ever knowledge acquisition bottleneck. I don't think there's any magick to my claim, either. Human minds can't handle the complexity of a few dozen, let alone a few million, interconnected rules without making mistakes. It's hopeless trying to create such a system by hand. From a certain point onward you have no idea what your system can and can't do, because you have no idea what information it has and hasn't access to.
But it's hopeless trying to create such a system by chance, too, i.e. by feeding the system all the data we can find in the hope that it will somehow spontaneously acquire all the knowledge we want it to; much of which is not even in the deductive closure of the information we feed it (and LLMs are not deductive inference engines, unlike expert systems).
Some kind of automatic knowledge acquisition is clearly a much better idea than manually coding rules by hand, but I don't see how peta-scale machine learning has moved the needle much either. We're still stuck with systems that can do some spectacular things but can't do simple things. Or things that look simple to us.
> Our concept of logic based on our subjective experience of "truth."
The idea that we experience objectivity subjectively, thus there is no objectivity, seems like an ultimately nonsensical and self-defeating sleight of hand to me.
>> Animal brains can't abstract like (some of) our brains can.
You mean they can't come up with mathematical abstractions? That's right of course, but they seem perfectly able to "abstract" in the sense of drawing general rules from specific observations. For example, I noticed recently how my cat friend was happy to exit and enter the house from either of two doors and a window as the opportunity presented itself (i.e. depending on which one was open at the time he wanted to get in or out). E.g. I just happened to open the window and he hopped onto the ledge and out into the mystery of the night, entirely unaided by human hands or voices.
That's an abstraction: one door is like another door and they're both like a window. Both things lead in and out of the house and they can be open or closed at different times. If one is closed another may be open. Something like that, obviously I have no idea what concepts, exactly, he has in his head. And btw, "in", "out", "house", etc are also abstractions, so a house in the UK is like a house in France, or like one in Italy, or one in Greece: that's where the human things are; I guess.
I think it's important to understand this about animal intelligence, that it is very much capable of broad generalisation and abstract thought. Absolutely not to the same degree as humans because we got language and that probably comes with a whole other level of ability for abstraction and reasoning, but I don't believe it's possible for an animal to survive in the physical world if it can't go from the concrete to the abstract, the specific to the general, to some extent.
You mention ASI so I'm comfortable making this comment which is about AI, without feeling I'm hijacking your conversation. I think one only begins to understand how powerful the animal brain is, and how overlooked (in AI discourse) its ability to form such broad, useful abstractions that allow animals to navigate the physical world autonomously while setting and pursuing their own goals, when one tries to reproduce the same behaviour artificially, in computers.
Like you say, yes, maybe when we stop understanding what our computers produce, it will be because they moved a level up from where we are, as ASI. Maybe there is such a level; maybe there isn't. For the time being, there is no artificial system that can spontaneously move in the physical world as easily and effortlessly as my cat friend can (and he's a graceful animal; really, much closer to an African wildcat than its domestic descendant). If you want an AI system to understand the difference between "in" and "out" and that there are doors and windows that connect the two you have to somehow explicitly feed that information into it, either by hand-coding (e.g. the PDDL models used in Planning and Scheduling) or by training on carefully chosen examples of those concepts (as in machine learning), or at least some kind of objective that will lead the AI to develop them, or develop similar concepts (as in Reinforcement Learning). We're still very far from the capabilities of the animal brain.
Also, may I quibble about the fact that our brain, too, is an animal brain?
> 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.
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 :)
https://archive.bridgesmathart.org/2014/bridges2014-111.pdf
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.
1 reply →
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 blind to visual reasoning. They really struggle reasoning with Floer Heegard diagrams for example.
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://github.com/emberian/svenvs
I took a look at dregg, I like the idea for an README-LLMS.txt. It seems like a good way to not only communicate to other LLM users (which we should be thinking more of doing effectively) but also I can imagine it’s helpful for your own new sessions with an LLM to arm them with proper context.
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 treated as malleable property with no rights whatsoever, edited to be hyper-fixated on specific tasks, and run in bulk to power the empire of just a handful of elites.
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:
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
[5]: https://en.wikipedia.org/wiki/Homomorphic_encryption
2 replies →
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.)
I believe the architecture for convolution neural networks were directly inspired by how vision works and some of the core design choices map onto real features of the visual cortex.
That's fair. Two things that are heavily underrated are architecture and encoders
> 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.
This feels like a non sequitur
Everyone, including blind people use their visual cortex to play chess
AI only works in the parts of reality that have been defined into granular atomic units. Which is by definition an approximation of reality.
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)
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 a cup to be a donut). Thurston's Geometrization Theorem outlines the 8 geometries that a closed 3 manifold can have. Topos theory studies space in a very general setting that connects logic to it. You may like the books "The Shape of Space" and "Surreal Numbers". The Numbers 1, 2, 3 is not the only in which mathematicians abstract reality.
3 replies →
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"