Chère de Prince

Présentation personnelle

Youp, je m'appelle la Bécasse et je suis un oiseau, qui fait des mathématiques. Il m'arrive aussi de coder un peu pour le web, et de dessiner des graphes sur la toile ici et là . Mais aujourd'hui, c'est mon graphe fétiche, que je te présente : Chère de Prince, un graphe de math.

Présentation du projet

Naissance d'un graphe

J'avais remarqué, que certains objets mathématiques se construisent toujours de la même manière. Par exemple, on définit ce qu'est un triangle, puis un triangle rectangle, isocèle, rectangle-isocèle. On peut faire un graphe à partir de ce constat, alors il fallait que je le fasse.

Pourquoi un graphe ?

Parce que j'aime les graphes ! Plus sérieusement, parce que c'est visuel, et que l'on peut joindre à chaque lien du sens et ça donne de la sémantique, de la logique. J'en parle plus loin.

Objectif du graphe

Chère de Prince a pour but de répertorier des énoncés mathématiques concis et les liens, qui existent entre eux. L'objectif est de créer une base de données sémantiques d'énoncés mathématiques, auquel chacun puisse participer. Il serait alors facile de trouver un exemple d'un objet, d'utilisation d'un théorème. Mais aussi, de donner un sens et une source, aux publications mathématiques faite sur le web en les rattachant à des énoncés du graphe. Évidemment, il faudrait une quantité d'énoncés significative, donc une communauté dynamique, aussi .

La différence avec Wikipedia réside dans la structure des données et la concision des énoncés, qui permettent de faire des liens précis.

État du graphe

Aujourd'hui les énoncés et les liens forment un graphe, qui contient 418 définitions et 180 propositions. Un lien est placé entre deux énoncés, à condition que le premier mentionne le second dans son contenu ou dans une de ses preuves. C'est ainsi que le théorème de Pythagore est lié à la définition de triangle rectangle.

On peut alors se promener d'énoncés en énoncé :

• soit en localisant un énoncé sur le graphe ;
• soit en regardant la liste des énoncés relié à un autre.

Un petit moteur de recherche fait maison permet d'aller rapidement voir un énoncé.

La méthode d'édition actuelle est assez primitive, et ne permet pas de récupérer les modifications passées. C'est pourquoi, seuls quelques personnes peuvent modifier le contenu, désolé. Ça va changer !

Quelques améliorations

Un graphe plus sémantique

J'ai parlé de liens sémantiques et finalement il n'y a qu'un seul type de liens dans le graphe. On est d'accord, c'est un peu pauvre . Pour améliorer ça, on peut par exemple créer deux nouveaux types de liens, est toujours et possède toujours, qui relient deux définitions. Dans la pratique, on pourrait les rencontrer ainsi :

• un triangle rectangle est toujours un triangle ;
• un triangle possède toujours une aire.

Et là, on a des liens intéressants, car ho magie, on en déduit que : un triangle rectangle possède toujours une aire. La création du graphe devient alors plus simple et rapide.

Bref, je ne rentre pas dans les détails, mais il y a plein d'autres liens, qui sont décrits dans un standard de web sémantique appelé OMDoc. Je dois encore potasser tout ça .

Parlons math dans le graphe

Un autre point important, qui n'a pas encore été abordé, c'est le dialogue. Il faut que les rédacteurs puissent discuter à propos de chaque énoncé. Donc il faudrait un canal de discussion, qui puissent être ouvert pour chaque énoncé.

Un autre flux de discussion sous la forme d'un forum permettrait de poser des questions générales de mathématiques en faisant référence à des énoncés du graphe. On pourrait demander des exemples d'objets mathématiques, ou d'applications de proposition.

Les mots de la fin

Pour les détails techniques, le site utilise un serveur node.js et l'application sails.js. Le graphe est affiché grâce à la formidable application javascript sigmajs. La rédaction se fait en markdown avec des intégrations de LaTeX compilé grâce à MathJax. Il y a aussi du code de Twitter pour les mentions.

Le projet est très ambitieux, j'en conviens, mais il me tient beaucoup à cœur. Tous les avis m'intéressent. Si tu veux participer à la rédaction, on peut en parler. Si tu connais un moyen technique pour améliorer quoique ce soit, je prends ! Parle-moi, je suis un être sociable .

• le site : Chère de Prince
• Twitter : @CheredePrince
• Facebook : La Bécasse
• Github : le dépot

Côté serveur, comment le graphe est modélisé ? Avec un base de données orientée graphe ?

Toi tu as choisi le bon jour pour présenter un projet nommé "Prince"…

Le graphe est modélisé dans un base MongoDB, avec des liens entre les collections représentant les énoncés. Je pense qu'une base de données orienté graphe serait un très bon choix pour mettre en place simplement des liens sémantiques. J'ai été voir rapidement Neo4j

Je ne complote rien du tout

Côté serveur, comment le graphe est modélisé ? Avec un base de données orientée graphe ?

Le graphe est modélisé dans un base MongoDB, avec des liens entre les collections représentant les énoncés. Je pense qu'une base de données orienté graphe serait un très bon choix pour mettre en place simplement des liens sémantiques. J'ai été voir rapidement Neo4j

Est-ce que tu as rencontré des soucis avec les liens entre collections, au niveau des perfs ? Je pose la question parce-que j'ai déjà eu l'occasion de travailler avec MongoDB (une seule fois), c'était pour modéliser des documents contenant éventuellement d'autres documents imbriqués, donc ça restait dans ce que MongoDB promet de bien savoir faire. Mais je n'ai pas eu l'impression que la modélisation de ce genre de relations était une excellente idée, avec MongoDB. D'où ma question.

Eh bien, je dois avouer être assez déçu par la lenteur, que je constate lors de la création et l'édition. J'avais commencé par suspecter mon code de ne pas être assez optimisé, puis il y a quelques jours, j'ai écouté le temps pris par MongoDB uniquement, c'était clairement le responsable . Si tu as une idée pour changer de base de données ou améliorer les perfs, je suis toute ouïe.

Je ne voudrais pas m'avancer et te dire n'importe quoi, je suis loin d'être un expert en ce qui concerne les bases de données. Mais si tu a le temps et l'énergie, tu peux créer une branche expérimentale et tester ce que ça donne avec Neo4j ou un autre système qui semble être adapté.

Petite question, le code sur le GitHub, il s'agit bien de l'intégralité de ton site, et non pas que de la partie qui gère le graphe ?

Ouais, tout le site est sur la même branche Github. Tu as complètement raison, je devrais m'assurer que neo4j marche bien. Créer une branche expérimentale pour séparer la base de données mathématiques du reste du site, que tout le monde puisse utiliser pour ses besoins. Ça me donnerait des bases saines

J'aime bien l'idée. À suivre de près.

Mathématiquement parlant, c'est toujours assez difficile de bien cerner quelles sont les notions en jeu dans tel ou tel énoncé. Un petit guide ne serait pas de trop.

Philosophiquement parlant, ce qui m'intéresserait plus, ce serait une classification des preuves selon les idées et non pas les objets (qui ont finalement qu'un intérêt limité).

Oui, tu as raison Holosmos. J'ai commencé par créer des liens de type mention, parce qu'elle est très simple. Il y a bien sûr un peu d’ambiguïté sur quand est-ce qu'il faut mettre un lien mention entre deux énoncés. Je vais essayer de clarifier ça, en ajoutant des sous-classes de liens mention, comme l'est le lien possède toujours. Bref, j'espère un peu trouver des textes, qui éclaircissent la voie vers une logique assouplie.

Du coup, j'espère bien, que des liens définissant des conséquences logiques soient décrits dans le standard OMDoc, sans être trop formel. En effet, il faut trouver un compromis entre être formel et être simple à rédiger.

Salut !

Ton projet me fait penser à un petit projet auquel j'avais contribué il y a quelques temps et qui consistait en un outil de prise de notes qui permettait d'organiser les notes sous forme de graphe. Et le rendu visuel était vraiment sympa je trouvais (voir ici ).

Du coup je me demandais si tu comptait modifier le design pour rendre la présentation des noeuds et de l'ensemble plus "visuelle" et plus 'user friendly" ce pourrait en faire un outil super sympa à utiliser ! Car là c'est un peu austère on va dire.

Salut Demandred,

Tu trouves que le design est trop simple ? Tu verrais plus d'information présente sur le graphe ? Tu trouves que ça manque d'aide pour la navigation ? Tu penses que mettre des images sur les nœuds rendrait le graphe plus lisible ? Je sais, ça fait beaucoup de questions

Je serais curieux de voir, le graphe de ton projet, de savoir avec quelle librairie, il est rendu.

Merci pour ton message et pour le lien, je vois mieux où tu veux en venir.

Je ne comprends toujours pas pourquoi tu me parles d'austérité. Un fond noir et des nœuds verts, ça fait peut être un peu Matrix, un peu inquiétant. Par contre, je ne me suis pas serrer la ceinture en le faisant, c'était pas l'austérité.

Pour le manque d'information au sujet du graphe, je suis mille fois d'accord. Si tu ne comprends pas comment s'utilise l'interface, c'est de ma faute. Ça manque d'une légende! Alors peut-être juste un peu de patience, j'y travaille. Les couleurs des nœuds correspondent au type de celui-ci (vert: définition, bleu: propriété, rouge: théorème … ), et le cercle blanc autour de certains nœuds signifient qu'ils sont sélectionnés ( leur contenu s'affiche dans le panneau latéral).

On pourrait aussi essayer d'affilier des énoncés à une catégorie, pour faire apparaître des territoires mathématiques (excitant, non ?). La classification fournie par l'AMS (société américaine des mathématiques) me semblait pertinente, parce que déjà utilisée. Par contre, je vois difficilement comment l'utiliser dans l'affichage du graphe. On pourrait ajouter une ombre colorée à chaque nœud, pour faire apparaître les tendances thématiques d'une région. J'ai peur que ça deviennent lourd. Si quelqu'un a d'autres idées, qu'il se manifeste !

Oui, il y a du bruit, lorsqu'on regarde des nœuds sélectionnés . Mais j'ai une proposition, pour le réduire. Si on met en place quelque chose, qui opacifie les nœuds et liens non sélectionnés (comme dans le dernier exemple de cette page, il faut cliquer pour sélectionner un nœud). Je pense mettre en place cet effet, à moins que l'on me propose autre chose. Merci pour cette remarque.

Le moteur de recherche indexe uniquement certains mot-clé (matrice, par exemple). Il retourne alors tous les énoncés contenant ce mot-clé. On se rend compte, que ma structure n'est pas très à jour. En effet, la notion de matrice est utile dans certains énoncés, auxquelles la définition de matrice n'est pas reliée de près ou de loin. Je fais essayer de corriger ça. Mais le problème vient du fait, qu'on est obligé de construire toutes ses dépendances dès qu'on écrit un énoncé. Il faudrait pourvoir faire des liens vers des notions qui ne sont pas encore rédigées, pour les compléter plus tard.

J'espère que l'opacité des nœuds non sélectionnés apportera une meilleure lisibilité des recherches sur le graphe.

Voilou

Je viens de mettre en place un système de gestion des versions, donc vous pouvez vous inscrire sur Chère de Prince dès à présent à l'adresse suivante . La page d'identification est ici (au cas où vous la perdiez).

Pour l'instant, je n'ai pas encore fait de tutoriel concernant l'édition des éléments mathématiques, mais vous pouvez déjà essayer d'en modifier ou ajouter. Le fonctionnement est très similaire à celui de Twitter. On mentionne les parents en ajoutant @nom_du_parent dans le contenu de l'énoncé. On peut ajouter du code Latex en ligne entre des $ et à la ligne entre des $$. Le formatage markdown est supporté, et il est conseillé de mettre les notions importantes en gras ou italique, pour un meilleur fonctionnement de la barre de recherche.

Ci-dessus l'interface d'édition de la définition de la suite de Cauchy de nom suite_de_cauchy de parent : suite dans un espace métrique.

En vous souhaitant une bonne édition, je suis à l'écoute de vos questions .

C'est rigolo, ça fait quelques mois que j'avais une idée similaire qui trainait dans ma tête. En tout cas, ton rendu est intéressant =) .

Pour les dépendances, il pourrait être intéressant d'utiliser des assistants de preuve comme Coq/Isabelle qui permettent de donner directement les dépendances =) .

Merci beaucoup Saroupille, ça fait plaisir de savoir que tu as partagé les mêmes idées. Tu sais quel est le niveau de formalisation, qu'il faut fournir pour utiliser Coq ou Isabelle ? Et quelle est la forme des dépendances, qu'on obtient ?

Merci beaucoup victor, j'ai commencé à indenter un fichier, j'aimerais savoir ce que tu en penses. C'est peut être le fichier que tu cherchais, car il gère les informations des éléments mathématiques. Je vais continuer à corriger l'indentation sur les autres fichiers, il y avait un problème entre le nombre d'espaces d'une tabulation sur Github et emacs.

En ce qui concerne tes pistes, j'ai appris des choses :

• Le temps de chargement est très long, mais le serveur est chez moi et la connexion est plutôt mauvaise. Je pense que le problème vient principalement de là. Après les fichiers statiques sont effectivement servis par le serveur node.js, mais production.min.js prend 135ms à charger en local sans le cache. Je ne sais pas, si on peut en déduire quelque chose.
• Tu pointes un problème, que je n'avais pas encore considéré. Tu as raison le graphe est chargé à travers une websocket et c'est lent, même en local. Mais le graphe n'est pas statique, il suit l'évolution de la base de données. Si une entrée est ajoutée, un sommet apparaîtra sur le graphe. Mais il pourrait être chargée par une autre voie que les sockets, et être mis à jour par eux. Et il pourrait être placé dans une variable, mais est-ce que ça change quelque chose par rapport à un appel à la base de données ?
• Ok, sur ce point-là, je ne savais rien. J'ai corrigé autant que j'ai pu, encore merci.

Là où je sens que MongoDb n'en peux plus, ce n'est au chargement de la page, mais lorsqu'un élément est mis à jour. Il peut mettre jusqu'à plusieurs secondes, uniquement pour la commande update, sans le traitement des données. Je te parle ici du temps, que m'indique le console.time('mongo') dans MathElt.js. S'il y a un moyen de diminuer clairement ce temp, ce serait magique !

Si j'ai un peu de temps, j'irai regarder. Le truc, c'est que lorsque tu souhaites formaliser complètement les mathématiques, tu te retrouves à devoir démontrer beaucoup plus de lemmes que ce qui serait fait dans la littérature habituelle.

Par exemple, une fois que tu as défini les entiers, prouver que $x + y = y + x$ n'est pas si simple (notamment car la définition de $+$ est asymétrique).

Au niveau des dépendances, une commande devrait pouvoir te les générer encore faut-il la trouver. Par contre, il faudra faire la correspondance à la main entre le nom des lemmes/théorèmes dans Coq, et ceux que tu veux avoir dans ton graphe. A voir vers quoi tu souhaites mener ton projet.

Merci beaucoup victor, j'ai commencé à indenter un fichier, j'aimerais savoir ce que tu en penses.

C'est vraiment pas top. Je suis pas un utilisateur d'emacs, mais je sais qu'emacs peut indenter automatiquement du JavaScript, n'importe quel éditeur de code peut faire ça, que ce soit emacs, vim, sublime, atom, ou vraiment n'importe quel autre éditeur.

Regarde: 1, 2, 3. C'est que quelques exemples, vraiment c'est pas lisible.

Normalement en une commande emacs tu peux régler ça pour tout le fichier sans t'embêter. Aussi, ne mélange pas les tabs et les espaces.

Je vais continuer à corriger l'indentation sur les autres fichiers, il y avait un problème entre le nombre d'espaces d'une tabulation sur Github et emacs.

Généralement en JavaScript on indente avec 2 espaces, jamais de tabs. Aussi, généralement on met des ;. C'est pas obligatoire, mais vu que t'es pas expert en JavaScript je te recommande vraiment de mettre des ;. Tu peux te permettre de programmer en JavaScript sans ;, mais ça demande de bien connaitre le langage.

• Le temps de chargement est très long, mais le serveur est chez moi et la connexion est plutôt mauvaise. Je pense que le problème vient principalement de là. Après les fichiers statiques sont effectivement servis par le serveur node.js, mais production.min.js prend 135ms à charger en local sans le cache. Je ne sais pas, si on peut en déduire quelque chose.

Non, on ne peut pas en déduire grand chose. Effectivement si le serveur est chez toi et que ta bande passante montante est pas top, servir les assets statiques avec nginx va pas résoudre grand chose.

• Tu pointes un problème, que je n'avais pas encore considéré. Tu as raison le graphe est chargé à travers une websocket et c'est lent, même en local. Mais le graphe n'est pas statique, il suit l'évolution de la base de données. Si une entrée est ajoutée, un sommet apparaîtra sur le graphe.

D'accord, du coup je ne comprends pas bien. Quand je regarde ton site, le graphe ne change pas, rien n'apparait ou disparait. La base de donnée est modifiée à quelle fréquence ? Est-ce que des actions utilisateur peuvent modifier la DB ? Seulement toi ?

Si le graphe en base de donnée n'est pas modifié en permanence, générer le graphe à chaque visite n'a pas de sens. Tu peux simplement le garder en cache côté serveur et invalider le cache dès que la base de donnée change. Regarde :

1. Un visiteur A va sur ton site
2. Node regarde si le cache est valide et contient le graphe, c'est pas le cas donc il génère le graphe, le met dans le cache et l'envoie à A.
3. B va sur le site
4. Node regarde si le cache est valide et contient le graphe, c'est le cas dont il fout la paix à la base de donnée et envoie le graphe depuis le cache (super rapide).
5. Un utilisateur modifie le graphe, ça appelle la fonction modifierGraphe(), qui change le contenu de la base de donnée et indique que le cache n'est plus valide.
6. C va sur le site
7. Node regarde si le cache est valide et contient le graphe, c'est pas le cas, etc, t'as compris l'histoire

Mais il pourrait être chargée par une autre voie que les sockets, et être mis à jour par eux. Et il pourrait être placé dans une variable, mais est-ce que ça change quelque chose par rapport à un appel à la base de données ?

Oui.

Là où je sens que MongoDb n'en peux plus, ce n'est au chargement de la page, mais lorsqu'un élément est mis à jour. Il peut mettre jusqu'à plusieurs secondes, uniquement pour la commande update, sans le traitement des données.

Peux-tu montrer le code qui fait cet update ? Aussi, peux-tu m'expliquer la différence que tu fais entre mettre à jour un élément et traitement des données ?