Chère de Prince

Un recueil collaboratif d'énoncés mathématiques

a marqué ce sujet comme résolu.

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 :) . Mais aujourd'hui, c'est mon graphe fétiche, que je te présente : Chère de Prince, un graphe de math.

Une vue d'ensemble du graphe

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.

Exemple d'utilisation au près de la notion de graphe.

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

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

Au

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

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

Kje

Je ne complote rien du tout :P

+0 -0

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

Au

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

+1 -1

Salut Demandred,

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 !

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.

Tu trouves que le design est trop simple ?

Je ne dirai pas "simple" non, mais je dirais plutôt "austère" : fond noir avec du vert.

Tu verrais plus d'information présente sur le graphe ?

Pas plus d'informations forcement, mais plutôt une présentation visuelle qui aiderait à mieux s'y retrouver. Par exemple si je cherche "matrice" et que je ne zoom pas, on ne peut pas dire que le graphe m'apporte grand chose comme information si ? (screen). Personnellement je vois un tas de noeuds et de lien, mais je n'arrive à me dire "tient la notion est matrice est connectée à telle autre notion", ce qui est pourtant le but de ton outil je crois.

Sur ce screen, pourquoi certains noeuds sont cerclés, d'autres cerclés avec un affichage à coté, et enfin d'autres sont en bleu ?

Tu trouves que ça manque d'aide pour la navigation ?

Oui^^

Tu penses que mettre des images sur les nœuds rendrait le graphe plus lisible ?

Hum pas forcement des images, sauf si tu peux classer les objets dans des grandes catégories et que cela ajouterait une information suplémentaire (par exemple une icone "algèbre", une "géomérie" etc). Mais je doute qu'une telle classification soit possible… :p

Pour moi actuellement je trouve le graphe difficile à manipuler et que du coup il apporte peu d'information visuellement parlant. Par exemple si je cherche "matrice" et que je zoom sur le noeud, voici ce que je vois : http://prntscr.com/aw5hx9

Je ne vois clairement aucun noeud directement en lien avec "matrice", mais je vois plein de noeuds qui n'ont au contraire rien à voir ! Par exemple la notion de "norme" en haut à gauche et cerclé de blanc, qui est à de nombreuses arrêtes de distances.

Il ne serait pas possible quand on clic sur un noeud de n'afficher que les noeuds adjacent et eventuellement ceux à 2 arrêtes de distances ? Comme ça on pourrait visualiser vraiment à quoi une notion est connectée, ce qui est le but du projet non ?

Là quand je clic sur matrice je ne suis pas capable de voir les connections et les explorer et j'ai à l'inverse plein d'infos "inutiles" sur les éléments qui sont autour et qui "polluent" la navigation et l'exploration.

Après ce n'est que mon avis personnel et c'est tout à fait possible que je ne sois pas le public visé pour un tel outil ce qui expliquerai pourquoi j'ai du mal à bien l'utiliser.

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

Alors moi je m'occupais uniquement de la partie graphique et de proposer des idées, ce n'est pas moi qui codait mais si je me souvient bien c'était du javascript vanilla, sans librairie particulière et avec une base de donnée SQL classique. Tu peux voir le site qui est toujours en ligne ici : www.nodynotes.com

Une nouvelle version est je crois disponible sur le github de l'auteur, avec un nouveau design et un nouveau code.

Voilà :)

+1 -0

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

affichage de l'édition

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 =) .

Salut !

C'est un chouette projet, belle idée en tout cas !

J'ai un peu jeté un oeil au code, parce que je connais bien JS et MongoDB et que je peux peut-être jeter un oeil aux performances et proposer des solutions (des solutions autres que passer par une DB graphe genre Neo4j ou passer par du RDF et une DB RDF genre Virtuoso, qui sont très très puissantes pour résoudre ton problème, mais sont difficiles à appréhender). Mais un truc m'a beaucoup refroidi : le code n'est pas vraiment indenté. Ca parait bête dit comme ça, mais c'est pas lisible. J'ai commencé à chercher l'endroit où tu fais une requête pour trouver les enfants d'un noeud, mais j'ai vite abandonné devant l'indentation.

Si j'étais toi, je corrigerais d'abord ça. L'indentation JS et HTML (tes .ejs).

[EDIT] Bon, au lieu de regarder le code sur github, j'ai regardé le comportement du site dans mon navigateur. Quelques pistes, en vrac :

  • Est-ce que les assets statiques sont servis par node ou par nginx ? Ils se chargent tellement lentement que je suspecte la première option. production.min.js pèse 123k, mais il met 5.43 secondes à charger ! C'est au moins 10x trop long. Idem pour production.min.css : 12.8k en 1.39s.
  • Les données du graphe semblent chargées à la volée depuis Mongo et envoyées sur une websocket. C'est pas une bonne idée. Ton graphe est complètement statique sauf erreur. Du coup, tu devrais le cacher côté serveur, et seulement le générer quand son contenu dans la DB a changé. S'il est statique, le servir par une websocket est contreproductif.
  • Côté JS, j'ai remarqué que tu delete des propriétés de gros objets ou que tu fais ça dans des boucles. Tu devrais supprimer toute utilisation de delete dans ton code. Tu peux par exemple remplacer delete obj.prop par obj.prop = null. Un objet qui a subit le delete d'une de ses propriétés passe directement en "dictionary mode", ce qui rend l'accès à ses autres propriétés au moins 10x plus lent. (Quelques exemples dans ton code, mais y'en a d'autres: 1, 2, 3, 4).

Voilà, si tu mets ça en place la page pourrait bien charger 10x plus vite au bas mot. Actuellement elle met plus de 10s chez moi, à froid.

+1 -0

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 ! :)

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 ?

la Bécasse

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.

+0 -0

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 ?

+0 -0
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte