codage de théorèmes

Bonjour
J'écris ce post car j'ai l'impression que quelque chose qui devrait exister dans le monde des mathématiques n'existe pas, et c'est bien dommage.
Il m'arrive souvent de chercher un résultat précis de maths, et je n'ai aucun idée d'où le trouver, à part en faisant des recherches sur google, arxiv, ou autres (google donnant en général les meilleurs résultats). Par exemple, je dispose d'une série de fonctions convexes sur [0,1]^2, dont je maitrise le gradient, et je voudrais savoir si il existe une condition sur le gradient qui me donne l'équicontinuité de la famille. Je me dis qu'il existe forcément un résultat de ce type quelque part, mais après trois jours de recherches je n'ai rien trouvé.
Je m'y prends probablement mal ou manque de culture mathématique, mais je sais qu'il existe par exemple des outils de "vérification de preuves", ou beaucoup de notions mathématiques ont été codées. Je me demande pourquoi il n'existe pas une base de données de théorèmes, qui seraient par exemple codés de la fonctions suivantes:
-Objets:
Suite de fonctions convexes sur un compact de Rn ou R2

-Hypothèses sur:
Gradient des fonctions

-Résultats sur:
Convergence uniforme, équicontinuité

Je pense que tout ceci n'est pas trop difficile à coder au vu de ce qu'on sait faire en "vérification de preuves", et si ça l'est ça serait sans doute un bon investissement dans tous les cas...Dés que quelqu'un trouve un résultat qu'il référence dans un livre ou un papier, il pourrait le mettre en ligne, je pense que tout le monde gagnerait énormément de temps...
Bon, fin de mes élucubrations, je serais en tout cas très intéressé par votre avis sur tout ça.

Réponses

  • On pourrait faire mieux: donner l'arbre des théorèmes de sorte qu'on aurait la démonstration en même tps que l'énoncé

    J'avais proposé ce chantier ici ds je ne sias plus quel fil, plutot qu'une gazette
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • raphayel : cela pose des questions non triviales d'isomorphisme de type. Il faut que ton système soit capable de savoir te donner un théorème à partir d'un énoncé qui peut être équivalent mais très différent. Par exemple, il te faut une définition standard d'être continue, et tu as des définitions diffèrentes mais équivalentes (par exemple avec les epsilon ou avec les suites), et parfois l'équivalence utilise des propriétés fortes (dans ce cas-là l'axiome du choix dépendant).
    Tu pourrais me dire et les numéro de Godel alors ? et je te dirais qu'un énoncé théorème correspondant à une classe d'équivalence des entiers pour la relation déduite de ces isomorphismes.
  • Bonjour
    Deufeufeu, je suis tout à fait d'accord avec tes remarques sur les problèmes logiques, mais je parle plutôt d'un outil de recherche que d'un véritable algorithme. Pour les mêmes raisons d'instabilité il serait difficile de prévoir un arbre.
    Quand je tape des mots clés sur arxiv, je tombe sur plein d'article qui n'ont finalement rien à voir avec mon problème, et quand je le tape sur google je tombe sur plein de trucs qui ne sont parfois pas des papiers.
    Je me dis qu'il y a forcément mieux à faire. Je te parle d'un codage mi mots-clés mi objets mathématiques du type
    objets :
    K : sous-ensemble -> R2 / Rn -> compact, convexe
    (fn) : Suite -> application -> de K -> vers R -> convexe , C^1
    hypothese :
    grad(fn), distribution
    conclusions :
    convergence (fn)/équicontinuité (fn)

    Evidemment c'est très simplistes ici, mais on peut surement trouver quelque chose de mieux.
    Après je ne parle pas d'un algorithme qui saurait relier entre eux tous les théorèmes équivalents (d'ailleurs dans ce cas on aurait plus besoin de mathématiciens..:D)
  • Euh...je n'ai rien trouvé. Tu pensais au livre? ceci dit je ne pensais pas que google pouvait retourner quelque chose de valable avec autant de mots clés.
  • oui il faut mettre des guillemets mais le lien ne passait pas, enfin c'était plutôt pour t'indiquer le site scholar.google.com qui donne de meilleurs résultats sur ce genre de recherche que le plain old google.
  • En effet je connaissais, merci en tout cas.
  • J'en profite pour poser la question qui tue: c'est quoi un gradient?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Quand tu as une fonction de $R^n$ vers $R$, le gradient de f en $x \in R^n$ c'est le vecteur de $R^n$ dont les $n$ coordonnées sont les $n$ dérivées partielles de $f$ $(\frac{\partial f}{\partial x_i}(x))$. C'est notamment un outil qui t'indique la direction et la variation de ta fonction en un point.
  • Christophe,

    Tu as entendu à la météo l'expression "gradient de pression" ou de température.

    Lorsque tu prends une carte des lignes de niveau (isobares ou isothermes en météo), c'est un vecteur dont la direction t'indique la ligne de plus grande pente c'est à dire la direction du vent, mets-toi à sa place, et dont la norme t'indique si la pente est raide ou non (si ça va souffler fort ou pas).

    Dans le cas du champ électrique, les lignes de niveau sont les équipotentielles et le gradient est tangent aux lignes de champ. Les lignes de champ sont perpendiculaires aux équipotentielles. C'est grosso modo le théorème des fonctions implicites.

    amicalement,

    e.v.
    Personne n'a raison contre un enfant qui pleure.


  • Merci ev, mais ces images électriques et venteuses me dépassent un peu, je veux bien "sentir", mais formellement, la définition du gradient c'est quoi?

    (D'après ce que tu me dis, ce serait des sortes de perpendiculaires aux lignes de niveau sur une carte de l'IGN par exemple, mais je ne peux guère "comprendre" plus...
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Imagine que tu escalades une colline, que tu es à un point (x,f(x)) (La colline est le graphe de $f$...). Tu prends une flèche de 1 mètre de long dans ton sac à dos et tu la poses à tes pieds dans la direction où la pente est la plus raide (vers le haut). Eh bien la projection de cette flèche sur le sol ($R^2$) c'est le gradient de la fonction f en $x$. Quand tu regardes du haut tous les gradients de $f$ sur $R^2$ tu as plusieurs informations: En ne faisant que suivre des flèches tu suivras toujours un chemin de pente maximale, et si en revanche tu suis un chemin orthogonal à toutes les flèches qu'il croise ça veut dire que tu ne changes pas de niveau (tu suis une ligne de niveau).
  • Merci, hip hip hip oura, je suis content, donc lignes de niveau perpendiculaires à un truc (et là je ne l'avais vu dans le discours d'ev) dont la projection est le gradient.

    Le gradient est donc un panneau routier (enfin en escalade..) pour descendre le plus vite..
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Tout bien réfléchi ce que je t'ai dit est faux...:D Il ne faut pas projeter les flèches en bas, car ça marche pour avoir la direction du gradient mais pas la norme (sinon les endroits avec pente forte auraient un gradient faible, ce qui est contradictoire...), en fait comme norme il faut prendre la projection sur l'axe des z...Voilà j'espère que c'est toujours clair.
  • Mais le gradient lui-même, c'est quoi, c'est la norme de la projection verticale d'un vecteur unitaire tangent à une des pentes maximum, précisément?

    [size=x-small]Merci, de toute façon, je survole surtout pour situer ces mots dans des contextes visuels, après je verrai si je me sens le courage de tout reformaliser et démontrer.

    J'ai un nombre extraordinaire de problèmes personnels urgents, et je suis presque en état de haine de devoir m'occuper de "maths" actuellement, accidentellement, j'avais juré récemment d'en divorcer au moins quelques années, par nécessité de survie psy (elles me servent de digression, de rèverie superficielle).

    Donc tu peux y aller, les erreurs ne me gènent pas, ni même les délires, je pose divers questions pour avoir une vue d'ensemble, pour ensuite prendre une décision mature sur le fait que je les approfondirai ou pas, mais l'idéal serait que je ne pense pas à tout ça (mais je ne veux pas le décider à la légère) et ne vienne plus ici, ni ailleurs d'ailleurs (livres etc).[/size]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Non c'est le vecteur projeté en bas avec la norme de la projection verticale (c'est donc un vecteur de R^2 dans notre cas)
Connectez-vous ou Inscrivez-vous pour répondre.