Science4All - 2017-02-23
Cette vidéo est une brève introduction à la théorie homotopique des types. 0:25 L'univers des types 5:29 Les quantificateurs 10:52 Le tiers exclus 16:03 L'axiome du choix 19:13 L'égalité propositionnelle 25:16 Types, groupoïdes et homotopie L'infini et les fondations mathématiques | Playlist Science4All https://www.youtube.com/playlist?list=PLtzmb84AoqRRgqV5DfE_ykuGQK-vCJ_0t Homotopy Type Theory | Book https://homotopytypetheory.org/book/
hardcore ça je confirme !
je me sens trop con face à tes videos Hardcore x)
T'es pas le seul !
Se sentir con, c'est le quotidien du mathématicien...
Il n'y a pas de sommaire dans la description mdr
Bah si: "Cette vidéo est une brève introduction à la théorie homotopique des types." c'est ça le sommaire. Il y a juste une seule entrée, pas besoin de sous chapitres.
+Mourad Qqch ah merde j'ai oublié... Je peux pas la mettre right now. Ce sera là demain
Science4All (français) pas de soucis, ce sont des choses qui arrivent :-)
... est ce qu'on aura ça au contrôle?
ce n'est pas au programme, mais ça pourrait être utile au contrôle...
Science4All (français) étant étudiant de math spé, j'ai beaucoup trop entendu cette phrase...
15'26'' y au rait - il pas une petite coquille : "supposer l'AC" (au lieu de TE) ?
Je comprends tellement rien que ça me fait rigoler :) Mais c'est pas grave, il y en a d'autres vidéos ou j'ai bien compris au moins 10% :)
Je me sens tout bête, je ne comprends RIEN à tes vidéos Hardocore. Mais j'aime comme même tes vidéos.(Je ne sais pas pourquoi)
"... je ne peux pas résumé un livre de 400 pages dans une vidéo de 20 mn..." Haha mais dans une vidéo dans 30 mn ?!? ah bah non
Drôle que AC (bon une variante, certes) soit vrai en théorie des types, alors qu'en logique intuitionniste il implique le tiers exclu 😆
Type 0 évolue en silvalié
Ça me semblait important
Je ne sais pas pour les autres, mais tu m'as perdu depuis quelques vidéos déjà :p
Et pourtant, je ne suis pas le dernier dans la compréhension du tiers-exclus ^^'
J'ai vrrraiment de la peine à rentrer dans le livre o_o
La vidéo m'aide un peu mais il me manque sûrement des étapes intermédiaires ou des prérequis
p^-1 c'est le chemin inverse
lol
j'ai pas aces au sommaire :)
Produit, somme, groupoïde, foncteur... Ça me rappelle quelque chose, mais quoi ? ;)
La vidéo est quand même géniale
Il ÿ a moÿen d' être soi sans moi ; ça va faire des malheureux mais pas énormément !
Très intéressant ! Effectivement ça donne envie de commander le livre, et j'ai trouvé courageux que tu présentes tout ça sachant que ça pourrait perdre ton public.
Pour la forme cependant j'ai trouvé la vidéo pour le moins austère, entre les hésitations et l'absence de musique. Tu es si impatient que ça de passer à la prochaine série ? ^^
Les épisodes Hardcore n'ont jamais été très travaillés visuellement ^^
Mais OUI, je suis impatient de commencer la prochaine série ;)
Hé hé ! Depuis que j'ai moi-même commencé à faire des vidéos je me rends compte de la somme de travail que tu abats, donc vraiment je te souhaite bon courage !
Le Biactol et le shampoing existent ^^
C'est vachement chaud -_-
Faut que je reregarde les anciennes vidéos sur les types
il y a l'égalité relationnel et l'égalité *** ? j'ai oublier
+Seb16120 égalité definitionnelle (même construction) et égalité propositionnelle (c'est un type et prouver l'égalité revient à construire un élément du type)
D'accord ^^
j'utilise tes termes ici : https://www.ilemaths.net/sujet-10-1-2-y-1-2-740197.html#msg6456241
Dois-je cité ton nom ?
Bravo super vidéo bien expliqué
Mais je me demande quelque chose, si j'ai bien compris la théorie des types est en grande partie constructiviste. Mais en maths constructive le tiers exclu et l'axiome du choix sont rejetés. Ma question fondamentale ( pour moi), c' est de savoir si en quelque sorte la théorie des types ne serait pas le lien parfait entre mathématique classique et mathématiques constructiviste. Le lien trouvé entre physique quantique et relativité générale par analogie
D'une certaine manière, la théorie des types est plus un langage mathématique, "une façon de parler maths", qu'une fondation mathématique. À partir du langage de la théorie des types, on peut tout faire. Et on peut tout faire joliment (mais ça c'est subjectif)...
Merci pour cette réponse.
Personellement je trouve ce langage très beau et très efficace.
Hate de voir la nouvelle série, j'espère que c'est les probabilités
Génial
Salut Lê ! Super vidéo (dis-je en ayant compris un dixième).
Tu m'as donné envie d'acheter le livre mais j'ai peur d'être totalement perdu. Est-ce que tu sais quels prérequis je dois avoir avant de m'y attaquer ? Et des livres à me conseiller ?
+Axel le pdf est gratuit donc tu peux essayer de lire directement le livre. Je trouve que l'effort pédagogique du livre est génialissime, et je ne vois pas trop qu'elle lecture intermédiaire conseiller
Science4All (français) Disons que si tu admets ne pas avoir tout compris, j'ai un peu peur de m'y attaquer avec mon brevet mention assez bien. Mais vu que c'est gratuit, je vais essayer de m'y attaquer.
Bonjour,
J'ai l'impression que dire qu'on ne peut pas créer un élément de A+B sans passer par les constructeurs (inleft et inright) est impropre.
En fait, j'ai l'impression que rien n'impose dans la théorie des types que tout passe par un constructeur ; pour un contre exemple trivial, il est indiqué dans le livre qu'il n'est pas possible de construire un élément de 0 directement, mais qu'il est possible de le faire indirectement pour une théorie inconsistante ; évidemment, la construction d'un tel élément ne pourrait pas passer par un constructeur (0 n'en ayant pas).
Pour un contre-exemple moins trivial... Je dirais, à l'aide des axiomes que l'on peut ajouter genre le LEM ? Le LEM va permettre de peupler des types sans passer par leurs constructeurs : par exemple, de peupler tous les théorèmes qui ne peuvent pas se démontrer sans le LEM. Mais l'on va peupler ces théorèmes non avec leurs constructeurs propres (...As a side note, je suis pas du tout assez loin dans le livre pour savoir si un théorème a vraiment des constructeurs propres : peut-être je suis en train de dire une ineptie), mais en faisant arriver une fonction dedans (fonction qui nous est donnée par le LEM). Me trompe-je ? (c'est une vraie question, j'ai pas l'impression de comprendre assez la théorie pour pouvoir dire un truc sensé dessus)
Bref, on arrive à un truc que j'arrive pas comprendre dans le livre, et qui est sensée être élémentaire (c'est donc très frustrant) : les propriétés d'induction de A+B, AxB et autres structures "de base" sont-elle des théorèmes, issus des règles fixées au départ, ou des axiome ? J'ai l'impression que c'est le second ; entre autre, parce que pour AxB, le livre indique que l'on va montrer que AxB ne contient que des paires - or cette démonstration part de la propriété d'induction, et je ne vois absolument pas comment on pourrait montrer la propriété d'induction sans partir du principe qu'il n'y a que des paires (... En fait je ne vois pas comment on pourrait la montrer tout court, mais c'est une autre histoire). Et seconde chose, justement lorsque AxB est défini dans le livre (chapitre 1.5), le livre semble définir comment on va définir une fonction dessus ; mais définir une fonction d'un type quelconque, mettons AxB (et allant où on veut), on sait déjà le faire depuis la partie 1.2 qui défini les fonctions A->B comme des lambda-expression.
Bref, j'ai l'impression que l'on ne part même pas du principe qu'un élément de AxB (ou A+B ou n'importe quoi) devra passer par un constructeur ; plutôt, on définit des constructeurs arrivant dans AxB, on décide que la propriété d'induction a un habitant, et de là, sachant toutes les façon dont on peut mapper AxB dans un autre type, on en déduit qu'il ne contient que des paires, ie des trucs qui sont passés par le constructeur (... ce qui ne me semble pas supposé vrai pour d'autres types - on l'espère plutôt, "constructivity, if attained, will be an added bonus"). Sauf que c'est absolument pas expliqué comme ça et que j'ai pas l'impression d'avoir bien compris.
Et bref, du coup pour A+B, j'ai la même impression que l'on ne suppose pas que tout habitant est forcément issu des deux constructeurs, mais plutôt qu'on suppose la propriété d'induction, laquelle implique que tout habitant est issu d'un des deux constructeurs (ou plutôt, est égal à un habitant issu des constructeurs, et en plus on sait retrouver lequel etc...).
Sinon j'ai essayé de mettre des messages sur votre site (ça me semble plus simple qu'une vidéo youtube pour des trucs techniques que je pense pas avoir compris), mais je ne sais pas si ça marche (ou si vous n'avez juste pas le temps et je suis juste en train de vous harceler :s auquel cas je m'en excuse).
Bien à vous,
Stéphane
+Le Roux Stéphane je ne maîtrise pas assez le sujet pour te répondre. En effet, le livre n'est pas très clair sur s'il s'agit d'axiomes...
Mais du coup, il n'y a qu'une seule manière de formuler la négation en théorie des types ? Parce que dit comme ça on croirait qu'il suffirait d'exprimer une proposition absurde par sa définition, et qu'elle serait capable d'exprimer la négation, ou plutôt la fausseté
C'est bizarre...
Coucou Science4All sauf si je me trompe pas une bonne partie de tes vidéos( si ce n'est la totalité) traite de sujets compliqués et inaccessibles sans beaucoup de prérequis feras tu des vidéos sur des sujets plus simples qui peuvent être compris niveau postbac ? ou bien quelque chose avec une mini progression ? :D
+Gabriel Pizzo (dj gab) lundi on commence une nouvelle série beaucoup plus compréhensible
@Science4All (français) merci bien, continue de faire des vidéos de qualités haha ^-^
Bonjour,
J'ai quelques petites questions. J em présente, Gabriel Mattucci et cela fait quelques vidéos que je regarde de vous et que je trouve vraiment intéressant. De plus je ne suis vraiment pas ferré en Maths par contre j'aime bien les maths. Dans cette video, au niveau de la commutativité. Je me suis dit que la commutativité existe toujours entant que nous faisons référence à des nombre qui ne sont pas irrationnel. par exemple 1+2 = 2+1 par contre peux-ton prouver que 1+racine carré de 2 = racine carré de 2 étant donné que racine de 2 est irrationnel? une autre question concernant lettres exclu. Vous avez dit que s'il existe une fonction f de X vers 0, c'est absurde car O ne contient rien. Effectivement, mais peut-on dire que tout de meme cette fonction existe pour n'importe quel X car cela signifierait que X se ferait absorber par 0 et donc que 0 annihilerait tout X.Il doit bien y avoir des trous noir en Maths aussi oui? :) :) :) enfin ..... voilà mérite pour votre réponse.
C'est étonnement beaucoup plus abscon. Quelque chose ne passe pas en terme de vulgarisation.
Le fait de noter des fonctions en indiquant juste leur ensembles de départ et d'arrivée, les produits avec " : " en bas (c'est juste pour pas mettre le "appartient à" sous prétexte qu'on fait pas de la logique classique ? plus tard tu le réutilise aussi dans " f(x) : x=x", si quelqu’un comprend, je suis admiratif, parce que des égalités qui ont des types différents, c'est pas simple à suivre.), et les mots en anglais balancés sans raison ("input", le nom des fonctions left et right qui vient semer la confusion avec inputLeft et inputRight, la où des fonctions f,g,h, ça plait très bien à tout le monde (enfin j'imagine...) PS : je suis mauvaise langue : ça ne dure pas.), et de plus tu passe très vite sur ce qu'est l'univers U, alors que je pense que ça doit vraiment être fondamental à visualiser vu la suite. Bref à 5 min j'étais déjà paumé même en repassant la vidéo en vitesse normale (1.25, habituellement je suis assez bien) et pourtant je suis en MP dans un bon lycée.
Bon à 6:20 ça s'améliore. 7:33, la notation en somme est hermétique, tu décris à côté d'elle un doublet (ce qui soyons clair ne fait pas sens), et tu parle de valeur de vérité sur les types, "si on veut"... et à 8:58, j'ai bien peur que l'analogie ne soit qu'un vulgaire moyen de passer au dessus de l'échec de communication des minutes précédentes... 9:30 tout va mieux mais je m’arrête néanmoins, j'ai déjà passé trop de temps à écrire ce commentaire.
Peut-être serais-je plus récéptif une prochaine fois mais bon, pour l'heure je suis déçu.
8 mois plus tard, en me refaisant tout l’intuitionnisme à la suite, ça passe, mais les notations restent lourdes. Finalement, ça ne me convainc pas de quitter la logique classique, mais je comprends ce que tu raconte : tu viens de perdre un pouce rouge.
Franchement c'est super intéressant et tout et tu doit sûrement bien expliquer les choses (puisque j'ai l'impression d'avoir compris des trucs) mais je sais pas pourquoi j'arrive pas à comprendre :'(
J'ai quelques questions pour essayer de comprendre un peu plus du coup:
- Qu'est-ce que veulent dire ces symboles exactement : := ≡ ?
- Quand tu écrit U c'est en quelque sorte l'univers de tout les types ? c'est pas un peu platonicien du coup ?
- Si j'ai bien compris, pour démontrer une propriété P il faut créer un type P et montrer qu'il est non vide ?
- Est-ce que les Π et les Σ peuvent être vu de la même façon que dans la théorie des ensembles (cad resp. un produit cartésien et une somme disjointe) ?
- Quel est la réponse à la grande question sur la vie, l'univers et le reste ?
En tout cas merci et continu comme ça c'est vraiment génial ce que tu fait ;)
Mes réponses (imparfaites) aux questions :
- Tout objet doit appartenir à un unique type, et le type auquel appartient un objet doit être défini dès la définition de l'objet. Si j'écris a:A, ça revient à la phrase "j'instancie un objet a de type A". Ça a des similarités avec l'appartenance mais c'est pas la même chose. En particulier, ça n'a pas de sens que de "prouver" a:B. Le symbole := ne me dit rien. J'ai peut-être loupé quelque chose. Le symbole ≡ est l'égalité définitionnelle (judgemental equality en anglais). On peut écrire :≡ pour parler de définition au moment de l'instanciation. Par exemple, si je veux construire un objet à l'aide d'une fonction f, je peux écrire y :≡ f(x). Il s'agit ainsi d'une définition. D'une certaine manière, je n'ai le droit d'écrire "y ::≡" qu'une seule fois. Je ne peux plus redéfinir y une fois qu'il a été défini. Mais ça n'empêche pas y d'être égal par définition à z, auquel cas je peux écrire y≡z.
- oui.
- oui.
- en première approximation, oui. Mais Π et Σ ont aussi des constructeurs et des principes d'induction.
- Je crois l'avoir lu quelque part mais je ne m'en souviens plus ;)
Science4All (français) Merci pour ta réponse ^^ je vais reregarder la vidéo pour essayer de mieux la comprendre en sachant ça.
+Moi j'ai parlé du type N dans l'épisode 24 : https://youtu.be/ba4E6EMagj0
je ne vois pas en quoi ce serait incompatible avec le platonicisme. Au fond toutes ces belles constructions (que je n'ai pas réussi a suivre en totalité) ne font que redéfinir des objets des mathématiques plus classiques.
Et même les objets bien spécifiques (qu'on n'a pas encore découverts) sont finalement déjà existants, juste pas encore identifiés (une sphère existe indépendamment de comment on la définit ou on l'appelle, et ses propriétés aussi).
Soit dit, je pense que c'est certainement intéressant de se pencher sur cette nouvelle interprétation des bases de la mathématique.
Simple réflexion : serait-il possible de créer un algorithme capable de trouver seul des théorèmes mathématiques encore non prouvé / non découvert à partir de cette formalisation homotopique des types ? Si je pose cette question, c'est que le sujet m'intéresse, que je ne comprends pas grand chose à tout ça mais j'y vois un intérêt probant à l'automatisation des preuves mathématiques (un peu comme le nez au milieu de la figure ... :D).
+Yarflam oui et non. Il existe déjà des algorithmes qui prouvent des nouveaux théorèmes. La théorie homotopique des types et son implémentation en Coq permettent même de compléter certains bouts de preuves pas trop difficiles.
Cependant, étant donné un théorème, en trouver une preuve est un problème algorithmique difficile, en un sens très précis. Il s'agit en fait d'un problème indécidable (il n'y a pas d'algorithmes qui y arrive à tous les coups). Et même si on se restreint à des preuves "pas trop longues", ça reste un problème NP-complet (on pense qu'aucun algorithme n'y arrivera en quelques milliards d'années)
+Science4All (français) tout ça n'exclut pas la possibilité de créer des intelligences artificielles qui soient meilleures que les meilleurs mathématiciens humains pour prouver des théorèmes...
Merci pour ta réponse. Ainsi prouver des théorèmes n'est pas totalement facilité par la théorie homotopique. Je ne pensais pas forcément à un algorithme déterministe, mais plutôt heuristique. Amener des formules à partir d'axiomes (ou équivalent), prouver qu'elles sont vraies et continuer à construire des objets toujours plus complexes - le tout en ajoutant un facteur (pseudo-)aléatoire qui déterminerait des ensembles de tests.
La difficulté, ce serait de savoir avec certitude si notre modèle de base permet de trouver suffisamment rapidement n'importe quel théorème jusqu'à maintenant démontré pour aller beaucoup plus loin. Peut-être que j'utilise mal le mot théorème ... je pense plutôt à l'idée de preuve par la formule, l'équivalence et la logique. Pas par des rapports de 1500 pages. :)
Je sais pas ce qui me fait le plus rire entre les mecs qui arrivent a suivre la video et les mecs qui sont tellement calés qu'ils arrivent a trouver des erreurs dans ta vidéo.. Ahlala a defaut de comprendre je me marre bien a chacune de tes vidéos et ca c'est cool :D (jespere qd meme pouvoir un jour les comprendre aha)
Hello !
Là je suis en train d'étudier la théorie des catégories, et je vois que il y a plein de points communs entre ce que tu nous raconte et les constructions sur la théorie des catégories (par exemple, avec la somme disjointe, on voit vraiment les flèches, que tu appelles "constructeurs"). Y-a-t-il des liens entre la théorie homotopique des types et la théorie des catégories ?
Oui ! Beaucoup même. Le chapitre 9 du livre s'appelle "Category Theory".
Merci pour la réponse ! Mais du coup la théorie des catégories c'est un cas particulier de la THT ou alors c'est quelque chose qu'on va axiomatiser avec. Ou alors la THT s’appuie dessus ?
donne des exemples bidons avec nos mathématiques usuelles , utilise des nombres
C'est hardcore ;-)
Mouais pourquoi voir simple, quand on peut tout compliquer... pour compliquer, comme si faire simple serait compliqué ?
Je suis prêt à me désabonner là...
des nombres c'est quoi ? :)
nonee noner - 2017-02-23
j'ai déjà envie de pleurer