Un zeste de mathématiques assistées par ordinateur

ou comment construire et vérifier des preuves automatiquement

a marqué ce sujet comme résolu.
Auteur du sujet

Tout le monde se secoue ! :D

J’ai commencé (il y a 3 heures) la rédaction d’un article au doux nom de « Un zeste de mathématiques assistées par ordinateur » et j’ai pour objectif de proposer en validation un texte aux petits oignons. Je fais donc appel à votre bonté sans limites pour dénicher le moindre pépin, que ce soit à propos du fond ou de la forme. Vous pourrez consulter la bêta à votre guise à l’adresse suivante :

Merci !


Il me manque les images, mais c’est une version quasi-finale à mes yeux.

Tous types de retours sont les bienvenus !

Édité par Aabu

+4 -0

Salut,

Super contenu et tu as trouvé le bon univers avec des petits théorèmes sympas pour ça. :) Tu as inversé le rewrite <- sym_n_s. et le rewrite <- rotd_n_o. dans la preuve que tu donnes. La preuve reste correcte bien sûr, c’est juste que tu dis qu’on fait la preuve dans le sens inverse, donc on s’attend à avoir l’ordre inversé par rapport à la preuve informelle.

Assez des salamis, je passe au jambon — Je fais un carnage si ce car nage car je nage, moi, Karnaj ! — Le comble pour un professeur de mathématique ? Mourir dans l’exercice de ses fonctions.

+0 -0
Auteur du sujet

Bonjour les agrumes !

La bêta a été mise à jour et décante sa pulpe à l’adresse suivante :

Merci d’avance pour vos commentaires.


Merci pour le retour, c’est corrigé. J’en ai profité pour corriger quelques autres fautes de frappes et maladresses.

Il faut que je m’attaque aux figures !

Édité par Aabu

+0 -0

Une question très naïve après un premier survol de l’article: pourquoi définir tes opérations sur des points comme des variables opaques, au lieu de les définir comme des fonctions (et donc les propriétés seraient des lemmes sur ces fonctions au lieu d’axiomes) ? Est-ce que c’est prévu pour dans un second temps ?

+0 -0
Auteur du sujet

Une question très naïve après un premier survol de l’article: pourquoi définir tes opérations sur des points comme des variables opaques, au lieu de les définir comme des fonctions (et donc les propriétés seraient des lemmes sur ces fonctions au lieu d’axiomes) ? Est-ce que c’est prévu pour dans un second temps ?

gasche

C’est un choix. L’idée c’est de faire des maths qui ressemblent aux maths habituelles, en ayant quelques axiomes et en démontrant des propriétés. Je n’ai volontairement pas introduit de fonctions, parce que ça sort de cet objectif. Ce ne sera donc pas non plus dans un second temps (a priori).

Ceci dit on pourrait tout à fait définir exhaustivement les fonctions, mais les démonstrations deviennent moins amusantes, parce qu’en gros il suffirait probablement de destruct et unfold dans tous les sens pour arriver à n’importe quel résultat. Là avec les axiomes, il y a beaucoup d’implicite, et je voulais le garder pour que les démonstrations ne ressemblent pas à de l’exhaustion de cas.

Une variante avec définitions pourrait être un autre petit article qui présente l’extraction de code, mais je n’ai pas prévu d’en écrire un. En fait, avant les choix que j’ai faits, j’avais tenté une petite fonction amusante qui rend une transformation permettant de retrouver le nord depuis n’importe quel point avec seulement les opérations élémentaires. C’était assez artificiel et pas très amusant.


Je viens de mettre à jour la bêta avec une figure pour illustrer.

@gasche : après réflexion, un article sur l’extraction de code serait sûrement intéressant, mais il faudrait prendre une approche plus orientée langage de programmation. Il faudrait un univers un peu plus riche. Je pense par exemple à un optimiseur de parcours qui opérerait sur un damier, et il s’agirait alors de prouver des théorèmes sur les simplifications possibles (par exemple tourner trois fois à droite revient au point de départ).

Édité par Aabu

+0 -0

Je viens de lire un peu en diagonale. Et moi qui ait un a priori plutôt négatif sur Coq (un de mes potes adoraient ça et m’a bien saoûlé avec), tu m’as presque donné envie d’en faire !

Un boulot très quali, bravo ! :)

+0 -0

Le choix actuel me convient. Par contre je pense que dans ta réponse tu fais un lien un peu trop fort entre "définir des fonctions" et "extraire du code". Même quand on n’essaie pas d’écrire un programme, mais une preuve mathématique, il peut être utile de manipuler des objets au comportement calculatoire (dans le cas de ton article, c’est même "trop utile" puisque comme tu le dis cela trivialise les preuves). D’ailleurs la bibliothèque SSR en Coq, qui a été développée pour faire des maths (et pas de la programmation), tient son nom de "Small Scale Reflection", une technique de preuve qui utilise beaucoup de petits calculs locaux.

+0 -0

Bonjour,

La bêta du contenu « Un zeste de mathématiques assistées par ordinateur » a été désactivée.

I don’t mind that you think slowly, but I do mind that you are publishing faster. — W. Pauli

+0 -0
Ce sujet est verrouillé.