> fond-math > théories-des-types > l-axiome-d-univalence-science4all

L'axiome d'univalence | Infini 25

Science4All - 2017-02-20

L'axiome d'univalence est un axiome moderne introduit par Vladimir Voevodsky. De façon intrigante, il permet d'effectuer des calculs d'homotopie sur des structures pourtant très discrètes.

L'infini et les fondations mathématiques | Playlist Science4All
https://www.youtube.com/playlist?list=PLtzmb84AoqRRgqV5DfE_ykuGQK-vCJ_0t

Homotopy Type Theory on Science4All
http://www.science4all.org/article/type-theory/
http://www.science4all.org/article/homotopy-type-theory/
http://www.science4all.org/article/univalence/

The Homotopy Type Theory Book
https://homotopytypetheory.org/2013/06/20/the-hott-book/

Computer Science ∩ Mathematics (Type Theory) | Computerphile 
https://www.youtube.com/watch?v=qT8NyyRgLDQ

Univalent Foundations of Mathematics | Vladimir Voevodsky
https://www.youtube.com/watch?v=9f4pS9s-X2A

Théorie des types dépendants et axiome d'univalence | Thierry Coquand (Séminaire Bourbaki)
https://www.youtube.com/watch?v=T_WcQpj-2to

Univalent foundations subsume classical mathematics | Andrej Bauer
http://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

Maxime Euzière - 2017-03-23

dur à intuiter, mais facile à retweeter

RATATOUILLE DU BLED - 2017-02-20

J'essaye de comprendre tes episodes hein, mais là je suis perdu x)

Anissa Mohib - 2017-02-20

RATATOUILLE DU BLED pareil

Dylan Vellut - 2017-02-20

je pensais que c'était des maths, mais les chiffres me manquent...

Mary Crowley - 2017-03-03

Haha j'ai longtemps hésité a poster ce commentaire mais bon, vu que je ne suis pas la seule a suivre ses vidéos et n'avoir absolument rien compris a celle ci ^^....

C'est moi ou il nous parle en chinois ?

Désolé >.>

Nevergreenapati - 2017-02-20

309ème, mort de lol !


Plus sérieusement, tu fais vraiment du bon boulot ;D

Quentin W - 2017-02-20

Tous sa me rappelle beaucoup le principe des spécifications algébrique en informatique

Aurelien Perdriaud - 2017-02-22

Euh... Attendez... Mais qu'est-ce qui m'a pris de voter l'infini ?

Christophe M - 2017-02-21

11:14 "Jeu de construction sur un ordinateur..."
+Science4All (français) Tu connais le film "Théorème 0" ?
https://fr.wikipedia.org/wiki/Zero_Theorem

Secifelam - 2017-02-20

Merci pour toutes les vidéos que j'ai appréciées, mais je vais maintenant te laisser et je te souhaite plein de réussites. Au revoir Lê.

Johan Maïbeche - 2017-02-23

π1( S1) = Z ?

C’est chaud là …

leschatsfontdix - 2017-02-20

Merci, <3

Hady Dia - 2017-02-20

tout le monde fustige Eddy Malou mais lui aussi ... xD

misnik1986 - 2017-02-21

s'il vous plait, soyez un peu clair essayez de faire beaucoup de dessin et de geometrie car c totalement incomprehensible

Kaggan67500 - 2017-02-21

Ce coup ci, je laisse tomber l'épisode hardcore car j'en suis encore à comprendre certains épisode de cette série. A+!

Redswap - 2017-04-05

Est-ce que tu feras une vidéo sur la définition de ce qu'est l'aléatoire ? Ça m'intéresserait...

Cyril Pujol - 2017-02-20

Exellente vidéo! J'adore tes épisodes, car je trouve que même quand il y a des choses que l'on ne comprend pas exactement directement (/pas) c'est extrêmement intéressant d'essayer de voir les liens entre les objets même quand il nous manque une étape , ou d'essayer de comprendre à quoi correspond un mot de vocabulaire.C est hyper stimulant et je suis sur que ça entraîne à mieux comprendre des explications en général.
Tu es une des seules chaînes (voir la seule) que je connaisse qui traite d'un niveau aussi élevé, et c'est agréable de vraiment apprendre des choses complètement différentes et vraiment en détail.
Bref tu es le meilleur

Valentin Dropp - 2017-02-21

Des que tu as prononcé "ascenseur", je l'ai attendu et tu l'as dit : "monter vers le haut" ..! Magnifique haha !

Sandros - 2017-02-20

J'apprend coq à l'école mais pas dans ce sens là :o

Pierre-Yves Strub - 2017-02-21

C'est un peu dommage de réduire la théorie des types à l'axiome d'univalence...

Arthur Belleville - 2017-02-20

Second

bbbbbbbouli - 2017-02-21

Coq qui a été développé par l'INRIA si je me trompe ?

demonceau karl demonceau - 2018-03-12

bonjour a toi je cherchais axiume et je suis tomber sur toi , j'ai éccouter la vid jsqu au bout ça me fais pense a la matière noir le point

Fumeal - 2017-02-20

Énorme travail et très bonne vidéo comme d'habitude !! Par contre j'ai rien compris et je sens que l'épisode hardcore va etre dur... (ça fait beaucoup trop de sous-entendu sexuel tout ça...)

Ainex - 2017-02-21

Je trouve ça paradoxal de prétendre qu'une vidéo est très bonne sans n'y avoir rien compris.

Luc Zorrilla - 2017-02-21

Je trouve ça paradoxal de n'avoir rien compris du tout

Mathis Lefebvre - 2017-02-20

Même avec beaucoup de bonne volonté ça devient compliquer à comprendre là :/ Mais ça reste une super vidéo comme d'habitude :)

Samuel Vidal - 2018-08-11

La seule chose que je regrette c'est de ne pas pouvoir laisser plus d'un like. Je surkiff Bisous !

Ouranos / Activit-E - 2017-02-20

Lol

Le Dixième Docteur - 2017-07-28

Les entiers relatifs, c'est ce que l'on trouve sur ses relevés de compte ! Voilà une application des maths : la finance ! Blythe Masters, ancienne haut cadre de JP Morgan Chase, est à la base une mathématicienne formée à Cambridge.

Ouranos / Activit-E - 2017-02-20

Quatrième

Arthur Blaser - 2017-03-07

J'ai rien compris mais c'est bien fait, on vois que ilèy a du travail derriere c'est agreable.

TC TrainConstruct - 2018-05-27

400th like

M.Evolite13 - 2017-02-23

homotopie toi même.

Megadrifter2 - 2017-06-20

Je découvre la chaîne et la série Infini. Ton discours sur les courbes de Peano et de Hilbert était très intéressant. Mais que penses-tu de la courbe de Lebesgue ?

Jean sartre - 2017-02-20

cinquième

LordKAY /-\\/\/ - 2017-02-20

J'ai 15 ans je te suis mais je ne te suis en rien dans tes vidéos c'est vraiment au dessus de mes capacités pour l'instant mais à chaque épisode au moins j'essaye de comprendre :)

Antoine du Fresne - 2018-09-27

LordKAY /-\\/\/ pareil maintenant j’ai 16 ans

Alexis Blandin - 2017-02-20

Ah, ce cliffhanger...hâte de voir la suite!!!
Google se met à faire des ordinateurs quantiques, je sais pas si ça compte comme une machine de Turing, mais en tout cas ça fait un argument en plus pour la théorie de Church-Turing...

D'ailleurs, est-ce que la théorie des types est compatible avec l'algorithmique quantique?

Lionel GUEZ - 2017-02-21

rien compris mais passionnant

txia77 - 2017-02-23

J'ai découvert S4A grâce aux magies des maths de prépa... Même si je comprends pas toutes les épisodes, même parfois beaucoup je l'avoue, mais à chaque fois j'ai l'impression de voir l'envers du décors et surtout d'entre-apercevoir cette sensation d'intuition des maths (qui malheureusement fait défaut lors de nos cours de maths)... c'est ça que j'aime..

Le Roux Stéphane - 2017-03-03

Bonjour,

je viens de comprendre un truc sur le cercle \o/.

En fait, en voyant la description du cercle S1, j'avais l'impression qu'il n'avait qu'un unique point : sa base. Et bien non. Enfin si, mais non.

Bref, on peut montrer la propriété suivante sur S1 :
non-(pour tout x de S1, base = x)
(ne pouvant pas faire des caractères spéciaux ici, je mets des "pour tout" plutôt que des produits, des "il existe" plutôt que des sommes, etc, enfin je pense que vous savez traduire ça en une propriété de la théorie d'homotopie des types).

En fait c'est une application du lemme 3.3.4 : "toute simple proposition est un ensemble". Or donc, (pour tout x de S1, base = x), c'est essentiellement isProp(S1) ; et isSet(S1) vaut (pour tous x et y de S1, pour toutes preuves p et q de x = y, (p =q)). Or ce dernier est faux, puisque contredit par Refl(base) et Loop dans (base = base).

Si l'on veut être plus exact en restant dans la théorie, nous avons une fonction allant de (pour tout x de S1, base = x) dans isProp(S1) (étant donné x, y de S1, mon hypothèse me donne des preuves de (base = x) et de (base = y) que je peux combiner en une preuve de (x=y) ), une fonction de isProp(S1) dans isSet(S1) donnée par le lemme, une fonction de isSet(S1) dans (Loop = refl(Base)) (il s'agit de l'opérateur appliquant un habitant de isSet(S1) à (base, base, Loop, Refl(base)), et enfin une fonction de (Loop = Refl(base)) dans 0 (c'est l'hypothèse que Loop est non-trivial), composer le tout me donne une fonction de (pour tout x de S1, base = x) dans 0, soit ce que j'affirmais au-dessus. \o\ |o| /o/

Ici j'ai l'impression que l'on touche du doigt l'étrangeté des maths intuitionnistes.

En fait, en logique classique, j'en déduirais qu'il existe existe un x dans S1 qui est différent de base. Sauf que je ne peux pas le faire en théorie des types, faute de me donner les moyen de construire un autre habitant de S1. J'ai vraiment l'impression qu'il existe d'autres points que ma base, mais il ne s'agit que d'un mirage et je ne peux saisir aucun de ces points. Je peux faire le tour du cercle (en utilisant Loop) et constater que je ne me suis pas contenté de rester au même endroit, sauf qu'il n'y a jamais eu d'autres endroits à parcourir pour en faire le tour. C'est extrêmement déroutant. Je suppose que c'est l'analogue de ce que vous disiez du R dans la vidéo précédente, qu'il est tellement continu qu'on ne peut pas le couper en deux pour séparer ce qui est plus grand de zéro de ce qui est plus petit.

Ceci étant, j'en suis encore à essayer de comprendre réellement le lemme 3.3.4, à essayer de voir si je peux montrer ma propriété uniquement via des outils plus bas niveau que ce lemme, et surtout à essayer de me convaincre que je ne peux pas envoyer S1 dans 0. Bref, je commence à comprendre deux trois trucs qui sont sans doute élémentaires (je suis sûr que ça fait sourire tous les gens connaissant le domaine de voir que je suis fier de montrer une propriété aussi élémentaire sur S1), mais j'ai vraiment l'impression de rien panner.

Entre autre, le lemme 3.3.4 est vraiment bizarre lorsqu'on le traduit en théorie de l'homotopie "classique" : "tout espace connexe (par arc) est simplement connexe" (le "par arc" me semble redondant, puisqu'en homotopie des types il n'y a aucune notion qui ne soit pas issue des chemins : évidemment que lorsque l'on traduit en homotopie "classique", parler d'une propriété P signifie toujours "P par arc"). J'ai l'impression que c'est la path induction qui donne tellement de possibilités de constructions de chemins, qu'il n'est plus possible d'envisager un espace connexe troué (...S1 se plaçant dans une catégorie bizarre où l'on sait montrer la non-connexité, mais on ne peut extraire qu'une composante connexe), mais visiblement l'univalence joue aussi un rôle dans la démonstration du lemme. Et surtout, en homotopie "classique", S1 n'est pas connexe OK, mais si je veux étudier les propriétés des chemins de base vers base, je me restreins à sa composante connexe ; visiblement en homotopie des types, ça ne marche absolument pas (ce qui ressemble le plus à la composante connexe de (base) : S1, c'est (somme pour x dans S1 des (base = x)) - un habitant de cet espace est un habitant de S1 muni d'un chemin de base vers x - , mais en passant de S1 à cet espace, Loop collapse sur la reflexion - le chapitre sur la path induction mentionne que l'on a dans cet espace une preuve de (base, Refl(base)) = (base, Loop) ; en somme, contrairement à l'homotopie classique, extraire une composante connexe en détruit les propriétés - ou plutôt, on ne sait pas isoler une composante connexe du reste de l'espace, si bien que la méthode pour tenter de le faire est tellement approximative qu'elle en détruit les propriétés).

J'espère ne pas avoir écrit trop de conneries et vous félicite à nouveau pour votre excellent travail de vulgarisation (j'aurais absolument rien panné du livre sans vos explications initiales, même si j'en avais connu l'existence). :)

En passant, je sais que beaucoup de gens se plaignent que vos vidéos sont trop compliquées ; et je sais qu'il faut que vous gardiez le contact avec votre public, ce qui ne sera possible que si vous continuez à faire aussi des vidéos plus accessibles. Dites-vous cependant que le fait de faire des vidéos de vulgarisation mais malgré tout de haut niveau, c'est ce qui vous distingue du reste, en somme ce qui donne une utilité à votre chaîne : des chaînes vulgarisant mais sans aller trop haut niveau, on en trouve déjà plein. Vous êtes en droit de me répondre "M. Le Roux, votre avis là-dessus aurait plus de valeur si les gens comme vous très intéressés par une chaîne comme la mienne la finançait" (il faut absolument que je le fasse).

Mathieu Montin - 2017-02-21

Salut Lê. Merci pour ces épisodes sur l'infini qui permettent d'introduire la théorie des types. A la fin de cet épisode, tu présentes l'outil coq et son interface (coqide) pas très élaborée. il existe aussi proofgeneral (au sein d'Emacs) qui permet de faire du coq un peu plus intuitivement. Et comme outil tu devrais jeter un oeil à Agda ! Il est basé sur la même théorie des types mais propose de créer ses lambda-termes à la main, à l'aide d'un mode emacs qui guide la preuve / le développement. Cela pourrait t'intéresser, d'autant plus qu'Agda supporte l'unicode et les notations infixes ce qui donne aux programmes Agda un aspect beaucoup plus mathématique visuellement que coq.

Guillaume le cam - 2017-02-20

putain ça m'énerve ça fait 5 épisodes que je regarde toujours ces vidéos mais j'ai beau m'efforcer je ne comprends vraiment rien je crois que je devrais aller voir d'autres chaine

Sylvain Poirier - 2017-02-22

Qu'y a-t-il donc de si extraordinaire dans les fondations univalentes : qu'il existe un plongement strict (non-isomorphique) de l'univers des mathématiques "classiques" dans l'univers des mathématiques univalentes ? Cela n'empêche nullement qu'il existe par ailleurs un autre plongement, de l'univers des maths univalentes dans l'univers des maths classiques, dans la mesure où les maths univalentes sont algorithmiques et que le concept d'algorithme est définissable en "maths classique". La seule "grande nouvelle" est qu'un tel second plongement ne saurait être l'exact inverse du premier. Bon et après ?
Avoir une théorie dans laquelle toutes les fonctions sont continues ? En maths classique on a néanmoins le droit de ne s'intéresser qu'aux ensembles des fonctions continues. Il y a même encore mieux: pour les gens qui ne se sentiraient pas confortables avec les fonctions continues dont la convergence serait plus lente que 10^10^....10^10/log(log(log.... log(1/x)...))) (avec n logs et n dix) pour un quelconque n, les maths classiques nous laissent même le droit de définir l'ensemble des fonctions continues qui ne sont sujettes à une telle lenteur de convergence en aucun point, et de ne travailler qu'avec cette ensemble si ça nous chante !!!
A part ça, ce que pour l'instant je retiens de cette histoire, donc, comme avantage principal des maths univalentes sur les maths classiques c'est son explication de comment gagner des concours de programmation des calculs du plus grand nombre possible de groupes d'homotopie.
Cependant, aussi beau que cela soit, j'ai du mal à voir à quoi d'autre ça pourrait servir. Sans avoir étudié précisément l'interaction electrofaible, je conçois que la brisure de l'interaction électrofaible en électromagnétisme+ interaction faible puisse fair appel à un ou deux groupes d'homotopie ; de même pour l'interaction forte. Je suis même prêt à envisager que la théorie des supercordes, dont le rapport avec la physique reste totalement spéculatif, utilise des groupes d'homotopie en pagaille. Néanmoins je reste perplexe: quel rapport sérieux tout cela peut-il avoir avec la question du... fondement des maths, à savoir, éventuellement plus précisément, la question de comment serait-il mieux de démarrer les maths en première année universitaire (libre à chacun de refuser de s'intéresser à cet aspect particulier de la question générale des fondements) ?
En effet j'ai une philosophie suivant laquelle les ordinateurs devraient être au service des humains et non l'inverse, de sorte que la question de savoir quelle est la plus puissante façon de programmer les ordis ne devrait pas asservir notre cerveau. Du moins pas trop souvent...
Cependant il y a bien des choses intéressantes à chercher du côté de la logique en rapport avec le réel, précisément la physique, mais autrement : voir plus de commentaires dans ma page http://settheory.net/intro

Antoine du Fresne - 2018-09-27

J ai 16 ans et j’ai absolument tout compris jusqu’a 5:20. Pourtant j’aimerais bien tout comprendre mais j’ai bien peur que je n’ai pas toutes les notions. Petite question : l’ecole polytechnique fédérale de Lausanne propose des cours de mathématiques a raisonnements par l’absurde et des démonstrations avec les axiomes d’ensemble?

antoine - 2017-02-22

Quel est le lien avec le nom de la série : Infini ? J'ai l'impression qu'il y en a un, mais il est super abstrait. Quelque chose comme, le fait que finalement l'infini pose des problèmes, et la théorie des types ne laisse pas de place à des notions comme l'infini ?

Dylan - 2017-02-20

de la même manière une droite peut représenter un cercle, sa se tiens pas...
et la boucle base->base n'a pas lieu car ya pa la même direction

Amine boujida - 2017-03-04

Je pense toujours au fait que le sol accelere vers le haut si on suppose que ceci est vrai je tire une balle direct en haut par une kalach et donc la balle a la vitesse initiale communiqué par le kalach + la vitesse que lui communique l'acceleration de la terre apres le moment du tire on la nomme v0 selon votre hypothèse après que la balle retombe par terre c'est le sol qui y est monté et donc le sol dépasse la vitesse v0 (ce qui est normal puisqu il est en acceleration constante) + la vitesse initiale de la balle qui est de 750m/s soit 2 700 km/h , la distance terre lune de 358350 si on suppose que la vitesse de la terre est de 2700 km/h elle doit donc rencontrer la lune dans presk 135 heure (si on suppose que le temps s ecoule de la meme façon tout le long de la distance terre lune) et touut ça si on neglige le faut que la lune accelere aussi
J'ai une grande confiance en einstein et je sais que oubien quelque chose va pas avec mon raisonnement oubien toi tu n'a pas su expliquer ce qu'einstein dit voudrais tu m'aider donc a comprendre ce qui s passe exactement et merci.

chkone007 - 2017-02-20

#PlatonicienFTW
Pour info Gerard Berry a fait plusieurs colloque au Collège de France sur les preuves de programme, le lambda calcul, le pi calcule etc:
https://www.college-de-france.fr/site/gerard-berry/_course.htm
D'ailleurs le 1er truc qu'on fait pour des preuves de code/algo c'est de le transformer en langage fonctionnel (pour être Lambda pure) et là il y a plein de théorème (constructiviste :( ) applicable.

Sylvain Poirier - 2017-02-21

Sur l'indéterminisme quantique : la réponse par la théorie bohmienne pose beaucoup de problèmes, dont notamment le fait que... elle commet un gros hors sujet vis-à-vis de ses propres prétentions, son exploit effectif consistant bien moins à réussir à se conformer aux critères du déterminisme, qu'à noyer le poisson en redéfinissant le label "déterministe" pour le vider de l'essentiel de sa signification logique en sorte de pouvoir étiqueter par ce vernis une théorie dont la différence avec la MQ standard n'est pas vraiment claire (puisqu'elle donne les mêmes prédictions !), de sorte qu'il n'est pas clair en quoi elle serait effectivement "déterministe" en particulier. Voir mon argumentaire détaillé en anglais : settheory.net/Bohm (J'avais déjà répondu sur la théorie bohmienne en réponse à Damien Aubert en commentaire de https://www.youtube.com/watch?v=Rj3jTw2DxXQ )
Sur la modélisation par les processus de Markov : effectivement il semble que les prédictions de la MQ soient traduisibles en cela, cependant, à part le fait qu'aucune loi physique ne vient préciser les circonstances suivant lesquelles les tirages aléatoires doivent être insérés (à savoir la décohérence, notion émergente), une telle traduction se présente en pratique comme "pas naturelle", les mesures de complexité de part et d'autre n'étant nullement compatibles. Notamment, comment qualifier d'algorithmique un processus de Markov dont chaque étape se fait suivant une certaine probabilité dont on peut donner une valeur approximive par un calcul fini mais dont la valeur exacte nécessiterait un temps de calcul infini ? j'ai raconté cela plus longuement dans mon texte http://settheory.net/fr/dualisme-esprit-math

Sébastien Desbordes - 2017-02-21

MDR pour les boucles j'ai crée un objet mathématique que j'ai nommé pour le moment "chemin perdu" ou "chemin-polygone-étoile" où les boucles on leur importance et non pas la même signification qu'un aller-retour ou rien faire. :

Sébastien Desbordes - 2017-02-21

Je m'étais d'abord concentré sur le trajet d'un mobile autour d'un polygone si à chaque sommet il avait le droit d'avancer ou reculer.
Mais il ne fallait pas qu'il reste bloqué à faire un aller-retour d'un sommet à un autre indéfiniment.
j'ai donc chercher à établir des règles. j'ai tester mes règles sur plusieurs polygone mais cela devenais compliquer (à partir du pentagone) et j'ai chercher à changer de point de vue.
Je suis dont passer de polygone à une droite segmenté et vue que certaine règle n'allais pas et que ma conjecture était fausse.
Je me suis poser des questions sur la droite à 2 segment (ou un un segment en 2 parties / coupé en 2) et je suis arrivé sur l'étoile, devais-je rajouter une flèche ? j'avais testé les 2 hypothèses et cela m’amenai sur quelque paradoxe / incohérence mais fini par faire le liens entre polygones et étoiles.
Maintenant que j'ai 3 représentation je dois me décider sur quel règles appliquer au cheminement de mon mobile pour avoir des trajet intéressant à étudier.

Sébastien Desbordes - 2017-02-21

Ce qui suit sont ldes photos de mes feuilles que j'ai poster à mon père sur FB, (S'ils sont de mauvaise qualités, illisibles, trop brouillon, je les reprendrais, re-rédigerais) :

http://www.noelshack.com/2017-08-1487634990-chemin-perdu.jpg
(1ere feuille, avec une conjecture sur la marge qui est sans doute fausse)

http://www.noelshack.com/2017-08-1487635229-segment-et-decouverte-polygone.jpg
(autre représentation qui m'a permis d’avancer)

Sébastien Desbordes - 2017-02-21

http://www.noelshack.com/2017-08-1487635400-conjecture-fleche-oui-ou-non.jpg
(une question qui ma permis de trouver une 3eme représentation)

http://www.noelshack.com/2017-08-1487635060-chemin-vers-polygone-vers-etoiles.jpg
(la synthèse des 3 représentations, le lien entre les 3 représentation)

Sébastien Desbordes - 2017-02-21

http://www.noelshack.com/2017-08-1487635038-contre-sens.jpg
(des contre sens, configuration plus ardue à comprendre)

http://www.noelshack.com/2017-08-1487635193-pb.jpg
(un problème, questionnement)

http://www.noelshack.com/2017-08-1487635199-pb-resolu.jpg
(le problème en parties résolue)


Ainsi la Boucles = Cercles de ta vidéo pourrais être le segment à 0 parties ( ou la droite à 0 segment)
Moins

Augustin Francotte - 2017-02-21

Super vidéo ! Question par rapport au caractère aléatoire de la physique quantique, est ce qu'il n'a pas été démontré de manière rigoureuse qu'il n'existe pas de variables cachées explicatives: la violation des inégalités de Bell par l'expérience de Aspect ?

VRB Blazy - 2017-02-22

@Sylvain Poirier Oui en effet merci d'avoir précisé qu'il s'agit de problèmes de compatibilité avec la Relativité Générale, et j'avoue que ce n'était pas complètement clair dans mon esprit. Mais si la compatibilité est totale entre Théorie Quantique des Champs et Relativité Restreinte, alors comment s'y expliquent les "instantanéités" de la première (celle des échanges d'information lors des phénomènes d'intrication, de réduction du paquet d'ondes...) alors même que la notion même d'instantanéité n'a tout bonnement pas de sens en Relativité, même Restreinte?? (C'était si je ne m'abuse ta première interrogation, et elle n'est toujours pas levée @Francotte Augustin​)

Et si je comprends bien ton second paragraphe, les théories à variables cachées globales ne tiennent pas encore la route, puisqu'elles permettent d'interpréter la M.Q. seule mais pas la T.Q.C.?

Sylvain Poirier - 2017-02-22

L'explication est, en quelque sorte, le fait qu'il n'est pas rigoureusement clair que ces "instantanéités" soient réellement des instantanéités. Echanges d'information ? Quels échanges d'information ? En fait il s'agit là d'échanges d'informations ayant une propriété renversante, fantastique, incroyable, hallucinante... mais qu'est-ce donc qu'un échange d'information peut avoir de si fantastique ? Eh bien, ce qu'il y a de si fantastique dans cet échange d'information, c'est.... son incapacité fondamentale et absolue à transmettre la moindre information !!!! de sorte que la question de savoir si un tel échange aurait réellement lieu ou non, et si oui, quand et comment, reste... une question fondamentalement indécidable. En effet, il faut se renseigner sur le caractère PARADOXAL de toute cette histoire, et la façon dont ce caractère paradoxal emmerde un grand nombre de gens qui du coup n'ont jamais pu trouver comment raconter ni encore moins "expliquer" les choses de façon claire et cohérente, alors même que les prédictions effectives et leur structure mathématique sont parfaitement sans ambiguité. Vous trouvez qu'il y a des trucs bizarre dans cette histoire ? Mais bien sûr, tous les grands esprits l'ont déjà remarqué, donc bienvenue au club ! Notamment l'interprétation en mondes multiples est parfaitement invariante relativiste, puisqu'elle ne comporte aucune réduction du paquet d'ondes, donc aucune transmission de quoi que ce soit à une quelconque vitesse lors de cette réduction qui n'a jamais lieu.
Oui je n'ai pas suivi en détail les tentatives des théories à variables cachées de se réconcilier avec la TQC, seulement que c'est un problème très difficile. A mon avis il est tellement plus simple de renoncer complètement aux variables cachées au lieu de chercher obstinément de tels rafistolages...

VRB Blazy - 2017-02-24

@Sylvain Poirier Ah bon d'accord... Oui je suis au courant que l'on ne pourrait se servir de ces mécanismes quantiques pour transmettre de l'information, mais je parlais de l'information intrinsèque au phénomène:
-pour l'intrication, information de la mesure de l'état de l'un des deux quantons qui se transmet en apparence instantanément au second quanton intriqué qui est projeté dans le même état;
-et pour la réduction du paquet d'onde en général, je vais prendre un exemple: la vision d'une étoile à 10al de la Terre réduit instantanément la fonction d'onde qui emplissait toute la boule (ou au moins la sphère) de rayon 10al centrée en l'étoile pour la concentrer toute entière dans l'œil de l'observateur; d'où une information transmise en apparence instantanément à 20al de distance.
Mais je suis me semble-t-il d'accord sur l'indécidabilité de la question...
Quant à l'interprétation par mondes multiples, elle règle en effet la question de compatibilité, mais tu affirmais qu'elle avait été réglée au niveau des théories elles-mêmes dans la T.Q.C. ... Donc est-ce que ton propos signifie que la Théorie des Mondes Multiples est l'une des interprétations possibles de la T.Q.C., au contraire de l'interprétation probabiliste de Copenhague classique, qui faute de ces questions d'instantanéité n'est plus cohérente?
Pour finir, je suis d'accord qu'il semble un peu artificiel de chercher à préserver les variables cachées face à tant de difficultés, surtout si le déterminisme peut être conservé via d'autres interprétations, comme celle des Mondes Multiples...

Sylvain Poirier - 2017-02-24

Il y a des contresens à eviter: la physique quantique est en fait non pas une théorie mais, en quelque sorte, 2 théories très différentes l'une de l'autre. L'une est la théorie de l'évolution d'un état quantique par une transformation unitaire de l'espace de Hilbert. L'autre est la théorie de ce qui peut se passer lors d'une mesure : définir une liste de possiblités (base de l'espace de Hilbert, ou liste de sous-espaces 2 à 2 orthogonaux; définir les probabliités de chaque possibilité ; définir l'état après mesure, étant donné son résultat. Or la TQC ne fait que fournir un concept invariant relativiste de la 1ère théorie, ignorant totalement la deuxième. Donc il ne "résoud le problème" que sous l'hypothèse que seule le premier type d'évolution a lieu, non le deuxième. Autrement dit : à condition d'avoir accepté l'interprétation en mondes multiples ! Ainsi, du point de vue du formalisme mathématique de la TQC, la théorie des mondes multiples apparait comme la plus naturelle, celle par défaut, il apparait très difficile de s'en débarrasser. Personnellement je n'adhère pas aux mondes multiples mais à l'interprétation de Wigner, pour cela je considère que la réduction du paquet d'ondes peut déroger à l'invariance relativiste de par sa nature non-physique.

"si le déterminisme peut être conservé via d'autres interprétations, comme celle des Mondes Multiples"
- Les Mondes Multiples ne "conservent" le déterminisme que sous une forme tellement redéfinie qu'il en est assez méconnaissable (on peut en dire autant des variables cachées....)
- Vouloir conserver le déterminisme, pour quoi faire ? je me porte bien à le rejeter.

VRB Blazy - 2017-02-24

@Sylvain Poirier​
Je n'avais jamais entendu parler d'une telle distinction, la première théorie ne modélise-t-elle pas l'état quantique par une fonction d'onde, celle-là même dont le carré du module est une densité (par rapport à la mesure de Lebesgue tridimensionnelle) des probabilités que tu classes dans la seconde théorie!?
Ceci dit en admettant cette hypothèse, je comprends la suite... Je ne me souviens plus si je connaissais l'interprétation de Wigner, mais en quoi postuler que ce soit la conscience qui réduise les paquets d'ondes fait considérer ce phénomène comme non physique?

-Ah bon, si méconnaissable que ça? C'est vrai qu'il y a toujours du hasard quantique fondamental mais il crée aussitôt une multiplicité d'Univers parallèles parfaitement déterministes (si je ne m'abuse)...
-Ah ben, quand même, le déterminisme semble le fondement de la logique, ce serait... Logique ou du moins sympa de le préserver autant que possible, demande à Bébert Einstein :P

MJAjani - 2017-02-20

prépa physique chimie... ah je croyais qu'on balançais les classes dans laquelle on est !