Preuve par ordinateur
Un article intéressant sur les preuves mathématiques qui utilisent un ordinateur article. En particulier les questions posées par Poonen
[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.
[small]
[/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 ?
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.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
-- Schnoebelen, Philippe
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".
> 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.
Est ce que Matlab est certifié ?
Cordialement,
Rescassol
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...
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.
-- Schnoebelen, Philippe
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...
PS:
Vous avez entendu parler de MINIX?
L'"OS" le plus utilisé dans le monde:
https://fr.wikipedia.org/wiki/Minix
Qu'est-ce qui t'assure que le circuit qui a été gravé est bien le circuit supposé ?
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.
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.