<div dir="auto"><div>I think you're right, this could be a very powerful tool. In the same way AlphaZero used intuition to narrow its game search tree, automated theorem provers could use a mathematical intuition to find interesting and useful proofs and avoid slogging through the full exponentially growing search tree.</div><div dir="auto"><br></div><div dir="auto">There's already a strong mathematician within GPT-4, see for example, page 40:</div><div dir="auto"><br></div><div dir="auto"><a href="https://arxiv.org/pdf/2303.12712.pdf">https://arxiv.org/pdf/2303.12712.pdf</a><br></div><div dir="auto"><br></div><div dir="auto">Jason </div><div dir="auto"><br></div><div dir="auto"><br><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Sun, Mar 26, 2023, 8:35 PM Rafal Smigrodzki via extropy-chat <<a href="mailto:extropy-chat@lists.extropy.org">extropy-chat@lists.extropy.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">It occurred to me that LLMs mated to a mathematical inference engine (like the Wolfram Alpha plug-in for GPT) and enhanced with visual data processing capabilities might make excellent automatic mathematicians.<div><br></div><div>Mathematical inference in the sense of symbol manipulation and theorem proving can be automated relatively easily but up till now such systems lacked the intuition and imagination as well as the sense of beauty that mathematicians use to select among the infinite numbers of mathematical objects and properties the ones that are worth thinking about. A theorem prover without this intuition would just aimlessly churn out proofs and never create anything useful. But add an intuition trained on the patterns imprinted in the mathematical literature by the minds of the mathematicians who create math, and the Automathician could write math like a human. Since its breadth of mathematical knowledge and raw symbol manipulation ability would be vastly superior to any human, its high-level mathematical insights could become superhumanly mathemagical.</div><div><br></div><div>A modest LLM training project using a corpus of mathematical papers with RLHF provided by mathematicians could be a very interesting endeavor. Who knows what kind of very non-obvious and ground-breaking truths could be discovered? The algorithms based on such non-human insights could be of immense practical value, too.</div><div><br></div><div>Rafal</div></div>
_______________________________________________<br>
extropy-chat mailing list<br>
<a href="mailto:extropy-chat@lists.extropy.org" target="_blank" rel="noreferrer">extropy-chat@lists.extropy.org</a><br>
<a href="http://lists.extropy.org/mailman/listinfo.cgi/extropy-chat" rel="noreferrer noreferrer" target="_blank">http://lists.extropy.org/mailman/listinfo.cgi/extropy-chat</a><br>
</blockquote></div></div></div>