On Implication Flow
I was thinking why the function of time (t⊆ T) | space (s ⊆ S), observer (o ⊆ O) is so persistent from observers’ point of view, and realized that we deal with relatively few categories of objects given the size of the parameter space, i.e. we experience the spatial (and temporal) topology of nature (observer scale is not necessarily always the same as the observed object scale), but don’t really change it that much (maybe except for physics wonders like the LHC).
In terms of architecting the space — many configurations of atoms are possible in a single glass. Few of them can be observed by the objects we know, i.e. legitimacy of objects is a function of scale.
Every object (body) b ⊆ B can be approximated by how it’s seen and interacted with by its neighbor observers. Given that the interactions we know are consequential (in timespace), bodies can be described as a sum of what implies them (those are (approximately) temporal implications).
The asymmetry between what’s implied and what’s not implied reminds me of how single-cell organisms are trying to explore every direction — a bit of everything, and then a highly organized action (that involves more energy given the energy used for the exploration). The ratio of exploration vs action (I think it sounds better than exploitation) is likely a function of scale, too.
Now, an observer o can be seen in terms of its compute c: o ∝ c. Compute can be seen in terms of algorithmic capability, I’ll call it implication flow (it’s an analogy to Ricci flow and Ricci tensor as well as the Equational Theories (maintained by Terence Tao, Pietro Monticone, and Shreyas Srinivas) project).
That implication flow should give us some sort of general algorithm approximation that doesn’t take forever to train, and for which inference runs in real-time on our servers (perhaps mirroring (or hologram) would be a better term (than approximation) here, because approximation implies looking for a perfect copy, whereas a reflection (in a mirror) would have its own implication signature, incl. their own number).
Assuming that the goal is to streamline mathematics and mathematical engineering, our digital nets would need longer, more insightful sentences from the language that nature speaks. They are quite rare — we’d need to generate them.
That would lead to a flywheel (generate, train, use).
I guess bootstrapping the flywheel will start with science. I’ll discuss math here. Solving math will take physics to the next level, too.
(You can skip this paragraph. I was thinking of a metallic wheel covered with a magnetic layer (even built a fun wheel with my son), and I would love to be able to simulate things like this. I’d love to ask an LLM to simulate how a flying object could move assuming it could move really fast.)
Bootstrapping the flywheel by equipping transformers with
access to the implications from the Equational Theory project (and similar) as well as tools (like Vampire, Prover9, Mimizinc, and so on; I already have a couple of LLM-based ideas for other tools),
and getting them to create new and high-quality (Lean-)verifiable knowledge themselves
would be a big step forward (point 2 is critical — the critical mass of data must be achieved for the newly trained net to create new knowledge; creating new knowledge is key here).
I was talking transformers here (or next-gen architectures profiting from what we’ve learnt from transformers). But let me mention one more idea.
A global verifiable e-graph (as well as private e-graphs) could not only be a seen as a means to train transformers, but potentially also as a standalone mathematical knowledge creation tool (for quite a bit). It’d be interfaced using tools and languages, and transformed by new proofs. It could become a new way of world exploration.
Engineers could bootstrap their codebases with more than just regular code — it’d be verifiable code (every reference to a mathematical function would be stronger than ever; new functions could be made possible — or even requested (agentic math would mean that agents could work in the background)). A new version of gradient descent could propagate verified implication chains.
In that verified implication chain environment, diffusionese (and similar) could be used to dream up new tactics. In the agentic math setting, agents would use those new (verified) tactics to create new implications.
Implications would flow in that future implication flow world.