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.
> [...] 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.
Chaitin's work (including in his own opinion) moved the philosophical needle on maths towards "discovery" and away from "invention".
Indeed, his philosophy on the nature of mathematics is closer to "discovery", as in physics, than "invention" as in arbitrary game of rules and symbols (Hilbert) or language game (Wittgenstein).
I forget who said, "If you keep asking why, eventually you end up in the mathematics department." Calling it Platonism is a misunderstanding of how physics (and chemistry, biology, and the rest) emerge from mathematical structures and relationships that are more fundamental.
In principle - if you're able to scale appropriately, using technology to augment capacity, then in principle, there's no abstraction for which we lack the capacity to comprehend, because calculation is calculation. Turing Computers can calculate anything which can be calculated given enough time and memory. Brains are Turing complete.
It's not just a tautology, it's a feature of the universe- if it can be computed, it's comprehensible. Even quantum physics is just computation - truth tables and counterintuitive operators interacting over time in ways that are strange to our embodied norms, but nonetheless following rules and limits strictly defined by mathematics.
But again, that's in principle. It might be completely impractical - taking a million years for an individual human - to hold a particular idea in their head, while an advanced AI can have such thoughts many times a day. Such things would remain mysteries, but in principle, an augmented human, or a series of interfaces with the relevant abstraction levels of such an idea, theory, or system, would in principle give us comprehension.
In practice, we'll never run out of mystery or ignorance or mistakes.
You've made a grave assumption in treating this as a binary problem: comprehensible or incomprehensible. The truth is that this lies along a spectrum. I can "comprehend" a color which my eyes can't see but this is different than trying to comprehend red. Or as a variant, I can comprehend a color that I can't see naturally but if I go into a lab and they simulate those cones in very specific ways I won't ever be able to really imagine it. Seeing it will be clearly a different level of comprehension.
> In practice, we'll never run out of mystery or ignorance or mistakes.
I fully agree with this but also for some reasons unmentioned. Truth has infinite precision, a thing we will never achieve. Similarly my namesake showed there are limits to axiomatic systems.
> Brains are Turing complete.
And there are problems that can't be solved by Turing complete machines. That only means they can solve computable problems but there's plenty that aren't. Very famously the halting problem isn't. And in the real world there's many problems which are intractable. And some are more intractable than others
>> 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.
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.
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 :)
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?
"unless you control the stack down to the hardware, it's basically a one way ticket to eternal slavery"
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.)
> unless you control the stack down to the hardware, it's basically a one way ticket to eternal slavery
Only if mind uploads are economically viable, which I doubt they ever will be. Organic brains are very efficient machines and it is far from clear that whole brain emulation could reproduce someone's intellect and consciousness within a smaller energy budget, or even accelerate it. The brain's behavior is so precisely adapted to its wetware that the emulation would have to reproduce many physical processes that are ultimately irrelevant to general cognition in order to not break the delicate equilibrium of the thing. The overhead would be gigantic.
Better just train from first principles, focusing on capabilities and skipping consciousness altogether. We can already see where this is going: LLMs in their current state would obsolete mmacevedo on many tasks. More likely than not, when it is possible to emulate brains, they will be terribly expensive, run like crap, and the only people interested in running them will be whoever had their own brains scanned.
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.
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.
I know I failed to explain this correctly and was downvoted for it
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
That sounds a bit like the Gödelian argument against mechanism: reality (or even math) may contain systems that require stepping outside the current framework to formalize. A machine that can only work with current frameworks would be blind to these, except insofar that it can stumble across them by brute force.
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.
People 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 confidence that our battle tested software is correct, mostly. And we tell people that we will never be 100% confident that any software is bug free. But that's a slight lie: if we wanted such confidence, we would start using provers, and create bug-free software. That possibility exists, but it's just extraordinarily expensive.
Well, in math that's the only possibility, and we use it. And it is indeed extraordinarily expensive, but it's also the cheapest among the alternatives. The alternatives are 2: be rigorous and do these proofs, or be sloppy and allow bugs to creep in, and allow an entire school of math to collapse like the Italian school of algebraic geometry [1].
There is one more alternative. If a particular math theorem has some applicability, then you write a program and use it in real life. In time you eliminate the bugs as much as you can, and you get to the steady state of "virtually bug free". At that point you don't have a solid proof that the theorem is correct, but in general you don't really care. Because you feel that a formal proof is just a thing one would pursue for getting academic satisfaction only.
Your example of the Italian school is well taken, although most of their results were later proven to be correct in the right setting. Severi's example is particularly egregious and I think a major reason this became a thing is Severi's refusal to course-correct and accept that some of the results were not correct. It has echoes of Mochizuki, and I fear, once you dig deeper, some issues around the initial declaration of "We've proven the Classification of Finite Simple Groups". There were many genuine gaps, and a lot of lore taken for granted. The sociology around how this happened is interesting - rushing to announce that it was done was the major mistake, it took away almost all incentive to actually write up the proofs and take them through proper peer-review. Genuine mathematical work was falsely reduced to "write up".
I thought this comment would go in a slightly different direction: the body of work that is mathematics has plenty of “bugs”; proofs with mistakes or other human errors. Yet we take the body to be correct (we believe it “works”) in aggregate, partly because the intuition of mathematicians tells us that these bugs are solvable and don’t bring down the whole. Of course the less intuitive/more surprising/more central the statement, the stricter the standard for proof and more eyes that have walked through it.
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.
It is because you can precisely define what would make the whole mathematical endeavor collapse (not following the rules of logic or showing inconsistency), while even defining precisely what would be undesirable for software requires bringing in the whole physical world. If you can't define the outcome you want, you can't have rigorous standards to follow.
I think you might be surprised that Linux is generally not involved in safety-critical systems. There is a whole separate ecosystem for those applications.
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 foundations (e.g. all popular asymmetric encryption schemes are built on top the assumption that certain problems such as integer factoring are hard, for which there is no formal proof), or at least explore both possibilities for statements with unknown truth value (e.g. you can find lots of work that explores the consequences of P = NP and/or P != NP).
However, there is a major separation between math and programs that I think mostly invalidates your proposal - most math we're talking about here is simply not applicable directly to the real world in any way. It's only studied for the interest of mathematicians. There is no real world consequence for Fermat's last theorem, for example - it was just a really interesting to prove theorem. In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.
> 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 was simply an infinitesimal delta x, not merely notation for derivation), which were not not formalized until much later, after they had already fallen out of favor and had been replaced in formal math by the delta-epsilon limits-based constructions.
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.
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 Archimedian property. It took until the 1960s before Newton's notion of fluxions became rigorously formalized with Non-standard analysis. https://en.wikipedia.org/wiki/Nonstandard_analysis
Physics famously has a rather cavalier attitude toward formal rigor, but that's because the ultimate test is comparison with experiment. String theory shows what happens when that bulwark against error is missing.
> 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
But this is due to a "failure" of programming language progress. We've had formal languages for a long time (see Ada and SPARK) and we've simply failed to use them for most scenarios, instead regressing to imperative manually memory managed languages like C and then deriving from that branch.
One thing I've realized after quite a long life of learning and contemplation is that: mathematics and software are essentially the same thing. Add to that that it might be the case that Physics is the same thing too. We'll see on that one, but there are signs...
Incredibly thoughtful. This essay gives that very rare sense of being well reasoned, gods at forest and trees, and sitting atop a shit ton of domain expertise.
Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves.
Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match or surpass the collective output of the entire human scientific community the equation will change.
The intelligence is only one part of the story. People need to actually go out there and do experiments. Science is not only theory, but also experimental. The best science happens when experiments show that a previously held assumption was not true. Eg the Michaelson Morley experiment where the assumption of ether was disproved. While AI is an incredibly powerful tool, it does not replace the act of observation. Thus Im sure we will still have scientists in the future and some degree of open science. There are experiments out there that by nature of their complexity need massive public coordination (CERN for instance) which in turn benefits from openness.
What is going to suck though is the ladder for juniors. We dont start out by working on big ticket problems, but usually early career researchers solve really tiny problems in a cheap way. The lowest bar for a cash strapped PhD student would be to contribute to some new theory in some way even if the student doesnt have access to equipment.
Ah I see your point, I took the word science to mean bio, physics, chemistry, etc. IMO mathematics is a different discipline and not one Id consider a science, rather I see it as the language with which we express science.
If AI is somehow able to prove everything wouldn't it bypass Godel's incompleteness theorems?
It's not even just science. Anyone producing anything digital is now heavily incentivized to keep their wares away from the public internet, in a way we've not seen before. Drop any sample of your unique production online, and the AIs will obsolete you in days. That is a massive loss for people looking for inspiration and guidance.
> 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.
You know how I read new papers back in 1994? By going to the library, finding one in bi-annual publication list and requesting it through the University system. And it better be necessary because the uni had to pay both the catalogue and each reprint of an article. The access is most certainly easier today.
I did try asking one of the PIs whether they were doing it to demonstrate that it doesn't work in order to get paper authors to provide their real data but didn't get a reply.
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.
+-- 2mo before by sdfrew
| 4 points / 1 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=47862472
|
+-- 2mo before by fuglede_
| 3 points / 1 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=47891494
|
+-- 2mo before by mathgenius
| 2 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=47909751
|
+-- 2mo before by delis-thumbs-7e
| 15 points / 4 comments
| David Bessis on AI destroying mathematics
| https://news.ycombinator.com/item?id=47985962
|
+-- 1mo before by magoghm
| 4 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48084737
|
+-- 1mo before by cubefox
| 2 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48089716
|
+-- 1mo before by cubefox
| 5 points / 0 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48152469
|
+-- 1mo before by tmp10423288442
| 4 points / 1 comments
| The Fall of the Theorem Economy
| https://news.ycombinator.com/item?id=48214866
|
`-- this submission by varjag
58 points / 7 comments
The Fall of the Theorem Economy
https://news.ycombinator.com/item?id=48758048
The core thesis seems to be that the "real value" is not in producing/proving theorems, but in understanding them. AI might be good at producing and proving theorems, but it fails utterly at getting humans to understand them. Even worse, humans have no interest in working on theorems that have already been proven, so we end up with theorems that will never be understood by humans.
I can understand why this is a major concern for mathematicians. They got into their field because they love the beauty of mathematics, and the intellectual satisfaction of understanding non-obvious insights. But to put it crudely, this sounds like a you problem. As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology. And their practical applications in human life. I have zero understanding of the math behind cryptography, but I still deeply appreciate the practical value they have provided humanity.
If AI systems start churning out accurate theorem-proofs, and we are able to use those theorems to build things that improve human quality of life, it doesn't bother me one bit that those theorems have not been understood by humans. If this offends your aesthetics, you are certainly entitled to your opinion and your preferences, but that does not make it a societal problem
They got into their field because they love the beauty of mathematics… As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology
I have some sad news for you. 99% of the work mathematicians do has no immediate application, nor even an obvious path toward application in the near future. You mentioned cryptography, so for an example consider number theory: no apparent practical applications, going back thousands of years to the time of Euclid and earlier.
It’s been religion, philosophy, and recreation that have provided the motivations to study mathematics all these years, not applications. Applications have almost always followed long after the development of the pure mathematical theory. For number theory, that was the development of cryptography during WW2, millennia after the ancients laid those foundations.
Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.
> Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.
In a world with no AI, it is vital for humans to understand math, in order to derive practical applications. But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.
But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.
We have examples of AI producing theorems but there is no evidence that AI will be able to find all of the practical applications of mathematics, at least not any time soon.
As I understand it, most of the theorem proving work done by AI today consists entirely of “glue code” style work: combining a bunch of different known results to prove a new result. This is great for those who desire completeness in the mathematical project but it’s often outside the areas of interest for mathematicians who are pursuing “big idea” problems whose solutions likely require development of entire new branches of mathematics. One famous example of such was Fermat’s Last Theorem.
Then you have to make sure that the AIs understand the theorems (sort of build a "world" for that - otherwise how'd there be confidence in the use of said theorems?
If cryptography didn't exist but the maths did, how'd you use it?
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 person and finally an editor tells us that they decided almost immediately to reject our paper but they didn't tell us because "they hate giving bad news".
These were not top journals like Annals, but decent, prestigious ones, from whom you'd expect some professionalism.
This 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 constructive communications.
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”.
The proposal needs to be larger, to education itself in all subjects. We are manufacturing too many specialist parrots without critical analysis. We need to teach how to discuss controversy and manage disagreements, and then we can start making progress.
When 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, Measure, Hypothesize (includes modeling with mathematics), Test and Refine; pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality. The AI revolution is now showing them up.
> pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality.
You’re describing a very small fragment of total current mathematical labor. Very few people work solely on “formalization” and even e.g. model theory or type theory have real consequences.
I meant "Formalization" in the larger sense of the word.
The Definition/Theorem/Proof (DTP) emphasis (to the exclusion of everything else) for axiomatization in mathematics arose in the late-19th century and solidified in the 20th century. Prior to this, while mathematicians always practiced rigour, they valued insight/intuition more for understanding.
An attempt was made to teach "Modern Math" in a "New Math" manner which though withdrawn, has left its detrimental mark on mathematics education to this day. See the "Reception" and "Legacy" sections at https://en.wikipedia.org/wiki/New_Math
Excerpts:
Physicist Richard Feynman argued, "first there must be freedom of thought; second, we do not want to teach just words; and third, subjects should not be introduced without explaining the purpose or reason, or without giving any way in which the material could be really used to discover something interesting. I don't think it is worthwhile teaching such material."
In a 1971 article, mathematician René Thom rejected the New Math as "a test of memory that poisons intelligence" because of its complete neglect of intuition.
Mathematician and historian of mathematics Morris Kline observed that it was "practically impossible" to learn new mathematical creations without first understanding the old ones, and that "abstraction is not the first stage, but the last stage, in a mathematical development."
Mathematician and author George F. Simmons wrote in the algebra section of his textbook Precalculus Mathematics in a Nutshell (1981) that by focusing on form rather than substance, the New Math produced students who had "heard of the commutative law, but did not know the multiplication table."
Mathematician Laurent Schwartz described the new reforms as "very poor" pedagogy. For him, "The goal of mathematics is not to prove rigorously things that everyone knows. Instead, the goal is to find rich results and then, in order to make sure they are true, to prove them."
Yes. Though even philosophy, which doesn't have the "real world" iteration that science does, arguably doesn't have the problems of pure mathematics.
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.
This is also my stance. The fact that large numbers of people spend large amounts of publicly-funded time exploring what are essentially abstract puzzles is bizarre and not that different from, like, cloistered religious devotees who are supported in spending their time studying scripture and are considered to be the 'source' from which flows a certain kind of universal truth.
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.
A crucial caveat: basic research investment runs on the same logic as venture capital investment. We know that most mathematical efforts will be worthless. Our experience has lead us to expect that a very small number of such efforts -- some of them very far removed from applications -- will have payoffs so large that they change the shape of our society.
_We do not know in advance which efforts are going to pay off_. Abstract efforts in topology put us on the road to nuclear energy. Silly number puzzles enabled internet commerce. Non-euclidean geometry gave us synchronized universal GPS.
We should not let our inability to conceive of applications of weird abstract stuff prevent us from making these investments. If our ancestors had fallen in to that trap, we'd be far poorer as a society.
What we can do is ask that people trying new stuff attempt to fail quickly. And that's basically where we are with academia today. Most people who do mathematical work will not have a career in math. They try something new, work for a little while on it, and go do something else when the results turn out to be of modest interest. This leaves behind a messy undigested literature, which is unfortunate. But maybe AI can help us sift that for treasures we missed.
> to come up with a conceptual framework where it became easy to express
Feels a lot like building software from bottom - once you get the building blocks defined right, the action, or the program, are trivial to express. When doing it from the top-down, you write the program using the building blocks you haven't defined yet, and you might end up with overly specific building blocks, needing other blocks for expressing different behaviors.
When you do the bottom-up building blocks right, new behavior is easy to express with them. Essentially, you are building up the language to reach the problem. Or making a DSL, whatever definition you like best.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to reason about.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to maintain.
Someday, there might be mathematics designed for AI. Mathematics that only a tiny fraction of humans can understand, but a different kind of mathematics might emerge. I wonder if we would still call it mathematics.
What would happen if a non-human layer of mathematics emerged on top of human mathematics? In this article, the distinction between Mathlib and Mathslop might be a precursor to that.
If models advance enough in the future, and new definitions, compressions, and representational forms that are convenient for AI-to-AI communication emerge, what would happen then? Would mathematics split into Human-facing and Machine-facing branches?
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
Agree, but more specifically Math is clearly about a human understanding structure of things. Math is basically for humans. It's one of the main reasons understandable proof is so important.
That’s a strange delineation. Engineering is essentially about designing a thing, asking whether that thing really does satisfy the desired criteria, and then iterating when it does not. Mathematical models of the world are tremendously useful to this practice—engineers don’t need to guess about many aspect of the real world: they have physics. What they want, more than anything else, is strong evidence that a property holds. Internal validity (proof) and external validity (experiment) are the best evidence that you can get—why would you throw one of those approaches away?
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 don’t think of that as engineering. In the future, maybe it will be called an Oracle
I would call it "Engineered (as machine-made trustworthy) Mathematics": you have results but nobody undrstands them but they were not produced by humans.
Despite that, people use them. In that sense, similar to the Finite Elements method. But the tools (statements) are machined like any other tool (screwdriver).
Similar to microprocessors in your example. But about statements.
From reading this, it looks like the projected future is mathematicians working more applied to a domain, and the basic research in the academia being severely impacted by the AI companies - who have the money to hire the senior mathematicians from the academia. I guess if some of the biggest universities could come up with their own AI powered programs there could be something to “answer” in a more accessible knowledge, but I don’t see how to properly keep the students motivated to ensure the field keeps producing new people.
To be devil's advocate, two things may offer a glimmer of hope:
First, 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.
> Some prophesy that mathematics will eventually resemble Chess, a sport that a few eccentrics practice with passion and the general public can safely ignore.
How 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.
I 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 skills and imagination, the creation of whole new types of wood-working inventions and techniques, the perpetuation of millenia-old traditions, the teaching, the joy of selling to a happy customer, etc.
But now comes techo-capitalism, division of labor, you cut that piece a that piece over and over, you operate that machine, you won't even see the finished table, fuck your human element, we want that profit !
I don't think you have it right- the analogy to woodworking and craftsmanship is a category error and probably misses the broad thrust of the essay.
The goal of a woodworker or craftsman is the production of a finished good. He's arguing that, although it's been convenient to position a mathematician as a
"theorem-producer", that's never really been the aim of mathematics, and that the actual products of mathematics are some kind of "mental software"-
see his references to neuroplasticity. Basically, he's saying that the goal of mathematics is to create abstract structures that allow humans to reason about increasingly complex concepts, and that the "mathematician as theorem producer" is more like a convenient fiction that mathematicians have allowed to persist for too long, and now threatens to endanger the whole practice of mathematics.
You start with instincts that are more easily ascribed to ethically-neutral or ethically-positive reasoning, and then turn them into a spurious criticism of capitalism. Case in point: in the USSR, the means of producing chairs were 100% state-controlled and not motivated by profit, but the country operated soulless production lines too.
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.
Being invited to conference talks around the world is a completely normal part of being an active researcher in almost any academic field, so it doesn't register as pompous to other academics.
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.
> [...] 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.
Chaitin's work (including in his own opinion) moved the philosophical needle on maths towards "discovery" and away from "invention".
Indeed, his philosophy on the nature of mathematics is closer to "discovery", as in physics, than "invention" as in arbitrary game of rules and symbols (Hilbert) or language game (Wittgenstein).
I forget who said, "If you keep asking why, eventually you end up in the mathematics department." Calling it Platonism is a misunderstanding of how physics (and chemistry, biology, and the rest) emerge from mathematical structures and relationships that are more fundamental.
> 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.
In principle - if you're able to scale appropriately, using technology to augment capacity, then in principle, there's no abstraction for which we lack the capacity to comprehend, because calculation is calculation. Turing Computers can calculate anything which can be calculated given enough time and memory. Brains are Turing complete.
It's not just a tautology, it's a feature of the universe- if it can be computed, it's comprehensible. Even quantum physics is just computation - truth tables and counterintuitive operators interacting over time in ways that are strange to our embodied norms, but nonetheless following rules and limits strictly defined by mathematics.
But again, that's in principle. It might be completely impractical - taking a million years for an individual human - to hold a particular idea in their head, while an advanced AI can have such thoughts many times a day. Such things would remain mysteries, but in principle, an augmented human, or a series of interfaces with the relevant abstraction levels of such an idea, theory, or system, would in principle give us comprehension.
In practice, we'll never run out of mystery or ignorance or mistakes.
You've made a grave assumption in treating this as a binary problem: comprehensible or incomprehensible. The truth is that this lies along a spectrum. I can "comprehend" a color which my eyes can't see but this is different than trying to comprehend red. Or as a variant, I can comprehend a color that I can't see naturally but if I go into a lab and they simulate those cones in very specific ways I won't ever be able to really imagine it. Seeing it will be clearly a different level of comprehension.
I fully agree with this but also for some reasons unmentioned. Truth has infinite precision, a thing we will never achieve. Similarly my namesake showed there are limits to axiomatic systems. And there are problems that can't be solved by Turing complete machines. That only means they can solve computable problems but there's plenty that aren't. Very famously the halting problem isn't. And in the real world there's many problems which are intractable. And some are more intractable than othersIt could potentially be falsified by an encounter with really weird aliens.
But I find it quite plausible because it feels like it's fundamentally "just" a restatement or a minor variation of the Church-Turing thesis.
I see it as implausible, and I find myself thinking of Godel's incompleteness theorem(s).
Somewhere out there are "correct" thoughts we can't practically think without changing how our brains work.
>> 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.
[dead]
> 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.
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.
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.
>> 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
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
"unless you control the stack down to the hardware, it's basically a one way ticket to eternal slavery"
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.)
> unless you control the stack down to the hardware, it's basically a one way ticket to eternal slavery
Only if mind uploads are economically viable, which I doubt they ever will be. Organic brains are very efficient machines and it is far from clear that whole brain emulation could reproduce someone's intellect and consciousness within a smaller energy budget, or even accelerate it. The brain's behavior is so precisely adapted to its wetware that the emulation would have to reproduce many physical processes that are ultimately irrelevant to general cognition in order to not break the delicate equilibrium of the thing. The overhead would be gigantic.
Better just train from first principles, focusing on capabilities and skipping consciousness altogether. We can already see where this is going: LLMs in their current state would obsolete mmacevedo on many tasks. More likely than not, when it is possible to emulate brains, they will be terribly expensive, run like crap, and the only people interested in running them will be whoever had their own brains scanned.
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.
I know I failed to explain this correctly and was downvoted for it
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
That sounds a bit like the Gödelian argument against mechanism: reality (or even math) may contain systems that require stepping outside the current framework to formalize. A machine that can only work with current frameworks would be blind to these, except insofar that it can stumble across them by brute force.
Seems easily provable as 1 does not contain information about blue. It’s useful but not complete.
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"
People 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 confidence that our battle tested software is correct, mostly. And we tell people that we will never be 100% confident that any software is bug free. But that's a slight lie: if we wanted such confidence, we would start using provers, and create bug-free software. That possibility exists, but it's just extraordinarily expensive.
Well, in math that's the only possibility, and we use it. And it is indeed extraordinarily expensive, but it's also the cheapest among the alternatives. The alternatives are 2: be rigorous and do these proofs, or be sloppy and allow bugs to creep in, and allow an entire school of math to collapse like the Italian school of algebraic geometry [1].
There is one more alternative. If a particular math theorem has some applicability, then you write a program and use it in real life. In time you eliminate the bugs as much as you can, and you get to the steady state of "virtually bug free". At that point you don't have a solid proof that the theorem is correct, but in general you don't really care. Because you feel that a formal proof is just a thing one would pursue for getting academic satisfaction only.
[1] https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
Your example of the Italian school is well taken, although most of their results were later proven to be correct in the right setting. Severi's example is particularly egregious and I think a major reason this became a thing is Severi's refusal to course-correct and accept that some of the results were not correct. It has echoes of Mochizuki, and I fear, once you dig deeper, some issues around the initial declaration of "We've proven the Classification of Finite Simple Groups". There were many genuine gaps, and a lot of lore taken for granted. The sociology around how this happened is interesting - rushing to announce that it was done was the major mistake, it took away almost all incentive to actually write up the proofs and take them through proper peer-review. Genuine mathematical work was falsely reduced to "write up".
I thought this comment would go in a slightly different direction: the body of work that is mathematics has plenty of “bugs”; proofs with mistakes or other human errors. Yet we take the body to be correct (we believe it “works”) in aggregate, partly because the intuition of mathematicians tells us that these bugs are solvable and don’t bring down the whole. Of course the less intuitive/more surprising/more central the statement, the stricter the standard for proof and more eyes that have walked through it.
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.
It is because you can precisely define what would make the whole mathematical endeavor collapse (not following the rules of logic or showing inconsistency), while even defining precisely what would be undesirable for software requires bringing in the whole physical world. If you can't define the outcome you want, you can't have rigorous standards to follow.
If a piece of software is in safety-critical applications these days, it is often required to have a proof of correctness.
Like Linux? ;)
I think you might be surprised that Linux is generally not involved in safety-critical systems. There is a whole separate ecosystem for those applications.
What do they use for that? BSD?
The ones that use an OS generally use seL4 these days.
Thanks. "OS considered harmful" is a satisfying answer, too!
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 foundations (e.g. all popular asymmetric encryption schemes are built on top the assumption that certain problems such as integer factoring are hard, for which there is no formal proof), or at least explore both possibilities for statements with unknown truth value (e.g. you can find lots of work that explores the consequences of P = NP and/or P != NP).
However, there is a major separation between math and programs that I think mostly invalidates your proposal - most math we're talking about here is simply not applicable directly to the real world in any way. It's only studied for the interest of mathematicians. There is no real world consequence for Fermat's last theorem, for example - it was just a really interesting to prove theorem. In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.
> 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 was simply an infinitesimal delta x, not merely notation for derivation), which were not not formalized until much later, after they had already fallen out of favor and had been replaced in formal math by the delta-epsilon limits-based constructions.
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.
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 Archimedian property. It took until the 1960s before Newton's notion of fluxions became rigorously formalized with Non-standard analysis. https://en.wikipedia.org/wiki/Nonstandard_analysis
Oops, I confused some history, thank you for the corrections!
Physics famously has a rather cavalier attitude toward formal rigor, but that's because the ultimate test is comparison with experiment. String theory shows what happens when that bulwark against error is missing.
> 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
But this is due to a "failure" of programming language progress. We've had formal languages for a long time (see Ada and SPARK) and we've simply failed to use them for most scenarios, instead regressing to imperative manually memory managed languages like C and then deriving from that branch.
One thing I've realized after quite a long life of learning and contemplation is that: mathematics and software are essentially the same thing. Add to that that it might be the case that Physics is the same thing too. We'll see on that one, but there are signs...
Incredibly thoughtful. This essay gives that very rare sense of being well reasoned, gods at forest and trees, and sitting atop a shit ton of domain expertise.
Tangential but this article got me thinking.
Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves.
Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match or surpass the collective output of the entire human scientific community the equation will change.
It's a sad outlook.
The intelligence is only one part of the story. People need to actually go out there and do experiments. Science is not only theory, but also experimental. The best science happens when experiments show that a previously held assumption was not true. Eg the Michaelson Morley experiment where the assumption of ether was disproved. While AI is an incredibly powerful tool, it does not replace the act of observation. Thus Im sure we will still have scientists in the future and some degree of open science. There are experiments out there that by nature of their complexity need massive public coordination (CERN for instance) which in turn benefits from openness.
What is going to suck though is the ladder for juniors. We dont start out by working on big ticket problems, but usually early career researchers solve really tiny problems in a cheap way. The lowest bar for a cash strapped PhD student would be to contribute to some new theory in some way even if the student doesnt have access to equipment.
> People need to actually go out there and do experiments. Science is not only theory, but also experimental.
For biosciences and physics, sure. For mathematics? I am skeptical that your assertion applies.
Ah I see your point, I took the word science to mean bio, physics, chemistry, etc. IMO mathematics is a different discipline and not one Id consider a science, rather I see it as the language with which we express science.
If AI is somehow able to prove everything wouldn't it bypass Godel's incompleteness theorems?
It's not even just science. Anyone producing anything digital is now heavily incentivized to keep their wares away from the public internet, in a way we've not seen before. Drop any sample of your unique production online, and the AIs will obsolete you in days. That is a massive loss for people looking for inspiration and guidance.
> if a computer can match or surpass the collective output of the entire human scientific community the equation will change
Yes, but this is when someone reaches ASI and everything changes. For now, a good researcher can build off their discovery in a way their AI can’t.
> 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.
You know how I read new papers back in 1994? By going to the library, finding one in bi-annual publication list and requesting it through the University system. And it better be necessary because the uni had to pay both the catalogue and each reprint of an article. The access is most certainly easier today.
This was a lot because of the technological restrictions of that time.
Also be aware that the world wide web was actually conceived by Tim Berners-Lee for the exchange of information between scientists.
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?
I did try asking one of the PIs whether they were doing it to demonstrate that it doesn't work in order to get paper authors to provide their real data but didn't get a reply.
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.
s/regenerate/hallucinate/ but go on ...
Some previous submissions
HN history
Very good! Thank you!!
Meta:
- Sad to see how well thought out + well written stuff like this only makes it to the HN front page by a fluke. (Below: https://news.ycombinator.com/item?id=48758048#48759391)
- @davidbessis: maybe look for an open alternative to Substack? (avoid bullshit, proprietary, gated access for quality content by humans).
The core thesis seems to be that the "real value" is not in producing/proving theorems, but in understanding them. AI might be good at producing and proving theorems, but it fails utterly at getting humans to understand them. Even worse, humans have no interest in working on theorems that have already been proven, so we end up with theorems that will never be understood by humans.
I can understand why this is a major concern for mathematicians. They got into their field because they love the beauty of mathematics, and the intellectual satisfaction of understanding non-obvious insights. But to put it crudely, this sounds like a you problem. As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology. And their practical applications in human life. I have zero understanding of the math behind cryptography, but I still deeply appreciate the practical value they have provided humanity.
If AI systems start churning out accurate theorem-proofs, and we are able to use those theorems to build things that improve human quality of life, it doesn't bother me one bit that those theorems have not been understood by humans. If this offends your aesthetics, you are certainly entitled to your opinion and your preferences, but that does not make it a societal problem
They got into their field because they love the beauty of mathematics… As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology
I have some sad news for you. 99% of the work mathematicians do has no immediate application, nor even an obvious path toward application in the near future. You mentioned cryptography, so for an example consider number theory: no apparent practical applications, going back thousands of years to the time of Euclid and earlier.
It’s been religion, philosophy, and recreation that have provided the motivations to study mathematics all these years, not applications. Applications have almost always followed long after the development of the pure mathematical theory. For number theory, that was the development of cryptography during WW2, millennia after the ancients laid those foundations.
Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.
> Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.
In a world with no AI, it is vital for humans to understand math, in order to derive practical applications. But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.
But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.
We have examples of AI producing theorems but there is no evidence that AI will be able to find all of the practical applications of mathematics, at least not any time soon.
As I understand it, most of the theorem proving work done by AI today consists entirely of “glue code” style work: combining a bunch of different known results to prove a new result. This is great for those who desire completeness in the mathematical project but it’s often outside the areas of interest for mathematicians who are pursuing “big idea” problems whose solutions likely require development of entire new branches of mathematics. One famous example of such was Fermat’s Last Theorem.
It is like an idiot savant, just really widely read enough to seem creative when it tries some obscure thing. see First Proof though if you haven’t.
More divergent type than convergent like ramanujan.
Then you have to make sure that the AIs understand the theorems (sort of build a "world" for that - otherwise how'd there be confidence in the use of said theorems?
If cryptography didn't exist but the maths did, how'd you use it?
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 person and finally an editor tells us that they decided almost immediately to reject our paper but they didn't tell us because "they hate giving bad news".
These were not top journals like Annals, but decent, prestigious ones, from whom you'd expect some professionalism.
I've had a paper unrejected from Duke. The publication process sucks
How does unrejection work exactly?
You get a fields medalist to email the reviewer to say "wait that paper is really good actually"
This 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 constructive communications.
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”.
The proposal needs to be larger, to education itself in all subjects. We are manufacturing too many specialist parrots without critical analysis. We need to teach how to discuss controversy and manage disagreements, and then we can start making progress.
When 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, Measure, Hypothesize (includes modeling with mathematics), Test and Refine; pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality. The AI revolution is now showing them up.
> pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality.
You’re describing a very small fragment of total current mathematical labor. Very few people work solely on “formalization” and even e.g. model theory or type theory have real consequences.
I meant "Formalization" in the larger sense of the word.
The Definition/Theorem/Proof (DTP) emphasis (to the exclusion of everything else) for axiomatization in mathematics arose in the late-19th century and solidified in the 20th century. Prior to this, while mathematicians always practiced rigour, they valued insight/intuition more for understanding.
An attempt was made to teach "Modern Math" in a "New Math" manner which though withdrawn, has left its detrimental mark on mathematics education to this day. See the "Reception" and "Legacy" sections at https://en.wikipedia.org/wiki/New_Math
Excerpts:
Physicist Richard Feynman argued, "first there must be freedom of thought; second, we do not want to teach just words; and third, subjects should not be introduced without explaining the purpose or reason, or without giving any way in which the material could be really used to discover something interesting. I don't think it is worthwhile teaching such material."
In a 1971 article, mathematician René Thom rejected the New Math as "a test of memory that poisons intelligence" because of its complete neglect of intuition.
Mathematician and historian of mathematics Morris Kline observed that it was "practically impossible" to learn new mathematical creations without first understanding the old ones, and that "abstraction is not the first stage, but the last stage, in a mathematical development."
Mathematician and author George F. Simmons wrote in the algebra section of his textbook Precalculus Mathematics in a Nutshell (1981) that by focusing on form rather than substance, the New Math produced students who had "heard of the commutative law, but did not know the multiplication table."
Mathematician Laurent Schwartz described the new reforms as "very poor" pedagogy. For him, "The goal of mathematics is not to prove rigorously things that everyone knows. Instead, the goal is to find rich results and then, in order to make sure they are true, to prove them."
See also;
Against mathematical proof - https://mathwithbaddrawings.com/2021/05/12/against-mathemati...
Proof and Understanding in Mathematical Practice by Danielle Macbeth - https://journals.openedition.org/philosophiascientiae/712?la...
Yes. Though even philosophy, which doesn't have the "real world" iteration that science does, arguably doesn't have the problems of pure mathematics.
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.
https://news.ycombinator.com/item?id=48791433
This is also my stance. The fact that large numbers of people spend large amounts of publicly-funded time exploring what are essentially abstract puzzles is bizarre and not that different from, like, cloistered religious devotees who are supported in spending their time studying scripture and are considered to be the 'source' from which flows a certain kind of universal truth.
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.
A crucial caveat: basic research investment runs on the same logic as venture capital investment. We know that most mathematical efforts will be worthless. Our experience has lead us to expect that a very small number of such efforts -- some of them very far removed from applications -- will have payoffs so large that they change the shape of our society.
_We do not know in advance which efforts are going to pay off_. Abstract efforts in topology put us on the road to nuclear energy. Silly number puzzles enabled internet commerce. Non-euclidean geometry gave us synchronized universal GPS.
We should not let our inability to conceive of applications of weird abstract stuff prevent us from making these investments. If our ancestors had fallen in to that trap, we'd be far poorer as a society.
What we can do is ask that people trying new stuff attempt to fail quickly. And that's basically where we are with academia today. Most people who do mathematical work will not have a career in math. They try something new, work for a little while on it, and go do something else when the results turn out to be of modest interest. This leaves behind a messy undigested literature, which is unfortunate. But maybe AI can help us sift that for treasures we missed.
> to come up with a conceptual framework where it became easy to express
Feels a lot like building software from bottom - once you get the building blocks defined right, the action, or the program, are trivial to express. When doing it from the top-down, you write the program using the building blocks you haven't defined yet, and you might end up with overly specific building blocks, needing other blocks for expressing different behaviors.
When you do the bottom-up building blocks right, new behavior is easy to express with them. Essentially, you are building up the language to reach the problem. Or making a DSL, whatever definition you like best.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to reason about.
Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.
On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.
I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.
The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to maintain.
Someday, there might be mathematics designed for AI. Mathematics that only a tiny fraction of humans can understand, but a different kind of mathematics might emerge. I wonder if we would still call it mathematics.
What would happen if a non-human layer of mathematics emerged on top of human mathematics? In this article, the distinction between Mathlib and Mathslop might be a precursor to that.
If models advance enough in the future, and new definitions, compressions, and representational forms that are convenient for AI-to-AI communication emerge, what would happen then? Would mathematics split into Human-facing and Machine-facing branches?
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
Agree, but more specifically Math is clearly about a human understanding structure of things. Math is basically for humans. It's one of the main reasons understandable proof is so important.
Well, by "understanding" I mean "understanding by humans", indeed.
Engineering is used fairly loosely these days but I insist engineering ends where you have to prove theorems.
That’s a strange delineation. Engineering is essentially about designing a thing, asking whether that thing really does satisfy the desired criteria, and then iterating when it does not. Mathematical models of the world are tremendously useful to this practice—engineers don’t need to guess about many aspect of the real world: they have physics. What they want, more than anything else, is strong evidence that a property holds. Internal validity (proof) and external validity (experiment) are the best evidence that you can get—why would you throw one of those approaches away?
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 don’t think of that as engineering. In the future, maybe it will be called an Oracle
You might have gotten it backwards. Proofs are essentially rooted trees
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)
I would call it "Engineered (as machine-made trustworthy) Mathematics": you have results but nobody undrstands them but they were not produced by humans.
Despite that, people use them. In that sense, similar to the Finite Elements method. But the tools (statements) are machined like any other tool (screwdriver).
Similar to microprocessors in your example. But about statements.
I built a toy autonomous math research project: https://paulklemstine.github.io/Lean/
From reading this, it looks like the projected future is mathematicians working more applied to a domain, and the basic research in the academia being severely impacted by the AI companies - who have the money to hire the senior mathematicians from the academia. I guess if some of the biggest universities could come up with their own AI powered programs there could be something to “answer” in a more accessible knowledge, but I don’t see how to properly keep the students motivated to ensure the field keeps producing new people.
To be devil's advocate, two things may offer a glimmer of hope:
First, 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.
Plenty of math showed zero real-world value for centuries until it suddenly did.
This might be the most interesting essay on the nature of mathematics I have ever read.
It was also about 10x longer than it had to be because an LLM was heavily involved in its writing.
> Some prophesy that mathematics will eventually resemble Chess, a sport that a few eccentrics practice with passion and the general public can safely ignore.
How 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.
I 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 skills and imagination, the creation of whole new types of wood-working inventions and techniques, the perpetuation of millenia-old traditions, the teaching, the joy of selling to a happy customer, etc.
But now comes techo-capitalism, division of labor, you cut that piece a that piece over and over, you operate that machine, you won't even see the finished table, fuck your human element, we want that profit !
I don't think you have it right- the analogy to woodworking and craftsmanship is a category error and probably misses the broad thrust of the essay.
The goal of a woodworker or craftsman is the production of a finished good. He's arguing that, although it's been convenient to position a mathematician as a "theorem-producer", that's never really been the aim of mathematics, and that the actual products of mathematics are some kind of "mental software"- see his references to neuroplasticity. Basically, he's saying that the goal of mathematics is to create abstract structures that allow humans to reason about increasingly complex concepts, and that the "mathematician as theorem producer" is more like a convenient fiction that mathematicians have allowed to persist for too long, and now threatens to endanger the whole practice of mathematics.
> I thought it was very interesting, but maybe also incredibly naive politically ? it's like he's re-discovering alienation under capitalism.
To be fair, a number of professional politicians and political scientists don’t understand alienation under capitalism.
You start with instincts that are more easily ascribed to ethically-neutral or ethically-positive reasoning, and then turn them into a spurious criticism of capitalism. Case in point: in the USSR, the means of producing chairs were 100% state-controlled and not motivated by profit, but the country operated soulless production lines too.
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.
Is being pompous and on the nose part of being in mathematics?
"I was in Switzerland", "I was invited to a talk", "I started a machine learning company", look at me bro.
Being invited to conference talks around the world is a completely normal part of being an active researcher in almost any academic field, so it doesn't register as pompous to other academics.
Yes, which makes starting with those somewhat strange as they're largely unrelated.
I see the AI panic has reached mathematics…
I've only started reading it but it looks very good. I'll finish it tomorrow or so.