Thomas🪴

www.youtube.com/watch?v=J54P...

Dans cette vidéo j'aborde le lemme de Kőnig (faible), des considérations de calculabilité autour de ce lemme et la construction de l'arbre de Kleene. Le lemme de Kőnig est fondamental en mathématiques à rebours, étant utilisé dans différents théorèmes en analyse. www.youtube.com/watch?v=2ox9...

Ceux qui prétendent que les gens sont tous pareils face aux maths sont aussi énervants que ceux qui prétendent que les maths seraient inaccessibles au « commun des mortels ». J'ai du mal à comprendre pourquoi les gens se polarisent autant sur ces questions.

(Enfin si je vois, c'est car les gens font de la politique, mais c'est pénible...)

Ceux qui prétendent que les gens sont tous pareils face aux maths sont aussi énervants que ceux qui prétendent que les maths seraient inaccessibles au « commun des mortels ». J'ai du mal à comprendre pourquoi les gens se polarisent autant sur ces questions.

Est-ce que les gens qui râlent parce que HAL met à disposition un MCP sont les mêmes qui disent « L'IA cite mal les références des articles » ?

Cf mathstodon.xyz/@hal_fr@soci... pour les râleries

Cette politique de Lean (ne pas chercher à être minimaliste dans les axiomes utilisés) me semble très discutable alors que les gens s'interrogent sur les axiomes utilisés dans la preuve du th. de Fermat générée par IA.

Un truc pénible pour quelqu'un qui s'intéresse aux sciences en amateur comme moi : je n'ai pas souvent de créneaux pour lire un bouquin en entier de façon approfondie. Généralement c'est pendant les vacances. Mais du coup si j'en lis un qui ne correspondait finalement pas à ce que j'attendais...

J'essayais d'apprendre des choses sur les sémantiques dénotationnelles du lambda-calcul avec Claude et, rapidement, je me rends compte qu'il me raconte n'importe quoi; ce qu'il finit par remarquer après que je l'ai mis devant sa contradiction.

C'est un scénario qui m'arrive très fréquemment depuis que je l'utilise pour apprendre des choses scientifiques, dès que ça sort des sentiers battus (et encore là ce sont des choses enseignées en Master).

Je me demande quel est le ratio moyen entre la taille des définitions nécessaires à l'énonciation d'une proposition et la taille de la preuve; en particulier dans le cadre des preuves formalisées. Un cas extrême :

Dans ce cas, si on veut s'assurer que je n'ai pas fait d'erreur d'énoncé, il suffit de relire P, ce qui est relativement simple. Mais prenez par exemple les résultats de calculabilité dans Mathlib, dont j'ai déjà parlé ici, ils supposent une formalisation des fonctions récursive, etc.

Je me demande quel est le ratio moyen entre la taille des définitions nécessaires à l'énonciation d'une proposition et la taille de la preuve; en particulier dans le cadre des preuves formalisées. Un cas extrême :