Ecouter les inquiétudes

Une émission au sujet de l'ia avec pour intervenants côté mathématiques : Isabelle Gallagher, François Charles (ainsi que Hugo Duminil-Copin ou Cédric Villani dont il est question dans les reportages de l'émission) lien
Il est question de ce dépôt de 719 preuves en 372 familles (la moitié ?), le readme est là lien. Déjà, il est question de l'invalidation de 3 documents pendant l'émission. En les cherchant, l'ia gemini dit que l'historique est là : lien et en bas de la page de l'historique, on lit
"Additional Formalizations : We have added an additional 6 formalizations and 5 other additions covering supporting results. This brings the total percentage of top-line results formalized to 300 / 719 = ~42%".
300/719, ça semble être celles qui ont été aussi démontrées en Lean, peut-être, avec mathlib, le répertoire qui contient déjà un certain nombre de théorèmes existant des mathématiques.
HDC dit qu'il en a pleuré (il pense que de nombreux axes de ses recherche ont été détruits) : dans la liste qu'il avait montrée dans cette vidéo lien, apparaissait le mot Heisenberg. Alors j'ai cherché par une autre ia pour voir si... Et l'ia a produit ça lien
Les concours de biceps (pour rester respectueuse) sont à la mode alors !
Je n'utilise que les versions gratuites : deux d'entre elles m'ont dit ce que j'avais consigné là : lien Voir aussi là lien ou là lien ou là lien ; ça permet d'avoir un peu moins peur, un peu.
Anecdote : 012. Independent largest prime factors of consecutive integers. Resolves the Erdős–Pomerance joint Dickman conjecture: the logarithmic sizes of the largest prime factors of 𝑛 and 𝑛+1 are asymptotically independent in ordinary natural density. In particular, the integers satisfying 𝑃⁺(𝑛) < 𝑃⁺(𝑛+1) have density 1/2. Pour moi, deux nombres entiers consécutifs n'ont jamais de facteurs premiers en commun, c'est vous dire si je n'y comprends tchi.