Je ne pourrais dire mieux que la phrase concluant son article :
Ils ne sont qu’une arme de plus dans la guerre que le consumérisme mène contre l’intellectualisme.
Qui redit, à sa façon, ce que Goerges Bernanos disait dans La France contre les robots en 1946 :
On ne comprend absolument rien à la civilisation moderne si l'on n'admet pas d'abord qu'elle est une conspiration contre toute forme de vie intérieure.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).
J'ai recherché le texte de Kant sur les limites de la connaissance humaine. Je le cite pour la clarté avec laquelle il expose le problème :
La conscience de mon ignorance (si cette ignorance n’est en même temps reconnue comme nécessaire), au lieu de terminer toutes mes recherches, est au contraire la véritable cause qui les provoque. Toute ignorance porte ou bien sur les choses, ou bien sur la détermination et les bornes de ma connaissance. Or, quand l’ignorance est accidentelle, elle doit me pousser, dans le premier cas, à soumettre les choses (les objets) à une investigation dogmatique, et, dans le second, à rechercher, au point de vue critique, les limites de ma connaissance possible. Mais que mon ignorance soit absolument nécessaire, et que par conséquent elle me dispense de toute recherche ultérieure, c’est ce que l’on ne peut prouver empiriquement par l’observation, mais seulement d’une manière critique, en sondant les sources premières de notre connaissance. La détermination des limites de notre raison ne peut donc se faire que suivant des principes à priori, mais nous pouvons connaître aussi à posteriori qu’elle est bornée, en remarquant ce qui, dans toute science, nous reste encore à savoir, bien que cette connaissance d’une ignorance à jamais invincible soit encore indéterminée pour nous. La première connaissance de l’ignorance de la raison, que peut seule nous donner la critique de la raison même, est donc une science ; mais la seconde connaissance n’est qu’une perception, aux suites de laquelle je ne puis assigner des limites. Quand je me représente (suivant l’apparence sensible) la surface de la terre comme un plateau rond, je ne puis savoir jusqu’où elle s’étend. Mais l’expérience m’apprend que, où que j’aille, je vois toujours devant moi un espace où je puis continuer de m’avancer, et je reconnais ainsi les bornes de ma connaissance réelle de la terre, mais non pas celles de toute description possible de la terre. Que si j’en suis venu au point de savoir que la terre est un globe et que sa surface est sphérique, je puis alors connaître d’une manière déterminée et suivant des principes à priori, même par une petite partie de cette surface, un degré par exemple, le diamètre de la terre, et, par ce diamètre, la complète circonscription de la terre, c’est-à-dire sa surface entière ; et, bien que je sois ignorant par rapport aux objets que cette surface peut contenir, je ne le suis pas quant à la circonscription qui les contient, à son étendue et à ses limites.
Comme c'est un problématique de ce genre que traite les auteurs :
Mais que mon ignorance soit absolument nécessaire, et que par conséquent elle me dispense de toute recherche ultérieure, c’est ce que l’on ne peut prouver empiriquement par l’observation, mais seulement d’une manière critique, en sondant les sources premières de notre connaissance.
afin de répondre par la négative au sixième problème de Hilbert, il n'ont pas grand choix sur la méthode. Je ne connais que trois résultats utilisables en la matière :
l'incomplétude de Gödel (limites de la déduction)
le problème de l'arrêt de Turing (limites du calcul)
la critique kantienne (limites de la raison théorique dans son usage philosophique)
Vu la question (existence d'un système axiomatique), il n'ont pas d'autres choix que de passer par l'incomplétude de Gödel. Il l'utilise correctement en l'appliquant à un système adéquate aux hypothèses du théorème (contrairement à Régis Debray. Mais une fois obtenue l'incomplétude déductive du système, le reste de l'argumentaire devient de plus en plus douteux.
D'ailleurs, les mathématiciens (toujours dans le cadre du programme de Hilbert) ont eux aussi cherché un système axiomatique unique dans lequel toutes les mathématiques connues pourraient se formaliser (un anneau pour les gouverner tous ;-). Rien ne disait que c'était faisable, et ce fût fait sous la forme de la théorie axiomatique des ensembles ZF. Elles est bien entendue incomplète, car soumise au théorème d'incomplétude, mais cela n'a jamais perturbé personne. On n'a nullement invoqué je ne sais quel entendement non algorithmique en conséquence. Bien au contraire, cela a ouvert un champ de recherche luxuriant : quels sont les énoncés ayant un sens mathématique important qui sont indécidables dans ZF ? On a au choix : toutes les formes de l'axiome du choix, l'hypothèse du continue de Cantor, l'existence ou non de partie des réels non mesurables au sens de Lebesgue, les axiomes sur les grands ordinaux… Cela a donné des résultats, dits de consistance relative, analogues à ceux obtenus par Poincaré sur la consistance relative des différentes géométries (euclidienne, hyperbolique et sphérique). Et toutes ces mathématiques sont algorithmiques de part en part, du moins on a pour l'instant ZF + Choix dépendant en logique classique interprété comme programmes via Curry-Howard, et ce système est suffisant pour développer tout l'outillage conceptuel actuellement utilisé par les physiciens théoriciens.
Et malgré cela, certains continuent, à bon droit, de chercher des théories concurrentes à ZF, à commencer par la théorie homotopique des types (HoTT) ou celle spéculative du sujet de thèse de Jeanas.
Après, que l'entendement humain soit non algorithmique, je n'en doute pas une seconde. Mais c'est parce qu'il ne sert pas qu'à faire des mathématiques, il sert aussi à philosopher. L'usage mathématique est algorithmique, pas son usage philosophique. Ça c'est Kant qui l'a prouvé.
Les mathématiques donnent le plus éclatant exemple d’une heureuse extension de la raison pure par elle-même et sans le secours de l’expérience. Les exemples sont contagieux, surtout pour cette faculté, qui se flatte naturellement d’avoir toujours le même bonheur qu’elle a eu dans un cas particulier. Aussi la raison pure espère-t-elle pouvoir s’étendre, dans son usage transcendental, avec autant de bonheur et de solidité qu’elle l’a fait dans son usage mathématique, surtout en appliquant ici cette même méthode qui lui a été là d’une si évidente utilité. Il nous importe donc beaucoup de savoir si la méthode qui conduit à la certitude apodictique, et que dans cette dernière science on appelle mathématique, est identique à celle qui sert à chercher cette même certitude dans la philosophie et qui y devrait être appelée dogmatique.
La connaissance philosophique est la connaissance rationnelle par concepts, et la connaissance mathématique la connaissance rationnelle par construction des concepts. Construire un concept, c’est représenter à priori l’intuition qui lui correspond. La construction d’un concept exige donc une intuition non empirique, qui par conséquent, comme intuition, soit un objet singulier, mais qui n’en exprime pas moins, comme construction d’un concept (d’une représentation générale), quelque chose d’universel qui s’applique à toutes les intuitions possibles appartenant au même concept. Ainsi je construis un triangle en représentant l’objet correspondant à ce concept soit par la simple imagination dans l’intuition pure, soit même, d’après celle-ci, sur le papier dans l’intuition empirique, mais dans les deux cas tout à fait à priori, sans en avoir tiré le modèle de quelque expérience. La figure particulière ici décrite est empirique, et pourtant elle sert à exprimer le concept sans nuire à son universalité, parce que, dans cette intuition empirique, on ne songe jamais qu’à l’acte de la construction du concept, auquel beaucoup de déterminations sont tout à fait indifférentes, comme celles de la grandeur, des côtés et des angles, et que l’on fait abstraction de ces différences qui ne changent pas le concept du triangle.
La connaissance philosophique considère le particulier uniquement dans le général, et la connaissance mathématique le général dans le particulier, même dans le singulier, mais à priori et au moyen de la raison, de telle sorte que, comme ce singulier est déterminé d’après certaines conditions générales de la construction, de même l’objet du concept auquel ce singulier ne correspond que comme son schème doit être conçu comme universellement déterminé. […]
Puisque nous nous sommes fait un devoir de déterminer exactement et avec certitude les limites de la raison pure dans l’usage transcendental, mais que cette faculté a ceci de particulier que, malgré les avertissements les plus pressants et les plus clairs, elle se laisse leurrer par l’espoir de parvenir, par de là les limites des expériences, dans les attrayantes contrées de l’intellectuel, il est nécessaire de lui enlever encore en quelque sorte la dernière ancre d’une espérance fantastique, en lui montrant que l’application de la méthode mathématique dans cette espèce de connaissance ne peut lui procurer le moindre avantage, si ce n’est peut-être celui de lui découvrir plus clairement ses propres défauts ; que la géométrie et la philosophie sont deux choses tout à fait différentes, bien qu’elles se donnent la main dans la science de la nature, et que par conséquent les procédés de l’une ne peuvent jamais être imités par l’autre.
La solidité des mathématiques repose sur des définitions, des axiomes et des démonstrations. Je me contenterai de montrer qu’aucun de ces éléments ne peut être ni fourni ni imité par la philosophie dans le sens où le mathématicien le prend ; que le géomètre, en transportant sa méthode, dans la philosophie, ne construit que des châteaux de cartes ; que le philosophe, en appliquant la sienne aux mathématiques, ne peut faire que du verbiage ; ce qui n’empêche pas que le rôle de la philosophie dans cette science ne soit d’en reconnaître les limites, et que le mathématicien lui-même, quand son talent n’est pas déjà circonscrit par la nature et restreint à sa sphère, ne soit obligé de tenir compte des avertissements de la philosophie et de ne pas se mettre au-dessus d’eux.
Et la physique a tout autant besoin de la philosophie que des mathématiques pour justifier ses premiers principes, à commencer par le principe de causalité, et pour se faire elle ne peut emprunter la méthode algorithmique des mathématiques.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Si je comprends bien, il ne s'agit pas ici de créer un "univers" (un système formel) sans contrainte a priori par rapport à la réalité physique mais de reformuler (donc a posteriori) sous forme d'axiomes les postulats d'une théorie physique sur le réel pour s'assurer de leur "validité", "objectivité", consistance, …
Oui, on ne va tout de même pas prétendre pouvoir faire sortir, comme par magie, de notre esprit, des lois de la nature qui ne peuvent être connus que par expérience.
Comme je l'ai dit par analogie avec la programmation, les spécifications, bien que formalisées et constituant une axiomatique du domaine métier, ne peuvent être formulées que par la connaissance expérimentale du dit domaine. Et l'on y retrouve les deux classes de bugs dans les logiciels : non conformité du code avec les spécifications (c'est là que les systèmes de types jouent un rôle), non conformité des spécifications avec le domaine (cela, aucune méthode formelle ne peut les résoudre).
Cela étant, il reste toujours un part d'a priori dans les théories physiques, que l'on ne peut totalement éliminer pour tout ramener à l'expérience. C'est cela que Kant avait formidablement remarqué (on le retrouve dans Curry-Howard) et que Hilbert espérait résoudre via l'axiomatisation de la physique. On le retrouve dans ce passage de l'article :
Autrement dit, l'axiomatisation de la physique nous permet de nous dégager de la géométrie euclidienne, qui, provenant de notre intuition spatiale, était jusqu'à présent un présupposé
anthropomorphique implicite à notre conception de la structure du monde empirique. Or, en axiomatisant la physique, il devient possible de se dégager de ce présupposé et ainsi atteindre une connaissance plus objective.
Pour un kantien, il restera toujours un fond a priori dans les sciences de la nature. Voir par exemple l'exemple des lois de l'electricité par Ampère, décrite dans cette article : La déraisonnable efficacité des mathématiques. Comme dit dans l'article, c'est lié à ce que Kant appelait sa théorie du schématisme, ce qu'exprime à sa façon la correspondance preuve-programme : les preuves sont des programmes, c'est-à-dire des schèmes (en terme kantien), et l'on ne peut s'en passer pour appréhender le réel. J'aime beaucoup les deux citations de Paul Valéry qui sont si kantienne dans l'esprit :
La mathématique est la science des actes sans les choses et par là des choses que l'on peut définir par des actes.
Quand les contenus sont créés par les opérations mêmes, c'est-à-dire quand quand des opérations remarquées sont désignées, isolées et qu'on en forme des combinaisons, alors on est en mathématiques
Paul Valéry.
On le retrouve dans la conférence donnée par Stéphane Mallat lors du colloque de rentrée au Collège de France sur l'intelligence artificielle : Mystères mathématiques d’intelligences pas si artificielles. À partir de la quatrième minute, il aborde la théorie de la connaissance et les deux tendances qui s'opposent depuis l'antiquité : rationalisme contre empirisme (Platon contre Aristote). Il évoque plus particulièrement David Hume (empiriste) qui mit en doute la notion même de causalité, et Kant qui vint développer la troisième voie : la méthode critique entre le dogmatisme rationaliste et le scepticisme empirique. Il soutient que l'approche des réseaux neurones tient du kantisme mais ne développe pas trop ses raisons, si ce n'est qu'il y a, aussi, une dimension d'a priori dans les réseaux de neurones.
Mais je veux surtout rebondir sur Hume, la causalité et son rapport à Kant. C'est Hume qui fit sortir Kant de son sommeil dogmatique (l'expression est de Kant lui-même) par son attaque contre le principe de causalité. Et la réponse de Kant fut ce qu'il est convenu d'appeler sa théorie des catégories qui est une correspondance preuve-programme bien avant l'heure : la Critique de la Raison Pure date de 1781 et la dite correspondance de la fin des années 1960. La réponse de Kant à Hume fut celle-ci : le principe de causalité n'est pas d'origine empirique, mais nous l'imposons a priori au réel en conformité avec la forme logique des jugements hypothétiques.
Que voulait-il dire par là ? Faisons un détour par la théorie de la démonstration. Parmi les règles de déduction employées par les mathématiciens, il y en a une bien connue sous le nom de modus ponens : si A alors B, or A donc B. Et cette règle est celle qui sert à typer l'application de fonction dans les langages fonctionnels (c'est la base de la correspondance de Curry-Howard). Mais cette règle de typage a un principe analogue dans l'analyse formelle des langages impératifs, c'est le cœur de logique de Hoare avec ses triplets de Hoare {P} C {Q} : un programme C a pour résultat de passer de P à Q. Autrement si ma machine est dans l'état P alors en éxécutant le programme C, elle sera dans l'état Q. Et c'est explicitement ce que Kant avait exposé dans sa table des catégories, via la correspondance entre la table des jugement et la table des catégories. Où l'on voit la correspondance entre les jugements hyptothétiques (si A alors B) et la causalité. Correspondance qu'exprime à leur manière Curry-Howard et Hoare : les programmeurs fonctionnels composent les fonctions, comme les programmeurs impératifs composent les instructions. Et c'est ce lien entre ces deux logiques qui expliquent pourquoi l'on peut automatiser (c'est à dire construire des machines soumises à la causalité) l'exécution des algorithmes et non les exécuter seulement à la main.
On retrouve cette correspondance de la logique dans la confrontation même des théories physiques avec l'expérience. La physique pose une loi causale (en arrière plan, il y a la forme logique si A alors B), constate un état A et observe non B : il y a contradiction entre le réel et la théorie. Conséquence : soit la loi est fausse, soit l'état A était mal déterminé. Deux exemples issu de de la cosmologie :
les perturbations orbitales de Mercure ne correpondent pas aux observations : on prédit B mais on observe non B, on émet l'hypothèse de l'existence d'une autre planète (on pose non A), à savoir Pluton, sans changer la loi ;
le périhélie de Mercure ou la déviation des rayons lumineux par le Soleil, on change la loi (le si A alors B) et on passe à la relativité générale.
Là tu te dis peut être : mais what the fuck !? De quel droit peut-on imposer totalement a priori des lois à la nature (non selon le contenu mais selon la forme) sans même les emprunter à l'expérience ? C'est là que Kant et les kantiens répondent en cœur avec l'enfant bouddhiste de Matrix : la cuillière n'existe pas ! :-P Derrière cette boutade, il y a le principe que si l'on voit partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous mêmes. Donc, d'un point de vue expérimentale, la cuillère existe bien, certes, comme objet spatio-temporellement déterminable. Mais si l'on fait abstraction de son rapport à un observateur, et que l'on se demande : cette chose qui nous apparaît sous la forme d'une cuillière, est-elle en elle même dans l'espace et dans le temps, soumise à la causalité… À cela nous répondons : non ! En tant qu'objet d'expérience possible elle l'est, mais abstraction faite du rapport à l'expérience elle ne l'est pas. Il n'y a pas de réalité absolument indépendante de l'esprit humain qui serait objet d'étude de cette science que l'on nomme physique.
Par exemple, reformuler les six postulats de la mécanique quantique sous forme d'axiomes, ça a été tenté ?
Je ne sais pas. Je ne suis pas assez les travaux de physiciens théoriciens pour le savoir, mais il y a de très forte chance qu'il y ait eu des tentatives.
Pour en revenir à l'objet du lien, utiliser le concept d'axiomatisation de la physique malgré sa nature très différente de l'axiomatisation des systèmes formels pour y faire des "démonstrations" basées sur ce qui a été démontré dans le cadre d'un système formel (les théorèmes de Gödel, notamment) me paraît douteux mais je n'ai largement pas le niveau pour aller au delà de ce doute "naïf". Je note cependant que tu n'es pas davantage convaincu.
Leur usage du théorème d'incomplétude est parfaitement valide. Ce que je ne comprends pas c'est quand ils arguent l'existence de phénomènes observables, donc dont on peut déterminer la valeur de vérité, qui sont hors du champ de la déductibilité du système : il y a des formules non déductibles, le système étant déductivement incomplet, mais en quoi correspondent-elles à des phénomènes observables ? De mémoire, chez Penrose, c'est le phénomène de réduction de la fonction d'ondes ou réductions du vecteur d'états en mécanique quantique qui l'amène à développer sa notion d'entendement non algorithmique. Mais dans cet article, bien court et peu développé, les principes tombent un peu comme un cheveux sur la soupe. Donc je ne sais quoi en dire, d'autant que je suis loin d'être un spécialiste du sujet. Mais je doute qu'il puisse convaincre ceux qui s'occupent du sixième problème de Hilbert.
Pour finir, avec une remarque quelque peu hors-sujet. Kant ne s'est pas contenté de faire usage de son système pour justifier l'usage des mathématiques en physique et la légitimité de certains principes a priori. Il l'a même étendu à la doctrine du droit et à la philosophie politique. Question : pourquoi nos États sont-ils structurés autour de trois pouvoirs (législatif, exécutif et judiciaire). Réponse :
Tout État renferme en soi trois pouvoirs, c’est-à-dire que l’unité de la volonté générale s’y décompose en trois personnes (trias politica) : le souverain pouvoir (la souveraineté), qui réside dans la personne du législateur ; le pouvoir exécutif, dans la personne qui gouverne (conformément à la loi) ; et le pouvoir judiciaire (qui attribue à chacun le sien suivant la loi), dans la personne du juge (potestas legislatoria, rectoria et judiciaria). Ce sont comme les trois propositions d’un syllogisme pratique : la majeure, qui contient la loi d’une volonté ; la mineure, l’ordre de se conduire d’après la loi, c’est-à-dire le principe de la subsomption des actions sous cette loi ; enfin la conclusion (la sentence), qui décide ce qui est de droit dans le cas dont il s’agit.
Kant, Doctrine du droit.
Autrement dit : nous ne faisons que projeter dans la constitution de nos États la structure formelle de notre propre esprit : raison (législatif), entendement (exécutif) et faculté de juger (législatif).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Alors je vais sûrement passer pour l'ignare de service qui s’immisce dans un débat qui le dépasse mais j'assume : c'est comme ça qu'on apprend :-)
Si je peux te donner conseil : conserve précieusement cette maxime, et ne cesse jamais d'en faire usage.
Le même prof qui avait plaisanté sur les sanctifiés du Pape nous avait donné ce principe dès les premières minutes de son premier cours :
Si vous ne comprenez pas quelque chose, n'hésitez pas à m'interrompre. Je m'arrêterais pour expliquer. Autrement, je continuerais partant du principe que vous avez compris.
Je n'ai jamais hésité à l'interrompre, et il a toujours satisfait à ma requête. Néanmoins, dans le cadre d'une salle de classe, j'ai pu constaté que nombreux sont ceux n'ayant jamais osé (bien qu'il ne comprenait pas), sans doute de peur de passer pour des idiots. Le problème de la peur du regard des autres…
Du coup, ça veut dire quoi, une axiomatisation de la physique ?
Il faut voir cela avec David Hilbert, c'est son sixième problème.
Le sujet étant long et complexe, j'ai trouvé ce texte en ligne : la portée epistémique de l'axiomatisation de la physique chez Hilbert. Cela reste tout de même un texte très technique qui revient tout d'abord sur l'utilité et la raison d'être de l'axiomatisation pour les mathématiques, avant de traiter de la volonté d'Hilbert d'étendre la méthode à la physique.
Mais sinon, en version plus simple et courte : c'est ce que font tous les programmeurs du monde. Lorsqu'une équipe de programmeurs établit un cahier des charges puis écrit les spécifications du logiciel qu'ils doivent écrire, ils axiomatisent leur domaine métier. Ensuite charge à eux de réifier cette axiomatique, c'est à dire implémenter les spécifications.
C'est là qu'intervient l'utilité pour les programmeurs du domaine de recherche de Jeanas, la théorie des types et la correspondance preuve-programme. Un système de type est un langage dans lequel on peut exprimer ses spécifications, le type checker vérifiant que le code est conforme aux types. Plus le systèmes de types est évolué, plus on peut exprimer finement ses spécifications, et moins il y a de bug (de code non conforme aux spécifications). Et c'est ce qu'on toujours fait les mathématiciens : la preuve d'un théorème est un programme dont l'énoncé est la spécification. Prenons l'exemple du théorème affirmant qu'il existe un nombre infini de nombres premiers. Celui-ci affirme que « pour tout entier n, il existe un entier p premier et strictement plus grand que n ». Toute preuve de ce théorème est un programme qui prend en entrée un entier n, et renvoie en sortie un entier p premier et plus grand que l'entrée. C'est cela la correspondance de Curry-Howard ou correspondance preuve-programme (toute preuve mathématique a un contenu algorithmique, est un programme). Vérifier qu'une preuve est logiquement valide (elle respecte bien les règles de déduction et les axiomes de la théories) ou vérifier qu'un programme est bien typé, c'est tout un ! Un vérificateur de preuves ou un type checker, c'est le même logiciel.
Sur le sujet, il y a ce texte bien plus abordable à lire et comprendre que le premier (je te le conseille pour commencer): À propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court). L'auteur est aussi un de mes anciens professeurs, celui qui m'initia à ce domaine de la logique. Il est l'auteur d'une machine abstraite La machine de Krivine dont le but était d'interpréter les preuves de théorèmes comme des programmes. Elle est proche, dans son fonctionnement, à la première machine abstraite qui interprétait le bytecode du langage OCaml (la ZINC).
Sinon, pour revenir à de la programmation de tous les jours : utiliser un types primitif d'un langage, c'est poser une axiomatique (tout ce que le langage fournit sur ce type est une axiomatique); programmer contre une classe abstraite, c'est poser une axiomatique (celle décrite par l'interface de la classe); utiliser des interfaces en golang, c'est faire de l'axiomatique (celle décrite par l'interface); utiliser des traits en Rust idem, des types classes en Haskell idem, des foncteurs en OCaml idem… Je n'ai jamais croisé un développeur de ma vie qui ne faisait pas de l'axiomatique sans le savoir (à la manière de monsieur Jourdain).
Enfin, c'est pour cela que je suis sur un site dédié aux logiciels libres : de même qu'une preuve mathématique se doit d'être publique, un code doit l'être; conceptuellement ce ne sont pas deux types d'objets distincts, mais les deux faces d'une seule et même pièce.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Donc c'est plus en lien avec la théorie de la démonstration et la correspondance de Curry-Howard ou correspondance preuves-programmes. Tu es plus du côté informatique (systèmes de types pour les langages de programmation) ou mathématique (HoTT, interprétation des preuves comme programmes, logique classique ou intuitionniste) ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Juste deux petits exemples pour contextualiser ce jugement à l'emporte pièce sur la seule base du titre
Ce jugement semble ne pas avoir été apprécié par un membre du site, à en juger par ma note.
Dans les années 90, les meilleurs physiciens appliqués, spécialisés en traitement du signal, armés de solides théorèmes mathématiques nous démontraient irréfragablement les limites théoriques en matière de signal transporté sur du câble en cuivre (les fameux xx kbauds). Puis quelqu'un inventa l'ADSL…
À la même époque, d'autres physiciens (Sokal et Bricmont) reprochaient à certains philosophes français leur usage saugrenu de l'incomplétude de Gödel.
Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).
L'un n'empêche pas l'autre. Notre connaissance peut être bornée quant aux contenu du monde (bornée par ce qu'il reste encore à découvrir) mais nous pouvons être en mesure de déterminer les limites du savoir humain (ce que font les méthodes formelles). Kant avait une belle image pour illustrer cela : je peux ignorer le contenu effectif de la surface du globe (il faudrait pour cela en avoir parcouru la totalité) tout en sachant qu'il est circonscrit dans des limites données que je peux déterminer (je n'ai pas besoin de le parcours pour connaître sa circonférence).
Cela étant j'ai fini par lire l'article est je suis moins catégorique que Jeanas sur son contenu : ce n'est pas du Régis Debray. La thèse principale n'est pas tant que nous ne vivons pas dans une simulation, mais qu'une théorie du tout qui unifierait la relativité générale et la physique quantique n'est pas axiomatisable. En résumé : la physique n'est pas axiomatisable. Ce qui a pour corrolaire que l'univers n'est pas une simulation d'ordinateur.
Dans l'ensemble, bien que je souscrives personnellement à ces thèses métaphysiques, leur argumentaire ne me convainc que moyennement. D'une part parce que je doute que la méthode mathématique soit la seule à même de traiter ces questions. D'autre part, parce que l'article consiste à formaliser la thèse de Roger Penrose d'entendement non algorithmique (non algorithmic understanding), thèse qu'il développe par exemple dans son livre Les deux infinis et l'esprit humain. Cette thèse me semblait pas très claire à l'issue de ma lecture du livre, et l'article ne change pas la donne dessus.
Ils font effectivement usage des deux théorèmes de Gödel que j'ai évoqué dans mon premier commentaire. Tout commence à la troisième page de l'article, lorsqu'il suppose une axiomatisation de la physique en supposant l'existence d'un système formel , dont la signification doit vouloir dire : Formalisation of Quantic Gravitation. Il font sur le système des hypothèses raisonnables : logique du premier ordre, ensemble d'axiomes récursivement énumérables, système complet de règles d'inférence. À dire vrai, ces derniers hypothèses n'en sont pas, c'est la définition même de la proposition « la physique est axiomatisable ».
À cela ils ajoutent deux contraintes :
l'arithmétique de Peano est dérivable dans ce système axiomatique ;
tout les phénomènes observables sont prévisibles par la théorie (conséquence du système d'axiomes par les règles de déduction)
On peut bien leur accorder la première, la physique théorique ayant besoin de l'arithmétique. C'est celle-ci qui leur permet de faire usage du théorème d'incomplétude : le système axiomatique étant une extension de l'arithmétique de Péano, il est déductivement incomplet.
Mais ensuite, je dois avouer avoir du mal à les suivre dans leur pensée. Ils semblent jongler entre syntaxe et sémantique : il y aurait des énoncés observables, et donc vrais (théorie de la vérité correspondance, sémantique de Tarski), dans l'univers (cf. deuxième contrainte), mais qui ne seraient pas conséquences déductives du système d'axiomes (que l'on pourrait obtenir à partir des axiomes de l'ensemble Sigma et des règles R). Peut être bien, mais lesquelles ? C'est à partir de là qu'ils introduisent leur méta-théorie non algorithmique, leur entendement non algorithmique à la Penrose et qu'ils me perdent. Non que ce genre de méta-théorie ne soient pas considérées par les logiciens mathématiciens (en théorie des modèles, on étudie bien les modèles non standard de l'arithmétique, des théories non récursivement énumérables voir même non dénombrables), mais je ne comprends pas selon quels principes ils l'introduisent ni la justifient.
Ça a au moins l'intérêt de montrer certaines limites des systèmes de publications.
Cela me rappelle une blague de notre professeur de théorie des modèles, lorsque j'étais étudiant en DEA de logique mathématique et fondements de l'informatique. Il faut faire attention, ici, que le mot modèle est un homonyme de celui utilisé en physique (bien qu'il y ait des rapports entre les deux). Pour un théoricien des modèles, à la question qu'est-ce qu'un groupe ? Il répond : un modèle de la théorie des groupes, c'est à dire une structure qui satisfait à l'axiomatique de la théorie.
Trève de digression et revenons à sa blague. Un jour, en début du cours, il nous tint à peu près ce discours : « je lisais ce matin dans le Monde que la pape Jean Paul II avait sanctifié plus de personnes que tous ces prédécesseurs réunis. Sachant que, durant ces 20 dernières années, on a publié plus d'écrits mathématiques que durant toute la période de l'humanité qui précède, si un jour vous publiez un article insignifiant, vous pourrez vous considérer en bijection avec un sanctifié du pape ! ».
Je dois admettre, après lecture de l'article, que je ne sais quoi dire sur le statut de sanctifiés de ses auteurs.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Quand je vois ce genre de titre, je n'ai même pas envie de lire l'article. Ce n'est pas la première fois, ni la dernière, que l'on fera dire n'importe quoi aux théorèmes de Gödel. Mais même si les physiciens s'y mettent, on n'est pas sorti de l'auberge.
De toute façon, comme je suis kantien, la question n'a même pas de sens pour moi : comme dit le petit enfant boudhiste dans le premier Matrix, « la cuillère n'existe pas ». :-P
Tu fais une thèse en théorie de la démonstration ? ou en calculabilité ? C'est là où j'y vois trois résultats fondamentaux :
théorème de complétude de Gödel
théorème d'incomplétude de Gödel
correspondance de Curry-Howard (logique intuitionniste et classique)
Théorèmes qui ne font que confirmer le cœur de la philosophie kantienne, et l'inexistence de la cuillère.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
il ne faut pas forcément prendre les chiffres pour argent comptant
Au delà de prendre les chiffres pour argent comptant, je vois ce que cela donne chez moi. En mai, pendant que je préparais ma terre, mon voisin se plaigner du manque d'eau, alors que, hormis le premier centimètre, mon sol état noir et gorgé d'eau.
Cherche un peu sur la chaîne agriculture vivrière et tu pourras constater la différence de structure entre deux terres à peine séparées de quelques dizaines de mètres (ce n'est pas chez moi, mais l'idée est la même). ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Ton article parle d'expérimentations, c'est très bien mais il ne faut pas forcément prendre les chiffres pour argent comptant,
Sur cette article c'est une petite expérimentation (petite ferme en maraichâge). Mais il y a eu des expérimentations à plus grandes échelle en Suisse (canton de Vaud), où ils dépassent de loin l'objectif du 4 pour mille. Et dans la série de vidéos donnée au dessus (journée de conférence), il y a une usine de production de pop corn qui avance un bilan carbone bénéfique (elle séquestre plus de carbone qu'elle n'en émet), avec encore de la marge de manœuvre : 80% des terres sont en non labour (il reste 20% de marge de manœeuvre) et ils travaillent à la réduction sur le transport.
ça nécessite une vision à grande échelle quand même
Ça nécessite un changement de pratique, qui ne sera certainement pas facile à mettre en place : cela nécessite une remise en cause de 10_000 ans de pratiques agricoles. Il est sûr que cela ne se fera pas du jour au lendemain.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
C'est sans doute pas le cas et pour vraiment à revenir à l'état antérieur faudrait retirer énormément de CO2 de l'athmosphère et ça c'est encore en partie dépendant de paris technologiques (qui peuvent être source d'inaction).
Où alors, un des leviers d'actions est le recul d'usage de la technologie. Si nos agriculteurs rengeaient leurs tracteurs pour arrêter le labour, ils pourraient stocker dans le sol nos émissions annuelles, voir plus. Adopter les méthodes de sol vivant pour inverser son bilan carbone.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Il y va fort, Mr Phi, notamment quand il émet des doutes sur les aptitudes mathématiques de Luc Julia.
Je n'ai pas regardé la vidéo, donc je ne préjugerais pas des aptitudes de Luc Julia. En revanche mon expérience passée sur Mr Phi m'a amené cette conclusion : je ne doute pas de ses aptitudes en mathématiques, il n'en a aucune, et pour la philosophie, il est comme nombre des personnes formées à l'école française : s'il a une tête bien pleine (histoire de la philosophie), il n'est pas certain qu'elle soit bien faite. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Disons que je ne comprends pas sa sociologie de la science, peut-être d'ailleurs parce que ça correspond à une époque lointaine et que le fonctionnement de la science a beaucoup changé depuis.
Oui ça doit être cela, tu ne comprends pas sa sociologie des sciences. Je ne crois pas que celà ait beaucoup évolué depuis son époque, si ce n'est la hausse de volume de cette catégorie :
Mais beaucoup d'autres se rencontrent également en se Temple qui, exclusivement pour une raison utilitaire, n'offrent en contrepartie que leur substance cérébrale !
Et d'ailleurs, dans ton commentaire, tu décris très bien ce que cette catégorie apporte au bon fonctionnement du système.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Qu'est-ce qui t'ennuis dans ce texte (tronqué, la suite et bien plus inintéressante) ? Le fait que, malgré ton doctorat et ta carrière de chercheur, certaines personnes te considèrent comme une être secondaire ? tu as une revanches à prendre sur la vie ?
La vision d'Einstein est quand même celle d'un élitisme scientifique assez vertigineux
Elle est celle de ceux qui, comme pierre essentielle, font la Science. (Je n'en fait pas, moi même partie, mais mon intellect a besoin de ces personnes hors normes pour se nourrir).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Repousser un peu les limites ou améliorer la physique ou les maths ne signifie pas que ce soit le cas. Einstein a pu faire ça tout en restant humain (enfin, je crois ?).
Demandons donc son avis à Einstein sur la question du savoir et de la science.
Le temple de la Science se présente comme une construction à mille formes. Les hommes qui le fréquentent ainsi que le motivations morales qui y conduisent se révèlent tous différents. L'un s'adonne à le Science dans le sentiment de bonheur que lui procure cette puissance intellectuelle supérieure. Pour lui la Science se découvre le sport adéquat, la vie débordante d'énergie, la réalisation de toutes les ambitions. Ainsi doit-elle se manifester ! Mais beaucoup d'autres se rencontrent également en se Temple qui, exclusivement pour une raison utilitaire, n'offrent en contrepartie que leur substance cérébrale ! Si un ange de Dieu apparaissait et chassait du Temple tous les hommes qui font partie de ces deux catégories, ce Temple se viderait de façon significative mais on y trouverait encore tout de même des hommes du passé et du présent. Parmi ceux-là nous trouverions notre Planck. C'est pur cela que nous l'aimons.
Je sais bien que, par notre apparition, nous avons chasser d'un cœur léger beaucoup d'hommes de valeurs qui ont édifié le Temple de la Science pour une grande, peut être pour la plus grande partie. Pour notre ange, la décision serait bien difficile dans grand nombre de cas. Mais une constatation s'impose à moi. Il n'y aurait eu que des individus comme ceux qui ont été exclus, eh bien le Temple de ne se serait pas édifié, tout autant qu'une forêt ne peut pas s'édifier si elle n'est constituée que de plantes grimpantes !
Einstein, Comment je vois le monde.
Mon avis sur la question, qui marche dans les pas d'Einstein, est celui-ci : l'ange de Dieu se retrouve, de nos jours, avec un critère infaillible : ceux qui sont remplaçables par un automate n'aurait jamais pu édifier et ne contribuerons que marginalement à l'édification du temple de la Science. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Je n'ai pas insisté sur mon message précédent. Mais crois tu vraiment aux coccinelles comme solutions miracles contre les pucerons ? Et produis-tu ta nourritures ou contes tu sur autrui pour le faire à ta place ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Ya pas besoin d'avoir un doctorat en biochimie pour comprendre le consensus scientifique, lire le modus operandi et les conclusions d'études, et se faire une opinion.
Certes un doctorat biochimie n'est pas nécessaire, mais déjà se nourrir soi même devrais pauser des questions (et si on le pratique, le coup des coccinelles fait rire jaune).
Personnellement; je produis plus de 50% de ma nourriture végétale (sans pesticides, en mode maréchal sur sol vivant ;-) Et, honnêtement, bien que je souhaites les changements de pratiques, je ne suis pas sûr que cela puisses se faire du coq à l'âne.
Si notre espoir est celui-là :
le chemin est celui là :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Car peut être que « la vérité » n'existe pas (en tout cas celles de Isaac, d'Albert ou de Donald sont peut être différentes).
Soutiens-tu que la notion de vérité est vide de sens et qu'en conséquence il ne peut exister de science (quelque soit son objet d'étude) ?
si le savoir ne vient pas de l'expérience, d'où provient il ?
Là tu accordes qu'il existe un savoir, et donc une véritié des propositions qu'il contient. Mais alors penses-tu que les critères de vérités des mathématiques sont fondées sur l'expéreince ? Si c'est le cas, sache qu'aucun mathématicien au monde ne te l'accordera. ;-)
Alors, il reste la question d'où vient ce savoir : il est codé en dure dans notre faculté de savoir, l'expérience est l'occasion pour nous de le mettre en action et c'est lors de cette mise à l'épreuve que nous en prenons conscience.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Après réflexion, j'appelle cela une non réponse. Ma question était pourtant simple : comment une science qui ne prend pas ses critères de vérités sur l'expérience, peut elle être utile pour la connaissance expérimentale ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
La question n'était justement pas rhétorique, je peux justifier mon point de vue. Malheureusement, cela sera très absrtait, et si je dois rendre accessible la réponse au commun des mortels (comme laisse sous entendre le reste de ton commentaire), je crains que mes capacités de vulgarisation ne soient pas au niveau.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Alors, après je pourrais toujours montrer en quoi Einstein a suivi ces principes. La question est dois-je le faire ? (Comme la réponse est longue, il ne faudra pas s'étonner si elle prend du temps).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Du coup pour moi une thèse de mathématique c'est a minima une expérience de vie. :)
Je ne te le fais pas dire. La vie de Grothendieck sue radio france en donne une idée.
Mais il reste, tout de même, que bien qu'en tant que mathématicien on ne prend pas l'expérience comme juge de paix de la vérité de nos jugements, les physiciens n'ont pas d'autre choix que d'utiliser notre langage. Mais alors, pourquoi ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Oui, mais ça ne change rien au fondement de ma thèse. Les critères de vérités des mathématiques pures ne sont pas fondés sur l'expériences, néanmoins elles n'ont pas d'autres usages qu'expérérimental (d'où les maths applis, où l'on envoie les moins bons étudiants).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
C'est bien de me prêter des intentions et de me traiter, en sous-main, d'imbécile.
C'est récurrent chez Barmic. Depuis qu'il a découvert le concept de biais, il en voit partout chez ses interlocuteurs, mais jamais chez lui. Va comprendre !
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Cherche un directeur ou une directrice de thèse qui accepteront de t'encadrer pour soutenir une thèse mathématique qui serait fondait sur l'observation du monde (j'ai bien dit une thèse de mathématique, pas de physique théorique). Si tu en trouves un ou une, je te tire mon chapeau. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# Pas mieux.
Posté par kantien . En réponse au lien La guerre que mènent les robots ascientifiques contre la solitude intellectuelle. Évalué à 10 (+12/-0).
Je ne pourrais dire mieux que la phrase concluant son article :
Qui redit, à sa façon, ce que Goerges Bernanos disait dans La France contre les robots en 1946 :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 3 (+1/-0).
J'ai recherché le texte de Kant sur les limites de la connaissance humaine. Je le cite pour la clarté avec laquelle il expose le problème :
Comme c'est un problématique de ce genre que traite les auteurs :
afin de répondre par la négative au sixième problème de Hilbert, il n'ont pas grand choix sur la méthode. Je ne connais que trois résultats utilisables en la matière :
Vu la question (existence d'un système axiomatique), il n'ont pas d'autres choix que de passer par l'incomplétude de Gödel. Il l'utilise correctement en l'appliquant à un système adéquate aux hypothèses du théorème (contrairement à Régis Debray. Mais une fois obtenue l'incomplétude déductive du système, le reste de l'argumentaire devient de plus en plus douteux.
D'ailleurs, les mathématiciens (toujours dans le cadre du programme de Hilbert) ont eux aussi cherché un système axiomatique unique dans lequel toutes les mathématiques connues pourraient se formaliser (un anneau pour les gouverner tous ;-). Rien ne disait que c'était faisable, et ce fût fait sous la forme de la théorie axiomatique des ensembles ZF. Elles est bien entendue incomplète, car soumise au théorème d'incomplétude, mais cela n'a jamais perturbé personne. On n'a nullement invoqué je ne sais quel entendement non algorithmique en conséquence. Bien au contraire, cela a ouvert un champ de recherche luxuriant : quels sont les énoncés ayant un sens mathématique important qui sont indécidables dans ZF ? On a au choix : toutes les formes de l'axiome du choix, l'hypothèse du continue de Cantor, l'existence ou non de partie des réels non mesurables au sens de Lebesgue, les axiomes sur les grands ordinaux… Cela a donné des résultats, dits de consistance relative, analogues à ceux obtenus par Poincaré sur la consistance relative des différentes géométries (euclidienne, hyperbolique et sphérique). Et toutes ces mathématiques sont algorithmiques de part en part, du moins on a pour l'instant ZF + Choix dépendant en logique classique interprété comme programmes via Curry-Howard, et ce système est suffisant pour développer tout l'outillage conceptuel actuellement utilisé par les physiciens théoriciens.
Et malgré cela, certains continuent, à bon droit, de chercher des théories concurrentes à ZF, à commencer par la théorie homotopique des types (HoTT) ou celle spéculative du sujet de thèse de Jeanas.
Après, que l'entendement humain soit non algorithmique, je n'en doute pas une seconde. Mais c'est parce qu'il ne sert pas qu'à faire des mathématiques, il sert aussi à philosopher. L'usage mathématique est algorithmique, pas son usage philosophique. Ça c'est Kant qui l'a prouvé.
Et la physique a tout autant besoin de la philosophie que des mathématiques pour justifier ses premiers principes, à commencer par le principe de causalité, et pour se faire elle ne peut emprunter la méthode algorithmique des mathématiques.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 3 (+1/-0).
Oui, on ne va tout de même pas prétendre pouvoir faire sortir, comme par magie, de notre esprit, des lois de la nature qui ne peuvent être connus que par expérience.
Comme je l'ai dit par analogie avec la programmation, les spécifications, bien que formalisées et constituant une axiomatique du domaine métier, ne peuvent être formulées que par la connaissance expérimentale du dit domaine. Et l'on y retrouve les deux classes de bugs dans les logiciels : non conformité du code avec les spécifications (c'est là que les systèmes de types jouent un rôle), non conformité des spécifications avec le domaine (cela, aucune méthode formelle ne peut les résoudre).
Cela étant, il reste toujours un part d'a priori dans les théories physiques, que l'on ne peut totalement éliminer pour tout ramener à l'expérience. C'est cela que Kant avait formidablement remarqué (on le retrouve dans Curry-Howard) et que Hilbert espérait résoudre via l'axiomatisation de la physique. On le retrouve dans ce passage de l'article :
Pour un kantien, il restera toujours un fond a priori dans les sciences de la nature. Voir par exemple l'exemple des lois de l'electricité par Ampère, décrite dans cette article : La déraisonnable efficacité des mathématiques. Comme dit dans l'article, c'est lié à ce que Kant appelait sa théorie du schématisme, ce qu'exprime à sa façon la correspondance preuve-programme : les preuves sont des programmes, c'est-à-dire des schèmes (en terme kantien), et l'on ne peut s'en passer pour appréhender le réel. J'aime beaucoup les deux citations de Paul Valéry qui sont si kantienne dans l'esprit :
On le retrouve dans la conférence donnée par Stéphane Mallat lors du colloque de rentrée au Collège de France sur l'intelligence artificielle : Mystères mathématiques d’intelligences pas si artificielles. À partir de la quatrième minute, il aborde la théorie de la connaissance et les deux tendances qui s'opposent depuis l'antiquité : rationalisme contre empirisme (Platon contre Aristote). Il évoque plus particulièrement David Hume (empiriste) qui mit en doute la notion même de causalité, et Kant qui vint développer la troisième voie : la méthode critique entre le dogmatisme rationaliste et le scepticisme empirique. Il soutient que l'approche des réseaux neurones tient du kantisme mais ne développe pas trop ses raisons, si ce n'est qu'il y a, aussi, une dimension d'a priori dans les réseaux de neurones.
Mais je veux surtout rebondir sur Hume, la causalité et son rapport à Kant. C'est Hume qui fit sortir Kant de son sommeil dogmatique (l'expression est de Kant lui-même) par son attaque contre le principe de causalité. Et la réponse de Kant fut ce qu'il est convenu d'appeler sa théorie des catégories qui est une correspondance preuve-programme bien avant l'heure : la Critique de la Raison Pure date de 1781 et la dite correspondance de la fin des années 1960. La réponse de Kant à Hume fut celle-ci : le principe de causalité n'est pas d'origine empirique, mais nous l'imposons a priori au réel en conformité avec la forme logique des jugements hypothétiques.
Que voulait-il dire par là ? Faisons un détour par la théorie de la démonstration. Parmi les règles de déduction employées par les mathématiciens, il y en a une bien connue sous le nom de modus ponens :
si A alors B, or A donc B. Et cette règle est celle qui sert à typer l'application de fonction dans les langages fonctionnels (c'est la base de la correspondance de Curry-Howard). Mais cette règle de typage a un principe analogue dans l'analyse formelle des langages impératifs, c'est le cœur de logique de Hoare avec ses triplets de Hoare{P} C {Q}: un programmeCa pour résultat de passer dePàQ. Autrement si ma machine est dans l'étatPalors en éxécutant le programmeC, elle sera dans l'étatQ. Et c'est explicitement ce que Kant avait exposé dans sa table des catégories, via la correspondance entre la table des jugement et la table des catégories. Où l'on voit la correspondance entre les jugements hyptothétiques (si A alors B) et la causalité. Correspondance qu'exprime à leur manière Curry-Howard et Hoare : les programmeurs fonctionnels composent les fonctions, comme les programmeurs impératifs composent les instructions. Et c'est ce lien entre ces deux logiques qui expliquent pourquoi l'on peut automatiser (c'est à dire construire des machines soumises à la causalité) l'exécution des algorithmes et non les exécuter seulement à la main.On retrouve cette correspondance de la logique dans la confrontation même des théories physiques avec l'expérience. La physique pose une loi causale (en arrière plan, il y a la forme logique
si A alors B), constate un étatAet observenon B: il y a contradiction entre le réel et la théorie. Conséquence : soit la loi est fausse, soit l'état A était mal déterminé. Deux exemples issu de de la cosmologie :Là tu te dis peut être : mais what the fuck !? De quel droit peut-on imposer totalement a priori des lois à la nature (non selon le contenu mais selon la forme) sans même les emprunter à l'expérience ? C'est là que Kant et les kantiens répondent en cœur avec l'enfant bouddhiste de Matrix : la cuillière n'existe pas ! :-P Derrière cette boutade, il y a le principe que si l'on voit partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous mêmes. Donc, d'un point de vue expérimentale, la cuillère existe bien, certes, comme objet spatio-temporellement déterminable. Mais si l'on fait abstraction de son rapport à un observateur, et que l'on se demande : cette chose qui nous apparaît sous la forme d'une cuillière, est-elle en elle même dans l'espace et dans le temps, soumise à la causalité… À cela nous répondons : non ! En tant qu'objet d'expérience possible elle l'est, mais abstraction faite du rapport à l'expérience elle ne l'est pas. Il n'y a pas de réalité absolument indépendante de l'esprit humain qui serait objet d'étude de cette science que l'on nomme physique.
Je ne sais pas. Je ne suis pas assez les travaux de physiciens théoriciens pour le savoir, mais il y a de très forte chance qu'il y ait eu des tentatives.
Leur usage du théorème d'incomplétude est parfaitement valide. Ce que je ne comprends pas c'est quand ils arguent l'existence de phénomènes observables, donc dont on peut déterminer la valeur de vérité, qui sont hors du champ de la déductibilité du système : il y a des formules non déductibles, le système étant déductivement incomplet, mais en quoi correspondent-elles à des phénomènes observables ? De mémoire, chez Penrose, c'est le phénomène de réduction de la fonction d'ondes ou réductions du vecteur d'états en mécanique quantique qui l'amène à développer sa notion d'entendement non algorithmique. Mais dans cet article, bien court et peu développé, les principes tombent un peu comme un cheveux sur la soupe. Donc je ne sais quoi en dire, d'autant que je suis loin d'être un spécialiste du sujet. Mais je doute qu'il puisse convaincre ceux qui s'occupent du sixième problème de Hilbert.
Pour finir, avec une remarque quelque peu hors-sujet. Kant ne s'est pas contenté de faire usage de son système pour justifier l'usage des mathématiques en physique et la légitimité de certains principes a priori. Il l'a même étendu à la doctrine du droit et à la philosophie politique. Question : pourquoi nos États sont-ils structurés autour de trois pouvoirs (législatif, exécutif et judiciaire). Réponse :
Autrement dit : nous ne faisons que projeter dans la constitution de nos États la structure formelle de notre propre esprit : raison (législatif), entendement (exécutif) et faculté de juger (législatif).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 6 (+4/-0). Dernière modification le 02 novembre 2025 à 22:05.
Si je peux te donner conseil : conserve précieusement cette maxime, et ne cesse jamais d'en faire usage.
Le même prof qui avait plaisanté sur les sanctifiés du Pape nous avait donné ce principe dès les premières minutes de son premier cours :
Je n'ai jamais hésité à l'interrompre, et il a toujours satisfait à ma requête. Néanmoins, dans le cadre d'une salle de classe, j'ai pu constaté que nombreux sont ceux n'ayant jamais osé (bien qu'il ne comprenait pas), sans doute de peur de passer pour des idiots. Le problème de la peur du regard des autres…
Il faut voir cela avec David Hilbert, c'est son sixième problème.
Le sujet étant long et complexe, j'ai trouvé ce texte en ligne : la portée epistémique de l'axiomatisation de la physique chez Hilbert. Cela reste tout de même un texte très technique qui revient tout d'abord sur l'utilité et la raison d'être de l'axiomatisation pour les mathématiques, avant de traiter de la volonté d'Hilbert d'étendre la méthode à la physique.
Mais sinon, en version plus simple et courte : c'est ce que font tous les programmeurs du monde. Lorsqu'une équipe de programmeurs établit un cahier des charges puis écrit les spécifications du logiciel qu'ils doivent écrire, ils axiomatisent leur domaine métier. Ensuite charge à eux de réifier cette axiomatique, c'est à dire implémenter les spécifications.
C'est là qu'intervient l'utilité pour les programmeurs du domaine de recherche de Jeanas, la théorie des types et la correspondance preuve-programme. Un système de type est un langage dans lequel on peut exprimer ses spécifications, le type checker vérifiant que le code est conforme aux types. Plus le systèmes de types est évolué, plus on peut exprimer finement ses spécifications, et moins il y a de bug (de code non conforme aux spécifications). Et c'est ce qu'on toujours fait les mathématiciens : la preuve d'un théorème est un programme dont l'énoncé est la spécification. Prenons l'exemple du théorème affirmant qu'il existe un nombre infini de nombres premiers. Celui-ci affirme que « pour tout entier
n, il existe un entierppremier et strictement plus grand que n ». Toute preuve de ce théorème est un programme qui prend en entrée un entiern, et renvoie en sortie un entierppremier et plus grand que l'entrée. C'est cela la correspondance de Curry-Howard ou correspondance preuve-programme (toute preuve mathématique a un contenu algorithmique, est un programme). Vérifier qu'une preuve est logiquement valide (elle respecte bien les règles de déduction et les axiomes de la théories) ou vérifier qu'un programme est bien typé, c'est tout un ! Un vérificateur de preuves ou un type checker, c'est le même logiciel.Sur le sujet, il y a ce texte bien plus abordable à lire et comprendre que le premier (je te le conseille pour commencer): À propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court). L'auteur est aussi un de mes anciens professeurs, celui qui m'initia à ce domaine de la logique. Il est l'auteur d'une machine abstraite La machine de Krivine dont le but était d'interpréter les preuves de théorèmes comme des programmes. Elle est proche, dans son fonctionnement, à la première machine abstraite qui interprétait le bytecode du langage OCaml (la ZINC).
Sinon, pour revenir à de la programmation de tous les jours : utiliser un types primitif d'un langage, c'est poser une axiomatique (tout ce que le langage fournit sur ce type est une axiomatique); programmer contre une classe abstraite, c'est poser une axiomatique (celle décrite par l'interface de la classe); utiliser des interfaces en golang, c'est faire de l'axiomatique (celle décrite par l'interface); utiliser des traits en Rust idem, des types classes en Haskell idem, des foncteurs en OCaml idem… Je n'ai jamais croisé un développeur de ma vie qui ne faisait pas de l'axiomatique sans le savoir (à la manière de monsieur Jourdain).
Enfin, c'est pour cela que je suis sur un site dédié aux logiciels libres : de même qu'une preuve mathématique se doit d'être publique, un code doit l'être; conceptuellement ce ne sont pas deux types d'objets distincts, mais les deux faces d'une seule et même pièce.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 4 (+2/-0).
Donc c'est plus en lien avec la théorie de la démonstration et la correspondance de Curry-Howard ou correspondance preuves-programmes. Tu es plus du côté informatique (systèmes de types pour les langages de programmation) ou mathématique (HoTT, interprétation des preuves comme programmes, logique classique ou intuitionniste) ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 3 (+1/-0).
Ce jugement semble ne pas avoir été apprécié par un membre du site, à en juger par ma note.
À la même époque, d'autres physiciens (Sokal et Bricmont) reprochaient à certains philosophes français leur usage saugrenu de l'incomplétude de Gödel.
L'un n'empêche pas l'autre. Notre connaissance peut être bornée quant aux contenu du monde (bornée par ce qu'il reste encore à découvrir) mais nous pouvons être en mesure de déterminer les limites du savoir humain (ce que font les méthodes formelles). Kant avait une belle image pour illustrer cela : je peux ignorer le contenu effectif de la surface du globe (il faudrait pour cela en avoir parcouru la totalité) tout en sachant qu'il est circonscrit dans des limites données que je peux déterminer (je n'ai pas besoin de le parcours pour connaître sa circonférence).
Cela étant j'ai fini par lire l'article est je suis moins catégorique que Jeanas sur son contenu : ce n'est pas du Régis Debray. La thèse principale n'est pas tant que nous ne vivons pas dans une simulation, mais qu'une théorie du tout qui unifierait la relativité générale et la physique quantique n'est pas axiomatisable. En résumé : la physique n'est pas axiomatisable. Ce qui a pour corrolaire que l'univers n'est pas une simulation d'ordinateur.
Dans l'ensemble, bien que je souscrives personnellement à ces thèses métaphysiques, leur argumentaire ne me convainc que moyennement. D'une part parce que je doute que la méthode mathématique soit la seule à même de traiter ces questions. D'autre part, parce que l'article consiste à formaliser la thèse de Roger Penrose d'entendement non algorithmique (non algorithmic understanding), thèse qu'il développe par exemple dans son livre Les deux infinis et l'esprit humain. Cette thèse me semblait pas très claire à l'issue de ma lecture du livre, et l'article ne change pas la donne dessus.
Ils font effectivement usage des deux théorèmes de Gödel que j'ai évoqué dans mon premier commentaire. Tout commence à la troisième page de l'article, lorsqu'il suppose une axiomatisation de la physique en supposant l'existence d'un système formel
, dont la signification doit vouloir dire : Formalisation of Quantic Gravitation. Il font sur le système des hypothèses raisonnables : logique du premier ordre, ensemble d'axiomes récursivement énumérables, système complet de règles d'inférence. À dire vrai, ces derniers hypothèses n'en sont pas, c'est la définition même de la proposition « la physique est axiomatisable ».
À cela ils ajoutent deux contraintes :
On peut bien leur accorder la première, la physique théorique ayant besoin de l'arithmétique. C'est celle-ci qui leur permet de faire usage du théorème d'incomplétude : le système axiomatique étant une extension de l'arithmétique de Péano, il est déductivement incomplet.
Mais ensuite, je dois avouer avoir du mal à les suivre dans leur pensée. Ils semblent jongler entre syntaxe et sémantique : il y aurait des énoncés observables, et donc vrais (théorie de la vérité correspondance, sémantique de Tarski), dans l'univers (cf. deuxième contrainte), mais qui ne seraient pas conséquences déductives du système d'axiomes (que l'on pourrait obtenir à partir des axiomes de l'ensemble Sigma et des règles R). Peut être bien, mais lesquelles ? C'est à partir de là qu'ils introduisent leur méta-théorie non algorithmique, leur entendement non algorithmique à la Penrose et qu'ils me perdent. Non que ce genre de méta-théorie ne soient pas considérées par les logiciens mathématiciens (en théorie des modèles, on étudie bien les modèles non standard de l'arithmétique, des théories non récursivement énumérables voir même non dénombrables), mais je ne comprends pas selon quels principes ils l'introduisent ni la justifient.
Cela me rappelle une blague de notre professeur de théorie des modèles, lorsque j'étais étudiant en DEA de logique mathématique et fondements de l'informatique. Il faut faire attention, ici, que le mot modèle est un homonyme de celui utilisé en physique (bien qu'il y ait des rapports entre les deux). Pour un théoricien des modèles, à la question qu'est-ce qu'un groupe ? Il répond : un modèle de la théorie des groupes, c'est à dire une structure qui satisfait à l'axiomatique de la théorie.
Trève de digression et revenons à sa blague. Un jour, en début du cours, il nous tint à peu près ce discours : « je lisais ce matin dans le Monde que la pape Jean Paul II avait sanctifié plus de personnes que tous ces prédécesseurs réunis. Sachant que, durant ces 20 dernières années, on a publié plus d'écrits mathématiques que durant toute la période de l'humanité qui précède, si un jour vous publiez un article insignifiant, vous pourrez vous considérer en bijection avec un sanctifié du pape ! ».
Je dois admettre, après lecture de l'article, que je ne sais quoi dire sur le statut de sanctifiés de ses auteurs.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 4 (+3/-1). Dernière modification le 31 octobre 2025 à 23:12.
Quand je vois ce genre de titre, je n'ai même pas envie de lire l'article. Ce n'est pas la première fois, ni la dernière, que l'on fera dire n'importe quoi aux théorèmes de Gödel. Mais même si les physiciens s'y mettent, on n'est pas sorti de l'auberge.
De toute façon, comme je suis kantien, la question n'a même pas de sens pour moi : comme dit le petit enfant boudhiste dans le premier Matrix, « la cuillère n'existe pas ». :-P
Tu fais une thèse en théorie de la démonstration ? ou en calculabilité ? C'est là où j'y vois trois résultats fondamentaux :
Théorèmes qui ne font que confirmer le cœur de la philosophie kantienne, et l'inexistence de la cuillère.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: La fin de la bulle ?
Posté par kantien . En réponse au lien IA - Le pari de Sam Altman est-il voué à l’échec ? . Évalué à 2 (+0/-0). Dernière modification le 17 août 2025 à 18:42.
Au delà de prendre les chiffres pour argent comptant, je vois ce que cela donne chez moi. En mai, pendant que je préparais ma terre, mon voisin se plaigner du manque d'eau, alors que, hormis le premier centimètre, mon sol état noir et gorgé d'eau.
Cherche un peu sur la chaîne agriculture vivrière et tu pourras constater la différence de structure entre deux terres à peine séparées de quelques dizaines de mètres (ce n'est pas chez moi, mais l'idée est la même). ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: La fin de la bulle ?
Posté par kantien . En réponse au lien IA - Le pari de Sam Altman est-il voué à l’échec ? . Évalué à 2 (+0/-0).
Oui, je le sais. Hervé Coves traite des solutions du dernier rapport du GIEC dans un série de vidéo sur le thème « Le carbone, c'est la vie ».
Sur cette article c'est une petite expérimentation (petite ferme en maraichâge). Mais il y a eu des expérimentations à plus grandes échelle en Suisse (canton de Vaud), où ils dépassent de loin l'objectif du 4 pour mille. Et dans la série de vidéos donnée au dessus (journée de conférence), il y a une usine de production de pop corn qui avance un bilan carbone bénéfique (elle séquestre plus de carbone qu'elle n'en émet), avec encore de la marge de manœuvre : 80% des terres sont en non labour (il reste 20% de marge de manœeuvre) et ils travaillent à la réduction sur le transport.
Ça nécessite un changement de pratique, qui ne sera certainement pas facile à mettre en place : cela nécessite une remise en cause de 10_000 ans de pratiques agricoles. Il est sûr que cela ne se fera pas du jour au lendemain.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: La fin de la bulle ?
Posté par kantien . En réponse au lien IA - Le pari de Sam Altman est-il voué à l’échec ? . Évalué à 1 (+0/-1).
Où alors, un des leviers d'actions est le recul d'usage de la technologie. Si nos agriculteurs rengeaient leurs tracteurs pour arrêter le labour, ils pourraient stocker dans le sol nos émissions annuelles, voir plus. Adopter les méthodes de sol vivant pour inverser son bilan carbone.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: critique (trop) sévère?
Posté par kantien . En réponse au lien critique de l'audition de Luc Julia par la commission sénatoriale sur la chaîne de Mr Phi. Évalué à 4 (+6/-4). Dernière modification le 15 août 2025 à 14:40.
Je n'ai pas regardé la vidéo, donc je ne préjugerais pas des aptitudes de Luc Julia. En revanche mon expérience passée sur Mr Phi m'a amené cette conclusion : je ne doute pas de ses aptitudes en mathématiques, il n'en a aucune, et pour la philosophie, il est comme nombre des personnes formées à l'école française : s'il a une tête bien pleine (histoire de la philosophie), il n'est pas certain qu'elle soit bien faite. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Inédit pour les métiers qualifiés
Posté par kantien . En réponse au journal Coder avec l'IA : le déclin du plaisir. Évalué à 0 (+0/-2).
Oui ça doit être cela, tu ne comprends pas sa sociologie des sciences. Je ne crois pas que celà ait beaucoup évolué depuis son époque, si ce n'est la hausse de volume de cette catégorie :
Et d'ailleurs, dans ton commentaire, tu décris très bien ce que cette catégorie apporte au bon fonctionnement du système.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Inédit pour les métiers qualifiés
Posté par kantien . En réponse au journal Coder avec l'IA : le déclin du plaisir. Évalué à 0 (+0/-2). Dernière modification le 14 août 2025 à 11:49.
Qu'est-ce qui t'ennuis dans ce texte (tronqué, la suite et bien plus inintéressante) ? Le fait que, malgré ton doctorat et ta carrière de chercheur, certaines personnes te considèrent comme une être secondaire ? tu as une revanches à prendre sur la vie ?
Elle est celle de ceux qui, comme pierre essentielle, font la Science. (Je n'en fait pas, moi même partie, mais mon intellect a besoin de ces personnes hors normes pour se nourrir).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Inédit pour les métiers qualifiés
Posté par kantien . En réponse au journal Coder avec l'IA : le déclin du plaisir. Évalué à 2 (+0/-0). Dernière modification le 13 août 2025 à 23:24.
Demandons donc son avis à Einstein sur la question du savoir et de la science.
Mon avis sur la question, qui marche dans les pas d'Einstein, est celui-ci : l'ange de Dieu se retrouve, de nos jours, avec un critère infaillible : ceux qui sont remplaçables par un automate n'aurait jamais pu édifier et ne contribuerons que marginalement à l'édification du temple de la Science. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Démarche intéressante
Posté par kantien . En réponse au lien La pétition contre la loi Duplomb a obtenu plus de voix que Pécresse au 1er tour de la pres.. Évalué à 2. Dernière modification le 03 août 2025 à 02:23.
Je n'ai pas insisté sur mon message précédent. Mais crois tu vraiment aux coccinelles comme solutions miracles contre les pucerons ? Et produis-tu ta nourritures ou contes tu sur autrui pour le faire à ta place ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Démarche intéressante
Posté par kantien . En réponse au lien La pétition contre la loi Duplomb a obtenu plus de voix que Pécresse au 1er tour de la pres.. Évalué à 2.
Certes un doctorat biochimie n'est pas nécessaire, mais déjà se nourrir soi même devrais pauser des questions (et si on le pratique, le coup des coccinelles fait rire jaune).
Personnellement; je produis plus de 50% de ma nourriture végétale (sans pesticides, en mode maréchal sur sol vivant ;-) Et, honnêtement, bien que je souhaites les changements de pratiques, je ne suis pas sûr que cela puisses se faire du coq à l'âne.
Si notre espoir est celui-là :
le chemin est celui là :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 2.
Soutiens-tu que la notion de vérité est vide de sens et qu'en conséquence il ne peut exister de science (quelque soit son objet d'étude) ?
Là tu accordes qu'il existe un savoir, et donc une véritié des propositions qu'il contient. Mais alors penses-tu que les critères de vérités des mathématiques sont fondées sur l'expéreince ? Si c'est le cas, sache qu'aucun mathématicien au monde ne te l'accordera. ;-)
Alors, il reste la question d'où vient ce savoir : il est codé en dure dans notre faculté de savoir, l'expérience est l'occasion pour nous de le mettre en action et c'est lors de cette mise à l'épreuve que nous en prenons conscience.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 1. Dernière modification le 25 juin 2025 à 00:30.
Après réflexion, j'appelle cela une non réponse. Ma question était pourtant simple : comment une science qui ne prend pas ses critères de vérités sur l'expérience, peut elle être utile pour la connaissance expérimentale ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 2.
La question n'était justement pas rhétorique, je peux justifier mon point de vue. Malheureusement, cela sera très absrtait, et si je dois rendre accessible la réponse au commun des mortels (comme laisse sous entendre le reste de ton commentaire), je crains que mes capacités de vulgarisation ne soient pas au niveau.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 2. Dernière modification le 24 juin 2025 à 23:29.
Effectivement, ce n'est pas ce que j'avais en tête, et seule l'expérience peut trancher cette question.
Ce que j'ai en tête, c'est par exemeple la correspodance de Curry-Howard enseignée par Xavier Leroy au Collège de France, enseignement qui n'est rien d'autre qu'une version simplifiée de ce Kant a développé dans la Crititique de la raison pure.
Alors, après je pourrais toujours montrer en quoi Einstein a suivi ces principes. La question est dois-je le faire ? (Comme la réponse est longue, il ne faudra pas s'étonner si elle prend du temps).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 2.
Je ne te le fais pas dire. La vie de Grothendieck sue radio france en donne une idée.
Mais il reste, tout de même, que bien qu'en tant que mathématicien on ne prend pas l'expérience comme juge de paix de la vérité de nos jugements, les physiciens n'ont pas d'autre choix que d'utiliser notre langage. Mais alors, pourquoi ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 0.
Oui, mais ça ne change rien au fondement de ma thèse. Les critères de vérités des mathématiques pures ne sont pas fondés sur l'expériences, néanmoins elles n'ont pas d'autres usages qu'expérérimental (d'où les maths applis, où l'on envoie les moins bons étudiants).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 1.
C'est récurrent chez Barmic. Depuis qu'il a découvert le concept de biais, il en voit partout chez ses interlocuteurs, mais jamais chez lui. Va comprendre !
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 2.
Cherche un directeur ou une directrice de thèse qui accepteront de t'encadrer pour soutenir une thèse mathématique qui serait fondait sur l'observation du monde (j'ai bien dit une thèse de mathématique, pas de physique théorique). Si tu en trouves un ou une, je te tire mon chapeau. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: bof
Posté par kantien . En réponse au journal [HS] La comédie Grok versus Musk/MAGA. Évalué à 2.
Il suffit de regarder les outils dont à besoin un mathématicien pour travailler : un tableau et un craie, ni plus, ni moins. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.