7 ms·

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

by olooney 3mo 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.

dkural 3mo ago
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.
- cmrx64 3mo ago
  i got so inspired by reading diaspora this year that i instantly started working on some polisware. cipherclerk operational: https://github.com/emberian/dregg 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 https://github.com/emberian/svenvs
  - appplication 3mo ago
    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.
  - olooney 3mo ago
    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: [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 https://qntm.org/mmacevedo [2]: https://en.wikipedia.org/wiki/Soma_(video_game) https://en.wikipedia.org/wiki/Soma_(video_game) [3]: https://en.wikipedia.org/wiki/Mind_uploading https://en.wikipedia.org/wiki/Mind_uploading [4]: https://www.goodreads.com/series/57134-jean-le-flambeur https://www.goodreads.com/series/57134-jean-le-flambeur [5]: https://en.wikipedia.org/wiki/Homomorphic_encryption https://en.wikipedia.org/wiki/Homomorphic_encryption
vatsachak 3mo ago
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.
- TimorousBestie 3mo ago
  > 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.
  - hlynurd 3mo ago
    This feels like a non sequitur
  - vatsachak 3mo ago
    Everyone, including blind people use their visual cortex to play chess
- tsunamifury 3mo ago
  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)
  - dkural 3mo ago
    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.
TheOtherHobbes 3mo ago
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.
- UltraSane 3mo ago
  Math is the least subjective thing. Logic has nothing to do with subjective experience. Are you aware of Lean 4 and mathlib?
  - 2snakes 3mo ago
    Said like a true formalist. Mathematical insight is a pretty creative act of consciousness. The formalization of it tends to come after.
    - UltraSane 3mo ago
      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.
playorizaya 3mo ago
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"

by olooney 3mo ago

dkural 3mo ago

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.

cmrx64 3mo ago
i got so inspired by reading diaspora this year that i instantly started working on some polisware. cipherclerk operational: https://github.com/emberian/dregg 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 https://github.com/emberian/svenvs
- appplication 3mo ago
  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.
- olooney 3mo ago
  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: [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 https://qntm.org/mmacevedo [2]: https://en.wikipedia.org/wiki/Soma_(video_game) https://en.wikipedia.org/wiki/Soma_(video_game) [3]: https://en.wikipedia.org/wiki/Mind_uploading https://en.wikipedia.org/wiki/Mind_uploading [4]: https://www.goodreads.com/series/57134-jean-le-flambeur https://www.goodreads.com/series/57134-jean-le-flambeur [5]: https://en.wikipedia.org/wiki/Homomorphic_encryption https://en.wikipedia.org/wiki/Homomorphic_encryption

vatsachak 3mo ago

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.

TimorousBestie 3mo ago
> 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.
- hlynurd 3mo ago
  This feels like a non sequitur
- vatsachak 3mo ago
  Everyone, including blind people use their visual cortex to play chess
tsunamifury 3mo ago
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)
- dkural 3mo ago
  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.

TheOtherHobbes 3mo ago

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.

UltraSane 3mo ago
Math is the least subjective thing. Logic has nothing to do with subjective experience. Are you aware of Lean 4 and mathlib?
- 2snakes 3mo ago
  Said like a true formalist. Mathematical insight is a pretty creative act of consciousness. The formalization of it tends to come after.
  - UltraSane 3mo ago
    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.

playorizaya 3mo ago

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"