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 so it's often hard to find nice ways to contribute but maybe there is something and I hope some encouragement is worth something :)
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? Do you already know a lot about formal mathematics and are including it in your system or are you taking a different approach? 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. 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. 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. 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! Jon -- 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/371730ce-2f1f-4ab6-9559-26cef4d847e8n%40googlegroups.com.
