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