Hi Jon, Interesting email! I have many comments to make, so, inline, below.
On Wed, Jan 6, 2021 at 5:47 AM Jon P <[email protected]> wrote: > Hello everyone, my name is Jon, I have a PhD in mathematics (partial > differential equations) and some experience as a programmer for a self > driving car firm. OpenCog seems awesome, my health is not so good A key priority in life is to take care of your health. Conventional wisdom about regaining health is mostly accurate, assuming you've figured out what "conventional wisdom" is. > > I have been part of the metamath <http://us.metamath.org/>community for a > while and wanted to ask, are there any links between the OpenCog community > and the metamath community? > I've never stumbled over it before. > Do you already know a lot about formal mathematics and are including it in > your system or are you taking a different approach? > I would like to believe that I know bucketloads of formal mathematics. And bucketloads of mathematics, in general. After a (literally) 15-second survey of metamath, I would say that the big difference is that "formal methods" appears to limit itself to crisp true/false values. By contrast, I'm more interested in probabilistic truth values, and generalizations thereof (time-varying, bounded, with hysteresis, etc. etc.) I also like to think of propositional calculus or sequent calculus or Hilber calculus as being a graphical network: Each sequent has some inputs, some outputs, and the rules of the game are to connect them up, until you've discovered a "proof". Well, that proof is "just a graphical network of connections between axioms attaining exact true/false values on each leg of each connection". So I've attempted to build the AtomSpace as a place to store and connect-up axioms/sequents/assertions/rules with connections that are probabilities/weights/fuzzy-logic values/etc. -- that is, numbers, or number-like things: qubits/homogenous spaces/etc. If you study neural networks, you can see that they are densely connected networks, with nodes, and almost all weights between almost all nodes being non-zero. If you study formal mathematical proofs, you can see that they are extremely sparse networks, where every node is connected to only 1 to 3 or 4 others, where the weights are exactly true/false/0/1. If you study natural language, and biochemistry and many other natural phenomena, you find a scale-free network that is neither dense, nor is it sparse, but somewhere in the middle. I am deeply interested in converting time-ordered expressions of that network into the underlying structure. (and back). So, by analogy: a seismologist, all they have are some time-series recordings of Earth's vibrations; from that they try to reconstruct the structure of Earth. I have a time series of words, I want to reconstruct the structure of the brain that wrote those words. And, once reconstructed, what else might that "brain" have said? Just like the Earth model: what other kinds of earthquakes might it produce? I've got half-a-dozen PDFS all 20 to 100 pages long, that spin out each of the above paragraphs into great detail. I think they're important, but I can't get anyone to read them :-) So it goes... > For anyone who has never heard of it here are a few reasons I am excited > about the approach metamath is taking. > > Firstly the metamath database is growing. It has it's own syntax to encode > mathematical statements and the main database > <http://us.metamath.org/mpeuni/mmtheorems.html> contains about 30k proven > theorems based on ZFC set theory and is about at an advanced undergraduate > level at the moment. It is in somewhat of a graph bases structure, where > each proof is a list of steps, each of which were themselves proven > previously. This may mean it has some compatibility with the atom based > hypergraph approach, though I can't claim to really understand that. > So what I wrote above "explains" the atom-based hypergraph. It is good at what it does, but, for special cases, such as crisp logic, it is not efficient representationally or computationally (RAM and CPU use). (Hey, its *also* inefficient for neural network-type computations!) The good news is that it does have a natural layering or "abstraction" mechanism that does allow it to "wrap" hyper-efficient proof engines (or neural net engines). I've wrapped a few things here and there. I have not daydreamed about wrapping formal systems, but have not found any compelling reason to do so. I strongly encourage others to do so. (Well, I strongly encourage planning and strategizing, first. Good plans results in fewer disappointments.) > > Secondly a core idea of mm development is that the software which operates > on the database is totally separate from the database itself (in contrast > to Lean and other formal systems). So there are a bunch of verifies, which > can check the validity of the encoded proofs, and people are writing new > ones all the time. This makes it easy to hook into the database which is > just stored as an ascii text file. There is some comparison of formal > systems here > <https://jiggerwit.wordpress.com/2018/04/14/the-architecture-of-proof-assistants/>, > which maybe is not so kind to metamath ha ha. > These are software engineering questions. Of course, it is always better to be modular, unless your modular design runs 10x slower or is 10x more bloated than the integrated design. But this is an orthogonal discussion, and is, in some ways, less interesting than the "meta" discussion of "what are you actually trying to accomplish?" > > Thirdly there has been some nice progress recently in AI proof generation. > OpenAI has been running a project <https://arxiv.org/abs/2009.03393> and > have created a pretty good narrow AI which is better than me at proving > theorems, which is maybe not such a big compliment ha ha. This has a nice > virtuous circle to it where a larger database makes it easier to prove new > theorems which makes the AI more powerful. > > There is a tipping point coming I think where the boundary of the mm > database (or another formal system) catches up with where cutting edge > mathematical research is. I think at that point many professional > mathematicians will switch to working formally (it has a huge number of > nice advantages, it's basically digitising the field and apply AI to it all > at once) and that will be a "big bang" of sorts. > > Fourthly Mario Carneiro has been doing some really cool work on formally > verifying computer programs. So he has a formal system which sits on top of > the x86 architecture and can prove, if the hardware executes the algorithms > correctly, that certain functions will have certain properties. He was kind > enough to explain a bit of it to me here > <https://groups.google.com/g/metamath/c/MbFrc9WEIGY/m/JGnhRp6DAgAJ> after > a nice talk he did. > > Fifthly I am then quite excited in the abstract about where this system is > headed. For example an AI which can formally reason about code it is > writing and can prove mathematical statements could be very powerful. I > think there is some nice approach to the control problem here, something > like "new code can only be run if it is proven to obey the same constraints > that currently running code is bound by." This maybe creates a way of > limiting what an AI can do no matter how clever it becomes. > I was thinking of replying to these in detail, but I think I already explained that "there's more to life than crisp true-false values" and that data is more general than simply networks of propositions and assertions, axioms and deduction rules. Some of my thinking on these matters is informed by ergodic theory, the theory of phase transitions in physics ... stuff like spin glasses (I can make a rough argument/analogy that says human society is like a spin glass. This is not meant to be a casual observation, but rather a statement about how neurons interact with one-another, forming thightly-bound, high-bandwidth, low-latency "human brains", and how "human brains" then interact with each other using low-bandwith, high-latency writing, speech, radio, television, and most importantly, social media. And that the network connectivity of human brains via social media is a change-of-phase as compared to mass media, which explains the current political turmoil. We have entered a fundamentally different era of inter-human-brain connectivity. So I am interested in modelling networks, in general: scale-free or hubby, centralized or decentralized, federated or not, exchanging messages that are more than binary true-false values. And then, like the neuroscientist sticking wires into the brain, I want to take time-series samples of that network, and reconstruct what that network "is thinking", what that network "knows". The networks formed by axioms and rules of deduction are just one very special case. A very important special case, but very remote from the other special case that storms capital buildings and makes facebook posts about it. They're both networks. I'm interested in the networks. (Sigh, to dot my i's and cross my t's -- molecular interaction between DNA, Proteins is also a network. An absolutely brilliant example of this can be found at https://algorithmicbotany.org where Professor Przemyslaw Prusinkiewicz has taken a 3-4 decade journey, starting out with state machines (crisp logic, grammatical rules) and stapling on the diffusion-reaction equation. You're a PDE guy. You know the diffusion-reaction equation. Now, imagine coupling one of the fields to a (deterministic) finite-state machine. What happens? The answer is "biology", or, at least, "botany". The "deterministic machine" is, roughly speaking "DNA", and the things that diffuse are the various proteins that are expressed. That's very very rough, but gives the idea. So: can I take a deterministic theorem prover, which discovers "facts", and attach them to a differential equation that models the diffusion of knowledge in human society? What happens when I do this? As that knowledge diffuses from machines to human brains, and back to machines, how does this change the priorities of what the theorem prover is working on? How does the man-machine symbiosis work? > > This is a much more speculative idea but I think it is interesting to > imagine a statistical layer feeding in to a formal layer. So for example > say a linear regression is applied to some collected data and finds some > formula for a relationship it would then be possible to use the metamath > framework to reason about this formula, maybe integrate it for example, and > from that generate a hypothesis which could then be tested in the world. > > Anyway that's probably enough from me I think. If anyone has questions or > would like to talk about any of this stuff I would enjoy that. Otherwise I > hope everyone has a great day! > I eagerly anticipate further discussion! -- Linas -- Patrick: Are they laughing at us? Sponge Bob: No, Patrick, they are laughing next to us. -- You received this message because you are subscribed to the Google Groups "opencog" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAHrUA348fxiCuOo4SFRYCEDkhjCKap2h%3D_Nn4m6CyJE0RPP7tA%40mail.gmail.com.
