Hi, there hasn't been actual work connecting OpenCog w/ ATPs, however I've been engaged with that community a bit since my son Zar Goertzel is currently doing a PhD on AI for theorem proving w/ Josef Urban... I have given talks on OpenCog PLN for commonsense reasoning and scientific reasoning at the last couple AITP events and Josef gave a talk at the AGI conference a few years ago when it was in Prague...
My commentary on GPTf is here http://multiverseaccordingtoben.blogspot.com/2020/09/gpt-f-one-more-funky-experiment-in.html -- Josef did a more in-depth analysis as he has been engaged w/ similar work prior to (and since) GPTf ... Metamath looks like an interesting knowledge base, I have looked at it a while ago but not recently... One issue with OpenCog-based logic reasoning now (e.g. PLN) is that it's very slow compared at crisp inference compared to modern ATPs ... this will be remedied somewhat with the new Hyperon version https://wiki.opencog.org/w/Hyperon but still there is a certain slowdown that comes w/ having such a general representation... A strategy that interests me is using heuristic/probabilistic/AGI-ish reasoning in OpenCog to learn "proof sketches" (by which I mean, more like what a regular mathematician rather than a logician or ATP guy would call a proof) and then invoke some traditional ATP system like vampire or E prover to fill in the blanks and make a fully formal proof ... (see some semi-related thoughts on formal proof sketches here, https://www.cs.ru.nl/~freek/pubs/sketches2.pdf , there is also more literature...) So in short -- definitely of acute interest to some of us (I'm a math PhD from way back when also) but not a subject of current actual work focus... ben On Wed, Jan 6, 2021 at 3:48 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 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 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 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, 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 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 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. -- Ben Goertzel, PhD http://goertzel.org “Words exist because of meaning; once you've got the meaning you can forget the words. How can we build an AGI who will forget words so I can have a word with him?” -- Zhuangzhi++ -- 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/CACYTDBcg%3D8W3%2BXnkemSUHm2_fnJquX%2BRKV0d6Z%3DzH3KXX9orwQ%40mail.gmail.com.
