Preuve par ordinateur

Joaopa
Joaopa
dans Mathématiques et Société
Un article intéressant sur les preuves mathématiques qui utilisent un ordinateur article. En particulier les questions posées par Poonen
[small]
What if the computations are too expensive to do more than once ?
•
What if the computation involves proprietary software (e.g., MAGMA) for which there is no direct way to check that the algorithms do what they claim to do ?
•
Should one insist on open-source software, or even software that has gone through a peer-review process (as in Sage, for instance) ?
•
In what form should computational proofs be published ?
[/small]

Personnellement, quand je dois arbitrer un article où les calculs sont faits sur Magma, Maple ou tout autre logiciel dont le code source n'est pas disponible, je rejette l'article.

Réponses

  • Lupulus
    Lupulus
    En tout cas les progrès vont vite, voir ici : https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean/311123
  • nicolas.patrois
    nicolas.patrois
    Et si on voulait pinailler, on devrait exécuter le programme libre dans un système d’exploitation libre sur un matériel libre.
    Algebraic symbols are used when you do not know what you are talking about.
            -- Schnoebelen, Philippe
  • mojojojo
    mojojojo
    Pourquoi ne pas poser la question aux autres scientifiques d'autres domaines ? Ces questions sont très récentes pour les mathématiques mais ça l'est moins pour la physique.

    Je suppose que certaines expériences du CERN sont suffisamment coûteuses, longues et compliquées pour ne pas être faites ailleurs. Je suppose que les lasers et microscopes électroniques des physiciens sont tous des appareils "propriétaires" et que leurs plans ne sont pas libres de droit. Je ne pense pas que les articles de physique soient rejetés pour ces raisons.

    D'ailleurs Joaopa, est-ce que les éditeurs te laissent une liberté totale pour accepter/refuser un papier ? On pourrait imaginer que cela fasse parti de la ligne éditoriale du journal de dire "on accepte les papiers avec du mapple" ou "on n'accepte pas les papiers avec du mapple".
  • noix de totos
    noix de totos
    Lire aussi ce preprint : https://arxiv.org/pdf/1809.08062.pdf
  • Joaopa
    Joaopa
    nicolas.patrois écrivait:
    > Et si on voulait pinailler, on devrait exécuter le programme libre dans un système d’exploitation libre sur un matériel libre.

    Je ne comprends pas ton objection. Ce qui est important, ce ne sont pas les résultats par les auteurs mais la vérification faite par les arbitres. Évidemment qu'en tant qu'arbitre, je vais faire les vérifications avec ces contraintes ou au moins sur du matériel qui a été certifié correct (certifié par la communauté et non par le fabricant ;))

    Maple, Magma ne sont pas certifiés eux.
  • Rescassol
    Rescassol
    Bonjour,

    Est ce que Matlab est certifié ?

    Cordialement,

    Rescassol
  • Héhéhé
    Héhéhé
    Un problème est que, comme le dit si bien David Madore, les logiciels libres sont assez à la ramasse par rapport à leurs concurrents non libre:
    David Madore a écrit:
    Malheureusement ce n'est pas du tout le cas de celui qui fait aujourd'hui référence en matière de calculs informatiques en algèbre et géométrie algébrique (et qui, même si Sage fait des progrès très rapides et très spectaculaires, domine tous les autres à peu près autant qu'un moine Shaolin m'éclaterait en combat singulier), à savoir Magma.
    Pour consulter l'article est entier, c'est ici.

    C'est pareil en calcul scientifique, Matlab est bien en avance par rapport à Scilab ou aux bibliothèques Python...

    Donc quid de calculs qui sont fait sur des logiciels propriétaires et qui ne sont pas faisables sur leurs équivalents libres ? Je n'ai pas la réponse...
  • nicolas.patrois
    nicolas.patrois
    Joaopa a écrit:
    http://www.les-mathematiques.net/phorum/read.php?9,1714802,1715064#msg-1715064

    Et comment peux-tu certifier un matériel non libre ? Pas plus qu’un logiciel non libre.
    Je veux juste dire que, selon les limites des gens, eh bien untel acceptera de travailler dans Scilab dans Windows, un autre n’acceptera que dans un Linux vérifié par vrms et un autre que sur du matériel libre avec un Linux libre et un logiciel libre.
    Algebraic symbols are used when you do not know what you are talking about.
            -- Schnoebelen, Philippe
  • Héhéhé
    Héhéhé
    Si on accepte le matériel certifié par la communauté on devrait aussi accepter les logiciels certifiés par la communauté ce qui est le cas vu les milliers d'utilisateurs de Maple, MATLAB etc. chaque jour.

    J'ai l'impression que cette quête du tout certifié est une impasse, qui ressemble un peu au fait de vouloir des démonstrations formelles dans les papiers...
  • Romyna
    Romyna
    Jusqu'à la preuve du contraire, quand on parle d'ordinateurs ou de programmes logiciels et matériels afférents, il s'agit d'assistants de preuves!
  • Fin de partie
    Fin de partie
    Les systèmes d'exploitation libres tournent sur des machines qui fonctionnent avec du code qui n'est pas libre: c'est matériel, un ordinateur a un bios, une carte graphique aussi etc et tous ces bouts de code qui sont au coeur de ces matériels ne sont pas libres.

    PS:
    Vous avez entendu parler de MINIX?

    L'"OS" le plus utilisé dans le monde:

    https://fr.wikipedia.org/wiki/Minix
  • Joaopa
    Joaopa
    Il existe des processeurs libres avec microprogramme d'amorçage libre.
  • Tryss
    Tryss
    Certes, mais peux-tu vérifier toi-même la bonne implémentation physique du matériel ?

    Qu'est-ce qui t'assure que le circuit qui a été gravé est bien le circuit supposé ?
  • Fin de partie
    Fin de partie
    Joaopa:

    Quid de la carte graphique et autres périphériques?

    Je croyais naïvement que les microprocesseurs contenaient seulement des bouts de code minimum pour pouvoir charger un OS.

    Les microprocesseurs d'INTEL, semble-t-il, contiennent une déclinaison d'UNIX, MINIX. On est loin de la séquence d'amorçage.
  • Romyna
    Romyna
    Le chargement du programme initial est l’amorçage (ou bootstrap en anglais). Il suffit de s'instruire de la séquence au démarrage de l'ordinateur.
  • Fin de partie
    Fin de partie
    Tu retardes de plusieurs générations de processeurs, comme moi il y a encore récemment.
    Les microprocesseurs d'INTEL ont du code "embarqué" qui peut faire beaucoup plus que charger un OS.

    C'est plutôt:

    https://fr.wikipedia.org/wiki/Unified_Extensible_Firmware_Interface

    qu'il faut lire à mon humble avis.
  • Romyna
    Romyna
    RESET et BOOT: Ces propriétés non propres aux µP d'INTEL sont vraies pour toute architecture de microcontrôleur avec ROM et/ou coprocesseur. !
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 8

AmadouMatricule_63 +6 Invités