Discussion:Théorème de Feit-Thompson

Lien rouge du modèle Traduction

Je ne sais pas pourquoi, le modèle Traduction, que j'ai placé sur l'article pour dire qu'il est tiré de l'article correspondant de la Wikipedia anglaise, pointe vers la page de discussion de l'article français. Pour éviter que ce lien ne soit rouge, je crée la page de discussion.
Marvoir (d) 29 novembre 2009 à 20:10 (CET)

Vérification dans Coq

Je viens d'enlever une mention selon laquelle le théorème a été "formalisé" dans Coq. En effet, il me semble que c'est peut-être intéressant quant à Coq, mais que cela ne nous apprend rien sur le théorème. Ceci dit, s'il y a des contributeurs qui ne sont pas d'accord avec le retrait, je ne m'obstinerai pas. Marvoir (d) 23 septembre 2012 à 20:43 (CEST)

J'admire Thierry mais je suis d'accord. Il serait plus utile pour tous d'insérer ça dans les articles liés à lui et Coq. Anne (d) 23 septembre 2012 à 21:05 (CEST)

Thierry n'a rien à voir là-dedans. Le fait que la preuve ait été vérifiée par ordinateur (que ce soit avec Coq ou un autre logiciel), est important à mes yeux. Surtout étant donné que ladite preuve est accessible à peu de personnes, beaucoup moins que le fonctionnement d'un système logique formel. La vérification par ordinateur est mentionnée pour la conjecture de Kepler, le théorème des quatre couleurs, et pour la page anglaise de Feit-Thompson. Sgnb (d) 26 septembre 2012 à 16:09 (CEST)

J'ai dit et je répète que je ne m'obstinerai pas si quelqu'un rétablit l'information, mais dire dans l'article sur le théorème de Feit et Thompson qu'il a été confirmé par un logiciel de vérification me semble avoir l'air naïf : personne, à ma connaissance, n'aspirait à ce que la démonstration de ce théorème soit confirmée. Que des mathématiciens de premier plan en aient publié une démonstration un peu remaniée en deux volumes a de quoi tranquilliser sur l'exactitude du théorème. La vérification par ordinateur est donc plutôt un exploit de Coq qu'un événement concernant le théorème. Je crois savoir que la classification des groupes finis repose sur des résultats non publiés. Par hasard, Coq ne pourrait-il pas essayer de boucher ces trous-là ? Ce résultat-là mériterait d'être signalé dans l'article sur la classification. Mais je crois qu'on en est loin Marvoir (d) 27 septembre 2012 à 09:09 (CEST)

Les preuves faites par des mathématiciens (quelle que soit leur réputation) ne sont convaincantes que pour les personnes capables de les lire et de les comprendre. Ces personnes peuvent avoir les mêmes biais que les auteurs eux-mêmes pour décider de l'importance d'un détail ou d'un autre. Dans le cas de Feit-Thompson, il faut être spécialiste en théorie des groupes. Pour être convaincu par la preuve en Coq, il suffit de comprendre l'énoncé du théorème (pour lequel il n'est pas nécessaire d'être un spécialiste en théorie des groupes) et la logique formelle sous-jacente à Coq (pour laquelle il n'est pas nécessaire d'être un spécialiste de Coq). Et de faire confiance à un programme générique (Coq lui-même) qui n'a pas été conçu spécialement pour prouver ce théorème particulier, ni même quoi que ce soit sur les groupes, et donc peut être considéré comme impartial (je ne dis pas infaillible), et qui va vérifier qu'il n'y a aucun trou dans la preuve jusqu'aux axiomes de base de la logique (chose pénible qu'aucun humain ne fera). Aussi, ce n'est pas "un exploit de Coq", ni des développeurs de Coq, mais bien de ceux qui ont formalisé la preuve jusque dans ses moindres détails. C'est pas sur Coq qu'il faut se focaliser à mon avis, mais sur la vérification mécanique. En ce qui me concerne, je vais attendre que la preuve soit publiée avant de modifier l'article. Sgnb (d) 28 septembre 2012 à 15:13 (CEST)

"Feit et Thompson" ou "Feit-Thompson" ?

Il me semble qu'on trouve "Théorème de Feit et Thompson" aussi bien que "Théorème de Feit-Thompson". Quand j'ai créé l'article, j'ai choisi "Théorème de Feit et Thompson" parce que 1° la forme avec trait d'union a toujours le désavantage de ne pas exclure qu'il s'agisse d'un seul mathématicien à nom composé, comme Lejeune-Dirichlet; 2° le trait d'union pour désigner deux mathématiciens me semble devoir être réservé au cas où le second mathématicien a renforcé ou généralisé un théorème du premier, comme dans Cauchy-Schwarz, ou encore au cas exceptionnel Fermat-Wiles. Quand un théorème a été publié en collaboration par deux mathématiciens, comme c'est le cas de Feit et Thompson, "et" me semble préférable. Mais s'il y a des arguments en sens contraire, je pourrais m'incliner. Marvoir (discuter) 22 octobre 2014 à 10:41 (CEST)

Je ne milite pas pour l'un plutôt que l'autre (je suis plutôt d'accord avec toi — tiens, voici quand même un petit « argument » contre), je me demandais juste comment titrer le lien ajouté en article connexe car pour cette conjecture je ne trouve pas de réf en français. Anne

Je comprends, mais ton interrogation sur la conjecture m'a fait réfléchir sur le théorème. Pour rendre les recherches Internet plus efficaces, je vais ajouter la dénomination "Feit-Thompson". Marvoir (discuter) 23 octobre 2014 à 10:15 (CEST)

J'ai tout renommé en "Feit-Thompson". En mathématiques, on sépare les noms dans un théorème par des tirets. Au hasard: Théorème de Cauchy-Lipschitz, Théorème de Perron-Frobenius, Théorème de d'Alembert-Gauss, etc. --Valvino ^(discuter) 6 octobre 2018 à 18:35 (CEST)

EDIT: on peut aussi aller faire un tour sur Liste de théorèmes. --Valvino ^(discuter) 6 octobre 2018 à 18:38 (CEST)

Vous auriez pu en parler d'abord, Valvino. Avez-vous lu le premier alinéa de la présente section ? L'Universalis dit "Théorème de Feit & Thompson". Google trouve "le théorème de Feit et Thompson", "au théorème de Feit et Thompson" dans des textes universitaires. Marvoir (discuter) 6 octobre 2018 à 19:34 (CEST)

Valvino, puisque vous êtes resté plus de vingt-quatre heures sans répondre, j'ai défait votre passage en force et rendu à l'article la dénomination "Théorème de Feit et Thompson". Peut-être pourriez-vous rétablir cette dénomination dans tous les articles où vous l'avez modifiée ? Marvoir (discuter) 8 octobre 2018 à 10:42 (CEST)

J'ai reverté ta modification. J'ai donné des sources dans l'article qui indique que "théorème de Feit-Thompson" est utilisé. J'ajoute aussi que "Feit-Thompson" suit le principe de moindre surprise car en mathématiques, on met toujours des tirets entre les noms des gens (personne ne dit le théorème de d'Alembert et Gauss, le théorème de Fermat et Wiles ou le théorème de Green et Tao...). Pourquoi diable le théorème de Feit-Thompson serait différent ? J'ajoute également que toutes les autres langues utilisent "Feit-Thompson" et non "Feit et Thompson" et qu'à part l'encyclopédie Universalis et des articles de vulgarisation je n'ai pas trouvé beaucoup de sources qui parlent de "Feit et Thompson" (notamment d'articles de recherche). Enfin une recherche Google indique environ 712 résultats pour "théorème de Feit-Thompson" et environ 404 résultats pour "théorème de Feit et Thompson". Bref je pense qu'il est légitime de mentionner que "théorème de Feit et Thompson" existe mais ne devrait en aucun cas être le titre utilisé ici. Valvino ^(discuter) 20 octobre 2018 à 10:38 (CEST)