The fall of the theorem economy

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

Chess does not require a visual cortex to play. People have been playing by mail with algebraic notation for centuries.

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)

(I bet there are people at all the big AI labs working on ways to incorporate something more CNN-like into LLMs somehow.)

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.

> 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

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 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?

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.

For biosciences and physics, sure. For mathematics? I am skeptical that your assertion applies.

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.

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.

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 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