# Software Recommendation for Theorem Suggestions

So I am not sure if this software already exists or perhaps this is something that humanity has to embark on to finally have as a product. A bit about myself, I am student training in a sub-area of Mathematical Logic.

My question is as follows, I wished to know if there is a software which can give us past theorems as suggestions once I write out my hunch for the problem statement I formalised after doing my literature survey? I feel this would be just like the similar questions suggestions menu stackexchange has in it's interface.

If the answer to the above is a `no' or it's a software in progress, then, I would wish to know the thoughts of the community on how such a software could be formed.

Two challenges for such a tool that at least I can spot immediately are:

1. First the Database of theorems on which this software will do a query or similarity analysis, perhaps that in itself is a task that at least manually would be really challenging. Perhaps a faster way to achieve this would be to train some machine learning algorithm to convert the Theorem or Proposition speak into a more rigorous formal language version amenable for the Search Query version. And, then crawl on the mathematical literature accessible.

2. The definition of the notion of similarity between two theorems. As a logician, my take here would be, what we wish to always search for are theorem "forms", keeping the domains of the objects/variables separate. The domains of the object would have certain properties that will make each proofs slightly different, which is what the user querying such a question will have to figure out.

An illustration of what I mean above is : "$$\exists x : x^2 = -1$$", this is a theorem "form" in my eyes, this particular statement would have different proofs about it's validity in different domains ($$\mathbb{Q},\mathbb{R}$$) of interpretation.

If there are further aspects that make this task an impossible or an incredibly difficult one do let me know.

• A keyword that might point you to existing research in this direction is "mathematical knowledge management". Commented Mar 21, 2023 at 5:09
• Ah, I see, I shall look into it and get back to you or this question with a self answer. Commented Mar 21, 2023 at 8:37