Théorème des quatre couleurs

[Yi Sun-sin]

Pour la force physique, c'est en général vrai, bien qu'il y ait des recoupements (il arrive qu'un gars soit plus faible qu'une fille, mais en général, les femmes ont trop de graisse et pas assez de muscles ).

Et dans le cas contraire, ça peut faire bizarre :


Un culturiste, ça fait déjà assez monstrueux, alors une culturiste…

(*) Une exception quant aux maths expérimentales. Un exemple d'expériences mathématiques est donné dans le cas du théorème des quatre couleurs qui n'a pu être démontré que via une simulation sur ordinateur.

Si je puis me permettre, puisque ça touche à mon domaine (les graphes), la preuve a été exhibée via Coq, qui est un moyen d'automatiser les preuves, ce qui n'a pas grand chose à voir avec une simulation. Pour expliquer le principe, il s'agit d'autoriser un certain nombre de règles axiomatiques le plus réduit possible, et de faire une preuve ne faisant appel qu'à ces règles axiomatiques très simple. On fourni à Coq la proposition qu'on veut prouver, on lui donne les règles à appliquer, et il renvoie le résultat de l'application de la règle si la règle est effectivement applicable à se cas précis, et sinon une erreur. Là où l'intérêt de Coq réside, pour ce genre de preuve, est qu'on peut construire des «tactiques», des choses du genre «Applique la règle 3, et ensuite, essaye d'appliquer la règle 2, si ça marche tente la règle 4, et sinon essaie la règle 1». Or, ces preuves se décomposent en milliers (voire millions) de sous-cas. Avec Coq, on peut écrire une tactique, la lancer sur tous les sous-cas, et laisser la machine vérifier elle-même pour quels cas elle marche, et conserver tout ceux sur lesquels elle ne marche pas, s'il y en a, pour te permettre d'écrire une nouvelle tactique pour les résoudre.
Voila, c'est l'idée générale, si ça t'intéresse je peux développer. Et tu peux même installer Coq pour tester toi-même, c'est un logiciel libre (et gratuit) disponible dans les dépôts de toute bonne distribution Linux, mais aussi installable sous Windows et MacOSX.

[abdelbouddha]

heu... Coq?

ça a un rapport avec Paul le poulpe?

[Yi Sun-sin]

Non. Désolé, j'ai fait un petit hors-sujet mathématique pour répondre à AliadArrakis.

[AliadArrakis]

Pour la force physique, c'est en général vrai, bien qu'il y ait des recoupements (il arrive qu'un gars soit plus faible qu'une fille, mais en général, les femmes ont trop de graisse et pas assez de muscles ).

Et dans le cas contraire, ça peut faire bizarre :

(non je ne vais pas reproduire l'image )

Un culturiste, ça fait déjà assez monstrueux, alors une culturiste…

Déjà que je n'aimais pas les culturistes masculins (je préfère une musculature plus naturelle).

Sinon, une coureuse déjà peut avoir très peu de graisse, et pas avoir la gonflexe. Ce peu de graisse peut perturber les fonctions hormonales.

(*) Une exception quant aux maths expérimentales. Un exemple d'expériences mathématiques est donné dans le cas du théorème des quatre couleurs qui n'a pu être démontré que via une simulation sur ordinateur.

Si je puis me permettre, puisque ça touche à mon domaine (les graphes), la preuve a été exhibée via Coq, qui est un moyen d'automatiser les preuves, ce qui n'a pas grand chose à voir avec une simulation. Pour expliquer le principe, il s'agit d'autoriser un certain nombre de règles axiomatiques le plus réduit possible, et de faire une preuve ne faisant appel qu'à ces règles axiomatiques très simple. On fourni à Coq la proposition qu'on veut prouver, on lui donne les règles à appliquer, et il renvoie le résultat de l'application de la règle si la règle est effectivement applicable à se cas précis, et sinon une erreur. Là où l'intérêt de Coq réside, pour ce genre de preuve, est qu'on peut construire des «tactiques», des choses du genre «Applique la règle 3, et ensuite, essaye d'appliquer la règle 2, si ça marche tente la règle 4, et sinon essaie la règle 1». Or, ces preuves se décomposent en milliers (voire millions) de sous-cas. Avec Coq, on peut écrire une tactique, la lancer sur tous les sous-cas, et laisser la machine vérifier elle-même pour quels cas elle marche, et conserver tout ceux sur lesquels elle ne marche pas, s'il y en a, pour te permettre d'écrire une nouvelle tactique pour les résoudre.
Voila, c'est l'idée générale, si ça t'intéresse je peux développer. Et tu peux même installer Coq pour tester toi-même, c'est un logiciel libre (et gratuit) disponible dans les dépôts de toute bonne distribution Linux, mais aussi installable sous Windows et MacOSX.

C'est marrant comme logiciel (je peux peut-être l'installer, mais j'ai peur pour la puissance de mon ordi, surtout que je le surcharge de pleins de trucs inutiles mais chouettes ces derniers temps), mais là, il me semble que des démonstrations, comme des démonstrations par récurrence, ne peuvent convenir pour démontrer le théorème. C'est ici de la simulation pure (d'où l'ajout "expérimental"). J'en fais aussi un peu, des simulations.

[Yi Sun-sin]

C'est marrant comme logiciel (je peux peut-être l'installer, mais j'ai peur pour la puissance de mon ordi, surtout que je le surcharge de pleins de trucs inutiles mais chouettes ces derniers temps),

Ça ne demande pas beaucoup de puissance pour marcher, je pense que tu dois pouvoir le faire marcher sur un ordinateur d'il y a dix ans sans trop de problèmes. S'il a vingt ans, par contre, n'y compte même pas .

mais là, il me semble que des démonstrations, comme des démonstrations par récurrence, ne peuvent convenir pour démontrer le théorème. C'est ici de la simulation pure (d'où l'ajout "expérimental").

Ah, je t'assure que non. Le théorème a été démontré en Coq, et Coq ne permet que des démonstrations parfaitement rigoureuses.

[abdelbouddha]

sans vouloir passer pour un rasoir le sujet ici c'est "le coran est une insulte à la femme"

(je sais pas pour votre coq, n'empêche que Paul le poulpe lui il avait prévu le résutat de la coupe du monde...)
wââââffff!

[Yi Sun-sin]

Ok, on continuera par MP.

[abdelbouddha]

mauruuru

(merci en tahitien)

[AliadArrakis]

Déplacement du hors sujet concernant le théorème des quatre couleurs trouvé dans le sujet "le coran est une insulte à la femme".

Alia l'animatrice qui espère que les modos vont bientôt revenir

[AliadArrakis]

C'est marrant comme logiciel (je peux peut-être l'installer, mais j'ai peur pour la puissance de mon ordi, surtout que je le surcharge de pleins de trucs inutiles mais chouettes ces derniers temps),

Ça ne demande pas beaucoup de puissance pour marcher, je pense que tu dois pouvoir le faire marcher sur un ordinateur d'il y a dix ans sans trop de problèmes. S'il a vingt ans, par contre, n'y compte même pas .

C'est que mon ordi est un portable. Sinon, si le logiciel marche pour un modèle de 10 ans plus vieux, alors ça marche.

mais là, il me semble que des démonstrations, comme des démonstrations par récurrence, ne peuvent convenir pour démontrer le théorème. C'est ici de la simulation pure (d'où l'ajout "expérimental").

Ah, je t'assure que non. Le théorème a été démontré en Coq, et Coq ne permet que des démonstrations parfaitement rigoureuses.

Qui fait des centaines de pages?

[Yi Sun-sin]

C'est que mon ordi est un portable.

Le mien aussi .

Qui fait des centaines de pages?

La version en Coq ? C'est de toute façon franchement pas lisible. Le code en Coq doit bien être fourni en annexe dans la preuve, mais le gros du papier doit être écrit dans de l'anglais courant .

[AliadArrakis]

Qui fait des centaines de pages?

La version en Coq ? C'est de toute façon franchement pas lisible. Le code en Coq doit bien être fourni en annexe dans la preuve, mais le gros du papier doit être écrit dans de l'anglais courant .

Si c'est de l'anglais courant, ça ira.

[Yi Sun-sin]

Bah, en disant courant, je suis peut-être allé un peu vite. Disons que la preuve fait appel à du jargon, évidemment. Et qu'elle fait appel à pleins de résultats qui renvoient vers d'autres articles. Et qu'elle est très compliquée. Et que je ne l'ai même pas lue, moi, parce que je sais que j'aurais un mal fou pour la comprendre.
Si tu arrive à la lire et à la comprendre, tu aura toute mon admiration !

[AliadArrakis]

N'étant pas mathématicienne de formation, c'est vrai que je risquerait de tomber des nues pour le jargon. (Sauf si ce jargon fait appel aux termes que j'ai appris)

[Yi Sun-sin]

Est-ce que l'expression graphe planaire (ou planar graph en anglais) ? Si ce n'est pas le cas, il te manque déjà du vocabulaire pour comprendre l'énoncé du problème formalisé .