Système existant ?

Bonjour à tous,
je voulais savoir s'il existait déjà, sous forme complète ou sous forme de projet, un système qui rassemblerait tout ou (grande) partie des résultats mathématiques connus (ça fait beaucoup je sais), dans un cadre entièrement formalisé et universalisé (définitions, notations, etc), qui permettrait d'avoir une sorte d'assistant de recherche automatisé.
Je ne parle pas d'un truc qui ferait des démonstrations tout seul, mais plutôt quelque chose du genre :
j'ai un objet $X$, ayant trois propriétés $P_1,P_2,P_3$. Ma question : est-ce que mon objet a aussi la propriété $P$ ?
Je rentre dans le système mon objet, qui est déjà référencé, ainsi que ses trois propriétés, et je pose ma question :
réponses possibles :
-"oui, c'est un résultat de machin, voici une référence"
-"oui, après un nombre fini d'implications je tombe sur cette propriété"
-"non, voici un contre-exemple"
-"je ne sais pas", et c'est là que le travail humain prend le relais.
Tout ça dans une optique de gain de temps pour la recherche.
Tout le monde pourrait y contribuer, ajouter un résultat qui n'y est pas encore, avec une équipe de vérification, etc.

Est-ce que ça existe, est-ce que c'est utopique ? (merci d'éviter les remarques du genre "c'est pas comme ça qu'on fait de la recherche !!!")