J’interprète peut-être de travers. Corrigez-moi si j'abuse. L'erreur soulevée par l'outil de preuve numérique est d'un type qu'on reprocherai à un élève de première. Évidemment tout le monde est faillible et commet de belles bourdes dans ses papiers, ses cours… mais en arriver là pour un papier de preprint interroge quelque peu sur la qualité des publications scientifiques à l'heure de l'évaluation quantitative de la recherche (par le nombre de publis).
Posté par BAud (site web personnel) .
Évalué à 8.
Dernière modification le 25 octobre 2023 à 18:29.
mais en arriver là pour un papier de preprint interroge quelque peu sur la qualité des publications scientifiques
euh, c'est la méthode scientifique
la capacité de révocation / correction / amélioration fait partie de la preuve, justement
même un résultat publié y sera éprouvé et tant mieux
Andrew Wiles est passé de ~1500 pages à ~4000 pages pour convaincre de sa démonstration de la conjecture de Fermat qui ne tenait pas dans la marge…
à l'heure de l'évaluation quantitative de la recherche (par le nombre de publis).
ça, c'est une connerie qui n'a rien de scientifique (même si subi /o\)
les références sont bien connues (et reconnues :p)
Posté par Thomas Douillard .
Évalué à 3.
Dernière modification le 25 octobre 2023 à 18:38.
Oui ça a toujours existé que les matheux fassent des trucs dans leurs cahiers sans forcément les publier pour une raison X ou Y, pas suffisamment intéressant par exemple.
Maintenant c’est publié plus facilement, sans garantie de relecture non plus mais plus facilement accessible pour quelqu’un qui aurait besoin d’un résultat.
Et sur l’évaluation, pas certain que les prépublis comptent beaucoup en général !
La le truc intéressant c’est comment la communauté mathématique peut prendre possession de l’outil des assistants de preuve, avec une tête d’affiche comme Terence Tao qui documente sa progression et son usage.
Ba est-ce que c'est pas un peu comme les compilateurs ?
Il est facile pour les vieux qui ont connu les cartes perforées d'arguer qu'à leur époque on vérifiait pendant 3 jours son programme avant de l'envoyer à l'assistant vu qu'il fallait une semaine pour avoir le résultat.
Aujourd'hui on code comme des sagouins car en moins de 2 minutes (compilation itérative) le compilo nous diras qu'on a oublié ici un ;, ici que la méthode est constante et qu'on ne peut donc pas modifier l'état de la classe.
Est-on devenu idiot ? Plus capable d'un raisonnement de type lycée ? Je ne crois pas, on se concentre sur plus important que cette fichue indentation (ba ouais c'est géré par mon linter).
Vous avez vu qui est l'auteur du pre-print en question ?
Vous avez bien conscience que c'est le n plus grand mathématicien vivant, où n ≤ 5 ??
Autant on peut avoir des questionnements légitimes sur la qualité des publications en général, autant je ne crois pas qu'on puisse soupçonner Terence Tao d'avoir besoin de réputation et d'être donc dans la hâte pour maximiser son nombre de publications.
Non seulement n’ai-je pas la moindre idée de qui est l’auteur, ou de la norme à employer pour définir un opérateur de comparaison entre mathématiciens, mais encore n’ai-je aucune prétention quant à ma propre science, sans négliger que j’ignore tout de l’article en question n’ayant lu que le lien pointé, sans bibliographie, aucune. Lien qui indique assez explicitement que l’auteur s’intéressait aux cas des n grands. Qu’importe. Ma remarque est très ponctuelle : la plupart des secondes savent que a/y n’est pas défini pour y=0. Les premières connaissent les logarithmes réels et aucun n’ignore que log(y) est défini pour y>0. Je trouve inquiétant que seul un outil de preuve ait détecté une telle coquille, tout de même sensiblement plus connexe au domaine que les conjugaisons ou la syntaxe. Ni plus, ni moins. Et surtout pas avec un jugement négatif de l’auteur qui semble avoir l’honnêteté de discuter de l’étourderie, allant même en assurer la publicité sur des réseaux sociaux là où le quidam (oserais-je écrire, le Pékin moyen ? Oups. Désolé :-) ce serait empressé de cacher l’étourderie sous les premiers tapis venus. Le seul soupçon d’opinion que j’en tire sur lui : probablement un bon enseignant.
Au cas ou le post serait dénué de toute intention trollesque et d’une ingénuité sans faille, voilà un lien vers son article Wikipédia Terence Tao. Perso je résumerai sa bio à "l’homme qui a tenté de créer un ordinateur liquide" https://www.scientificamerican.com/article/a-fluid-new-path-in-grand-math-challenge/ (pour montrer que les équations de la mécanique des fluides sont au moins aussi difficile à résoudre que le problème de l’arrêt en informatique)
Mon Français est-il vraiment si mauvais ? Dans ce que j'écrivais il est question du domaine de définition de la fonction f(y)=a/y, et de la course à la publication. Rien d'autre. Il me semblait avoir fait tout mon possible pour que ce soit bien explicite. Désolé si ce n'est toujours pas clair. L'expression écrite n'est pas un art maîtrisée par tous. Mille excuses.
Je trouve inquiétant que seul un outil de preuve ait détecté une telle coquille, tout de même sensiblement plus connexe au domaine que les conjugaisons ou la syntaxe.
Je sais depuis ma première année d'étude post bac ce qu'est est comment éviter les buffer overflow, c'est pas pour ça que c'est simple à détecter et éradiquer dans nos code.
De ma compréhension, ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ s’émeut pour une erreur d’inattention et on lui fait le procès de ne pas connaitre l’auteur ou on veut faire croire que c’est hyper complexe.
Pour moi, on est typiquement dans un cas plus ou moins courant qui est normalement détecté à la relecture. Et ce que pointe le lien est que l’outil permet de gagner du temps et d’avoir de la confiance alors que traditionnellement il aurait fallu que beaucoup de paire d’yeux y passent énormément de temps. C’est assez différent du BOF
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
Pour répondre à ton interrogation initiale, « l'erreur soulevée par l'outil de preuve » n’est pas vraiment une erreur dans l’absolu (du moins n’est pas perçu comme une erreur par les relectures parce-que cela semble aller de soi pour les humains dans le domaine) mais plutôt une ambigüité (pour l’ordinateur qui n’aime pas ça car étant juste basiquement manichéen.) Il y a donc une reformulation à faire pour que les outils ne partent pas dans des directions fausses (et se retrouve dans une impasse qu’elle ne comprend pas.)
Donc, plutôt qu’une bourde de calcul, c’est plus de la subtilité de formulation des conditions qui bornent la démonstration. Du coup, la prépublication était et reste de qualité, mais devient doublement carré on va dire. Accessoirement, cela répond un peu à ta crainte : l’auteur fait du raffinement au lieu de passer à autre chose pour faire du quantitatif.
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
La preuve de programme sert à montrer qu’un programme est correct vis-à-vis de ce qu’on veut lui faire faire. Pour ça on fait des maths sur un langage avec ses types et ses termes et structures de contrôle.
La preuve tout court sert à montrer qu’un raisonnement est correct pour démontrer une propriété. Pour ça dans les assistant de preuve on utilise des … types pour coder les propriétés en question. Cf. La leçon inaugurale de Xavier Leroy par exemple, mais il y a d’autres ressources. Et on écrit la preuve comme on écrirait un programme mais avec une logique un peu différente. Et une fois qu’on a fait ça dans certain cas on peut … compiler la preuve pour avoir un programme exécutable et correct : https://coq.inria.fr/refman/addendum/extraction.html
# Première
Posté par ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ (site web personnel) . Évalué à 5.
J’interprète peut-être de travers. Corrigez-moi si j'abuse. L'erreur soulevée par l'outil de preuve numérique est d'un type qu'on reprocherai à un élève de première. Évidemment tout le monde est faillible et commet de belles bourdes dans ses papiers, ses cours… mais en arriver là pour un papier de preprint interroge quelque peu sur la qualité des publications scientifiques à l'heure de l'évaluation quantitative de la recherche (par le nombre de publis).
« IRAFURORBREVISESTANIMUMREGEQUINISIPARETIMPERAT » — Odes — Horace
[^] # Re: Première
Posté par Thomas Douillard . Évalué à 3.
C’est un pre-print, il n’a pas l’air publié en revue pour l’instant ?
[^] # Re: Première
Posté par BAud (site web personnel) . Évalué à 8. Dernière modification le 25 octobre 2023 à 18:29.
euh, c'est la méthode scientifique
la capacité de révocation / correction / amélioration fait partie de la preuve, justement
même un résultat publié y sera éprouvé et tant mieux
Andrew Wiles est passé de ~1500 pages à ~4000 pages pour convaincre de sa démonstration de la conjecture de Fermat qui ne tenait pas dans la marge…
ça, c'est une connerie qui n'a rien de scientifique (même si subi /o\)
les références sont bien connues (et reconnues :p)
[^] # Re: Première
Posté par Thomas Douillard . Évalué à 3. Dernière modification le 25 octobre 2023 à 18:38.
Oui ça a toujours existé que les matheux fassent des trucs dans leurs cahiers sans forcément les publier pour une raison X ou Y, pas suffisamment intéressant par exemple.
Maintenant c’est publié plus facilement, sans garantie de relecture non plus mais plus facilement accessible pour quelqu’un qui aurait besoin d’un résultat.
Et sur l’évaluation, pas certain que les prépublis comptent beaucoup en général !
La le truc intéressant c’est comment la communauté mathématique peut prendre possession de l’outil des assistants de preuve, avec une tête d’affiche comme Terence Tao qui documente sa progression et son usage.
[^] # Re: Première
Posté par alkino . Évalué à 5.
Ba est-ce que c'est pas un peu comme les compilateurs ?
Il est facile pour les vieux qui ont connu les cartes perforées d'arguer qu'à leur époque on vérifiait pendant 3 jours son programme avant de l'envoyer à l'assistant vu qu'il fallait une semaine pour avoir le résultat.
Aujourd'hui on code comme des sagouins car en moins de 2 minutes (compilation itérative) le compilo nous diras qu'on a oublié ici un
;, ici que la méthode est constante et qu'on ne peut donc pas modifier l'état de la classe.Est-on devenu idiot ? Plus capable d'un raisonnement de type lycée ? Je ne crois pas, on se concentre sur plus important que cette fichue indentation (ba ouais c'est géré par mon linter).
[^] # Re: Première
Posté par jeanas (site web personnel, Mastodon) . Évalué à 2.
Euh… je suis un peu interloqué.
Vous avez vu qui est l'auteur du pre-print en question ?
Vous avez bien conscience que c'est le n plus grand mathématicien vivant, où n ≤ 5 ??
Autant on peut avoir des questionnements légitimes sur la qualité des publications en général, autant je ne crois pas qu'on puisse soupçonner Terence Tao d'avoir besoin de réputation et d'être donc dans la hâte pour maximiser son nombre de publications.
[^] # Re: Première
Posté par ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ (site web personnel) . Évalué à 4.
Non seulement n’ai-je pas la moindre idée de qui est l’auteur, ou de la norme à employer pour définir un opérateur de comparaison entre mathématiciens, mais encore n’ai-je aucune prétention quant à ma propre science, sans négliger que j’ignore tout de l’article en question n’ayant lu que le lien pointé, sans bibliographie, aucune. Lien qui indique assez explicitement que l’auteur s’intéressait aux cas des n grands. Qu’importe. Ma remarque est très ponctuelle : la plupart des secondes savent que a/y n’est pas défini pour y=0. Les premières connaissent les logarithmes réels et aucun n’ignore que log(y) est défini pour y>0. Je trouve inquiétant que seul un outil de preuve ait détecté une telle coquille, tout de même sensiblement plus connexe au domaine que les conjugaisons ou la syntaxe. Ni plus, ni moins. Et surtout pas avec un jugement négatif de l’auteur qui semble avoir l’honnêteté de discuter de l’étourderie, allant même en assurer la publicité sur des réseaux sociaux là où le quidam (oserais-je écrire, le Pékin moyen ? Oups. Désolé :-) ce serait empressé de cacher l’étourderie sous les premiers tapis venus. Le seul soupçon d’opinion que j’en tire sur lui : probablement un bon enseignant.
« IRAFURORBREVISESTANIMUMREGEQUINISIPARETIMPERAT » — Odes — Horace
[^] # Re: Première
Posté par kantien . Évalué à 6.
Ce genre d'étourderie arrive aux meilleurs,
57 (3*19)étant connu comme le nombre premier de Grothendieck.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Première
Posté par Thomas Douillard . Évalué à 3.
Au cas ou le post serait dénué de toute intention trollesque et d’une ingénuité sans faille, voilà un lien vers son article Wikipédia Terence Tao. Perso je résumerai sa bio à "l’homme qui a tenté de créer un ordinateur liquide" https://www.scientificamerican.com/article/a-fluid-new-path-in-grand-math-challenge/ (pour montrer que les équations de la mécanique des fluides sont au moins aussi difficile à résoudre que le problème de l’arrêt en informatique)
[^] # Re: Première
Posté par ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ (site web personnel) . Évalué à 3.
Mon Français est-il vraiment si mauvais ? Dans ce que j'écrivais il est question du domaine de définition de la fonction f(y)=a/y, et de la course à la publication. Rien d'autre. Il me semblait avoir fait tout mon possible pour que ce soit bien explicite. Désolé si ce n'est toujours pas clair. L'expression écrite n'est pas un art maîtrisée par tous. Mille excuses.
« IRAFURORBREVISESTANIMUMREGEQUINISIPARETIMPERAT » — Odes — Horace
[^] # Re: Première
Posté par barmic 🦦 . Évalué à 3.
Je sais depuis ma première année d'étude post bac ce qu'est est comment éviter les buffer overflow, c'est pas pour ça que c'est simple à détecter et éradiquer dans nos code.
https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll
[^] # Re: Première
Posté par Gil Cot ✔ (site web personnel, Mastodon) . Évalué à 3.
De ma compréhension, ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ s’émeut pour une erreur d’inattention et on lui fait le procès de ne pas connaitre l’auteur ou on veut faire croire que c’est hyper complexe.
Pour moi, on est typiquement dans un cas plus ou moins courant qui est normalement détecté à la relecture. Et ce que pointe le lien est que l’outil permet de gagner du temps et d’avoir de la confiance alors que traditionnellement il aurait fallu que beaucoup de paire d’yeux y passent énormément de temps. C’est assez différent du BOF
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
[^] # Re: Première
Posté par Gil Cot ✔ (site web personnel, Mastodon) . Évalué à 3.
Pour répondre à ton interrogation initiale, « l'erreur soulevée par l'outil de preuve » n’est pas vraiment une erreur dans l’absolu (du moins n’est pas perçu comme une erreur par les relectures parce-que cela semble aller de soi pour les humains dans le domaine) mais plutôt une ambigüité (pour l’ordinateur qui n’aime pas ça car étant juste basiquement manichéen.) Il y a donc une reformulation à faire pour que les outils ne partent pas dans des directions fausses (et se retrouve dans une impasse qu’elle ne comprend pas.)
Donc, plutôt qu’une bourde de calcul, c’est plus de la subtilité de formulation des conditions qui bornent la démonstration. Du coup, la prépublication était et reste de qualité, mais devient doublement carré on va dire. Accessoirement, cela répond un peu à ta crainte : l’auteur fait du raffinement au lieu de passer à autre chose pour faire du quantitatif.
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
# Et l'informatique aussi
Posté par Pol' uX (site web personnel) . Évalué à 4.
On peut aussi déboguer l'informagique. Cf les excellents cours de Xavier Leroy.
https://www.college-de-france.fr/fr/agenda/cours/semantiques-mecanisees-quand-la-machine-raisonne-sur-ses-langages
https://www.college-de-france.fr/fr/agenda/seminaire/logiques-de-programmes-quand-la-machine-raisonne-sur-ses-logiciels
Adhérer à l'April, ça vous tente ?
[^] # Re: Et l'informatique aussi
Posté par Thomas Douillard . Évalué à 3.
Tout à fait d’ailleurs les domaines sont liés :
La preuve de programme sert à montrer qu’un programme est correct vis-à-vis de ce qu’on veut lui faire faire. Pour ça on fait des maths sur un langage avec ses types et ses termes et structures de contrôle.
La preuve tout court sert à montrer qu’un raisonnement est correct pour démontrer une propriété. Pour ça dans les assistant de preuve on utilise des … types pour coder les propriétés en question. Cf. La leçon inaugurale de Xavier Leroy par exemple, mais il y a d’autres ressources. Et on écrit la preuve comme on écrirait un programme mais avec une logique un peu différente. Et une fois qu’on a fait ça dans certain cas on peut … compiler la preuve pour avoir un programme exécutable et correct : https://coq.inria.fr/refman/addendum/extraction.html
[^] # Re: Et l'informatique aussi
Posté par Gil Cot ✔ (site web personnel, Mastodon) . Évalué à 3.
Pas que déboguer, mais (mieux) spécifier&implémenter… (souvenirs de Z et B)
“It is seldom that liberty of any kind is lost all at once.” ― David Hume
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.