<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>