LaurentClaessens a écrit 327 commentaires

Mais il n'y a pas d'intelligence. Aucune.

Défi du jour.

Pondre une définition de «intéligence» qui satisfait à :

1. les IA ne sont évidemment pas intelligentes
2. les humains, les chevaux, les abeilles[1] sont évidemment intelligentes
3. que ladite définition n'aie pas l'air d'être inventée exprès pour satisfaire les critères 1 et 2.
4. la définition doit être tellement fondamentale que c'est évident que dans 5 ans, le point 1 sera toujours valide.

À part ça, les IA nous forcent sans doute à repenser le concept d'intelligence en excluant la conscience. Peut-être que la propriété «être intelligent» est indépendante de «être conscient» [2].

[1] pas les chats hein; faudrait pas déconner non plus.
[2] étant donné que je suis le seul être de l'univers à n'être ni un zombie philosophique ni un cerveau de Boltzmann, ce dernier point n'est pas tellement important.

Résumé de la vidéo pour celles qui n'ont pas envie de prendre 30 minutes juste pour savoir si ça les intéresse.

1. Paul Erdős est un mathématicien mort en 1996 qui a laissé derrière lui énormément de problèmes ouverts. Des conjectures.

2. Il y a un site qui liste les différents problèmes que Erdős a posé un peu partout dans sa vie : dans des lettres, des articles, des discussions, etc.

3. Il y a 6 mois, un de ces problèmes a été résolu par IA. Mais fausse alerte. En fait une solution était déjà disponible sur internet. Il se fait que la personne qui l'avait résolu et publié la démonstration ne savait pas que c'était un problème de Erdős. Il était non listé sur le site.

4. Un peu plus tard, une IA démontre un des problèmes. Preuve validée par des humains.

5. Des gens disent «oui, mais ce problème-là était facile, pas important, peu de mathématiciens l'avaient essayé, etc.»

6. Des mathématiciens publient une liste des 10 problèmes de Erdős qui sont à la fois difficiles et importants.

7. Un de ces problèmes a été récemment résolu.

Donc cette fois, on a réellement un problème ouvert, reconnu comme étant difficile et important qui a été résolu par IA.

La preuve trouvé n'est pas incroyablement compliquée.
La raison pour laquelle les humains ont raté la preuve ?

1. Erdős était persuadé que sa conjecture était vraie. Donc les mathématiciens ont essayé de la prouver. En réalité elle était fausse et l'IA a trouvé un contre-exemple. Les humains étaient donc biaisé par leur confiance en Erdős.

2. La preuve fait intervenir des mathématique, certes classiques, mais d'un domaine totalement différent de celui d'où provient le problème. Pour trouver le contre-exemple, il aurait fallu qu'un mathématicien qui :

   • soit expert des deux domaines en même temps
   • soit prêt à passer du temps sur ce problème

Bref, ce qui a donné un avantage à l'IA est

1. une bonne intuition qu'il fallait chercher un contre-exemple plutôt qu'une preuve "positive".

2. une connaissance simultanée des résultats "classiques" de toutes les branches de la mathématique

3. la patience qu'il faut pour tester des centaines de voies qui ratent pour tomber sur celle qui marche.

Voila voili voilou.

Comme ça vous savez à peu près de quoi ça parle.

Note : en général Monsieur Phi est très bien. Et il a beaucoup de bonnes vidéos sur l'IA.

La spécificité d'une croissance exponentielle est que la vitesse de croissance est proportionnelle à la valeur de la fonction.

C'est pour cela qu'on a souvent des exponentielles dans les taux d'équipements quand il y a un effet de réseau : l'envie de posséder (et donc le nombre de nouveaux clients) est proportionnelle au nombre de personnes déjà équipées.

Une fonction puissance est quand tu fais x-> x^2.
Une fonction exponentielle est quand tu fais x -> 2^x

Pour calculer avec x=6, pour le premier tu fais par exemple 6*6 = 36
Pour le second tu fais 2⁶ = 2*2*2*2*2*2 = 64

J'en profite pour une autre de mes marottes.

Quand on choisit un mot de passe de longueur l dans un alphabet de N caractères, il y a

N^l

possibilités.

C'est donc polynomial (puissance) en la taille de l'alphabet, mais EXPONENTIEL (et là la définition correcte du mot est requise) en la taille du mot de passe.

Or les exponentielles croissent plus vite que les polynômes.

Donc il vaut mieux un mot de passe LONG qu'un mot de passe qui puise dans un large alphabet.

Par exemple, un mot de passe de 12 caractères avec rien que des lettres minuscules est plus fort qu'un mot de passe avec 8 caractères lettres+majuscules+chiffres+caractères spéciaux (tout mélangé).

Mes mots de passe sont toujours 40 lettres minuscules auxquelles j'ajoute ".1A" pour faire plaisir.

Une raison de n'utiliser que des lettres minuscules est qu'en cas de problèmes, si il faut rentrer le mot de passe sur un clavier qu'on ne maîtrise pas le moindre ~ tue.

mais il désigne aussi une croissance rapide. C'est ce second sens qui est utilisé la plupart du temps, et ce n'est pas incorrect du tout :).

C'est comme dire que le mot «logiciel libre» a un sens en informatique (4 libertés tout ça), mais que ça désigne aussi un logiciel gratuit. C'est ce second sens qui est utilisé la plupart du temps, et ce n'est pas incorrect du tout :).

Si les mots «gratuits» et «libres» existent, c'est pour pouvoir les utiliser à bon escient. Si les mots «rapide» et «exponentiel» existent, c'est pour la même raison.

Cela soit dit en passant, dans le commentaire initial de patrick_g,

C'est fou comme c'est rigolo les exponentielles.

le mot exponentiel n'était même pas utilisé pour répondre à un commentaire qui parlait de «croissante rapide», ni même croissance vers l'infini, mais simplement une croissance qui ne s'arrête pas.

Bref. ok, c'est un sujet sur lequel je m'irrite facilement.
Déso pour le bruit.
J'essaie de me limiter à un commentaire rageux par an contre l'usage du mot «exponentiel». C'est important pour ma pression sanguine :)

la qualité de l'IA ne fera que progresser sans jamais connaitre de fin

Si on extrapole la hauteur future d'un bambou à partir de sa croissance actuelle on trouve qu'elle doit atteindre la Lune au bout de quelques mois non ?
Et que la masse des bébés, si la aussi on extrapole, doit atteindre le million de tonnes en quelques années.
C'est fou comme c'est rigolo les exponentielles.

Il y a parfaitement moyen de progresser sans jamais connaître de fin tout en restant borné, et très à fortiori sans être exponentiel.

Par exemple la suite
0, 0.1, 0.11, 0.111, …
elle est strictement croissante, ne s'arrête jamais et n'arrive même pas à 0.2.

"We don't even have enough data to show our progress has been exponential up till now. Instead it's more like the series [1, 2, 4, 8] and everyone's assuming the next several numbers are 16, 32, 64, when they could easily be 9, 10, 10.5, 10.6, 10.65, etc. Like we're on a curve that could easily be an S curve that's turning logarithmic but because we haven't seen the inflection point yet, we assume it trends to infinity".

Une des premières fois sur internet où je vois le mot «exponentiel» utilisé correctement. Ça vaut la peine d'être mentionné :)

Énorme disclaimer dans le readme du projet

À mon très humble avis, une description de la façon dont l'IA est utilisée dans un projet devrait être dans un fichier à part.

Perso j'écris ça dans un fichier nommé ai_usage.md.

Si l’attaquant (ou l’attaquante) n’a cure de tes précieuses données (ce qui est probable), mais souhaite plutôt devenir, à bon compte, administrateur ou administratrice de ta machine (tout en agissant en ton nom), alors la faille le lui permet. Si ça t’est indifférent, alors tout va bien, laisse donc ton noyau tranquille.

En pratique, tu penses à quoi ?

Que peut faire root sur ma machine que mon utilisateur ne peut pas déjà faire ?
Je doute que les programmes utilisés par les botnet s'installent avec des apt get—qui nécessite les droits root.

Cette faille permet, si je comprends bien de passer de l'utilisateur courant à root sans entrer de mot de passe.

Les vrais trucs que je veux protéger sont dans ma home (documents, photos, mails, etc.).

Mon ordinateur est une tour bien lourde sous mon bureau connectée à plein de fils (on ne risque pas de me le voler allumé).

Quelle est la surface d’attaque ?

Un de mes enfants pourrait profiter d'une absence pour se créer un accès permanent à mon ordi ?

xkcd obligatoire: https://xkcd.com/1200/

Le seuil de sécurité est une limite faite pour protéger les consommateurs, ce n'est pas un objectif optimal à atteindre.

Je double-plussoie.
Parce que un seuil doit être pensé de façon à pouvoir être dépassé sans danger.
Il y a toujours un moment où tout va aller mal en même temps : une mauvaise décision prise juste au moment où la météo ne va pas et que par malchance le responsable est en vacances.

Si on veut éviter 10, il ne faut pas mettre le seuil à 9.9, mais à 5.

Corollaire : Si on veut éviter 10 et qu'on met le seuil à 5, le jour où tout va mal et qu'on arrive à 7, on a la confirmation que le seuil était bien pensé. Par contre il ne faut pas se dire (en tout cas pas automatiquement) « on va mettre le seuil à 3 pour éviter de dépasser 5 ».

Pour info, le texte du lien ne parle pas de nuage arrêté à la frontière.
Tu déserts l'information en la présentant avec un cliché connu pour être complètement faux.

C'est comme si tu écrivait 1+1=4 en donnant comme source la page wikipédia sur l'arithmétique.

Si en tout on remarque que, malgré l'effet d'accumulation, le nombre de victimes de myrtilles est moindre que le nombre des chutes de toits, on doit être bon.

Quoi qu'il en soit mon point n'est pas d'absolument comparer l'un et l'autre, mais de faire remarquer que :

1. Le problème soulevé est le seuil, pas le panachage.
2. Si on veut baisser les seuils, il faut quand même se donner une limite raisonnable.

Si on accepte que X personnes meurent en tombant d'un toit sans demander qu'on augmente la sécurité des travailleurs, alors il n'y a pas de raisons si évidentes de se choquer que X personnes meurent en mangeant des myrtilles ukrainiennes.
C'est juste une analogie pour donner une notion de "seuil raisonnable". Sinon on peut utiliser l'équivalent banane. On peut demander que la radioactivité (mesurée en Sv) d'un panier de fruits doit toujours être au max la radioactivité d'un panier de bananes bio de même poids.

Si tu as d'autres idées de comment définir un seuil raisonnable, mes oreilles sont grandes ouvertes. Ne dis juste pas "zéro" ;)

Bref, avant de parler de baisser les seuils, il faudrait discuter ce qu'on entendrait par un seuil "raisonnable".

Le risque est le même, mais dans un cas (ou tu as une myrtille très radioactive au milieu d'autres qui ne le sont pas), il aurait pu être éliminé complètement (en triant et en ne commercialisant pas du tout les myrtilles contaminées, plutôt que de les mélanger aux autres).

Ok. Donc si je comprends bien le problème n'est pas d'être capable de respecter le seuil en panachant deux types de myrtilles. Le problème est le seuil.

Ce que tu demandes réellement est de baisser le seuil. Ça peut être argumenté; je n'ai rien contre. Mais il faut bien le dire en ces termes et non camoufler «il faut baisser le seuil légal» en «il faut interdire le panachage». Explicite est mieux que implicite.

Mais attention toutefois qu'il ne faudrait pas mettre des seuils tellement bas qu'il deviendrait plus efficace de mettre des règles sur la formation en escalade des poseurs de panneaux solaires sur toits : dès qu'on remarque qu'il y a plus d'installateurs de PV qui meurent en se cassant la binette en tombant d'un toit que de personnes qui meurent des myrtilles ukrainiennes, je crois qu'on peut dire que le seuil est bon. (ou alors je commencerais à soupçonner que ce que l'auteur a vraiment dans dans la tête n'est pas un soucis de santé publique mais autre chose)

La vraie information est qu'on peut mélanger des myrtilles trop
radioactives avec d'autres qui ne le sont pas si on reste en moyenne sous les seuils.
Personnellement ça me choque.

Est-ce vraiment un problème ?

Est-ce qu'il y a une différence entre :

A. un panier contenant 1 myrtille de 0Bq et 1 myrtille de 10 Bq
B. un panier contenant 2 myrtilles de 5Bq ?

Je prends un panier A, je presse les myrtilles en bouillie A.
Je prends un panier B, je presse les myrtilles en bouillie B.

Maintenant je te donne un verre de bouillie A et un verre de bouillie B.
Comment peux-tu savoir lequel est lequel ? Quelle mesure/expérience tu peux mener pour les distinguer ?

M'est avis qu'en mangeant l'un ou l'autre des deux paniers, on prend le même risque.
Après tout, si deux atomes se désintègrent dans mon estomac, mon ADN ne va pas savoir si ils viennent tous les deux de la même myrtille ou de deux myrtilles différentes.

Ou alors il y a quelque chose qui m'échappe ?

un moteur, cinq sièges, quatre roues,

Pourquoi cinq ?
Un seul siège couvre le besoin «tu comprends j'ai pas le choix j'en ai besoin pour aller au boulot».
Deux sièges suffisent pour le besoin «je dois amener mon enfant au foot».
Quatre sièges suffisent pour le besoin «j'ai trois enfants».

Boutade à part, je suis tout à fait d'accord avec ton commentaire.
Mais pour la curiosité je pose quand même la question : pour quel besoin on a réellement besoin de plus que 2 places ?
Et est-ce que ces besoins concernent vraiment beaucoup plus qu'un automobiliste sur 5 ?

Le mien est mieux que he-she (même pas honte) parce que le mien n'est pas réellement aléatoire.

Ma macro regarde la parité de "page + numéro du dernier théorème". Grâce à ça je peux faire

\randomGender{Le lecteur}{La lectrice} peut faire la
 démonstration \randomGenger{lui}{elle}-même.

Et je sais que les deux \randomGender sélectionneront le même.
Du coup ma macro n'est pas cryptographiquement sure.

Et maintenant que je le dis, je crois que ce serait mieux de faire "numéro du chapitre + numéro dernier théorème".

forcément, si tu prends une fonction non continue en 0 — définie par \forall x \in \mathbb{R}^* , f(x)=0 et f(0)=1 — il vaut mieux connaître la différence entre les deux définitions possibles de limite… Tu attendais de l'IA une précision par rapport à Bourbaki ?

Je vais tenter de ne pas troller sur ce sujet maintenant, mais ça me brûle les doigts.

Ce que je voulais dire est qu'un étudiant français (qui a la limite pointée dans son cours) risque de se faire avoir si il demande des choses à l'IA parce que la limite pointée est complètement inconnue en-dehors du microcosme de l'enseignement en France. Tellement qu'elle est inconnue de l'IA.
La différence entre la limite pointée et épointée fait partie de ces choses que les étudiants ignorent d'ignorer (contrairement à leurs formules de trigono qu'ils savent ignorer).

Et le pire est que l'étudiant n'aurait aucun moyen de se rendre compte que l'IA lui dit des fautes (par rapport à la définition de son cours) parce que le plus souvent le prof ne prévient pas ses étudiant que la définition donnée en France est TRÈS minoritaire par rapport à la définition .

Mon point était surtout de dire que, si on veut utiliser de l'IA pour faire des math, il faut vraiment avoir le niveau parce que l'IA peut poser des pièges inattendus.

Bref. Je vais réviser ma copie parce que je n'ai manifestement pas été clair. Merci.

HS : en fait, j'aime bien ton écriture mathématiquépicène (et les mots-valises qui se prononcent), faudrait proposer de l'ajouter en 7. à https://fr.wikipedia.org/wiki/Wikip%C3%A9dia:%C3%89criture_%C3%A9pic%C3%A8ne (vu que les 5. et 6. ont tendance à m'horripiler :/)

Moi, je ne vais pas le faire parce que ce serait assez prétentieux de ma part. Par contre si quelqu'un d'autre le faisait, j'en mourrais d’orgueil et de vanité :)

Mais pour être honnête, je crois que je suis le seul à faire de l'écriture inclusive "en moyenne". Ça ne vaut pas mention sur Wikipédia :(

Ça veut dire quoi "contribution par IA" ?

C'est la question à 1000 blingzons ça.

Comme je le disais ailleurs, je crois que chaque projet devrait avoir son ai_usage.md décrivant le niveau d'implication de l'IA dans le projet.

Ça donnerait des indications aux éventuels contributeurs.

Et d'ailleurs ça devrait également être valable pour les musiciens, dessinateurs, écrivains et vidéastes.

Personnellement ça ne me dérange pas du tout d'écouter de la musique générée par IA, mais je sais qu'il y a des gens qui se sentiront trahis le jour où ils apprendront que leur chanson préférée qui a gagné l'Eurovision aura été générée par l'IA[1].

Avoir un petit ai_usage.md permettrait de clarifier les choses.

[1] Jeu concours : à quelle cote prenez-vous le pari que c'est déjà arrivé ? Moi je prends à 2 contre 1 que ce n'est pas encore arrivé.

Il y a un monde entre
«Code moi un projet complet qui fait ça et ça»
et
«
Écris une fonction qui prend en entrée le chemin d'un fichier image, l'ouvre, inverse les canaux bleu et vert, puis le sauve en ajoutant "_BG" dans le nom de fichier.
»

Certes dans le deuxième cas on a le risque que l'IA invente des méthodes OpenCV qui n'existent pas (divulgâchis: ce n'est pas le cas), mais en gros, en lisant le code on comprend et c'est facilement testable.
Et puis surtout : si je sais que j'ai besoin d'une fonction qui fait exactement ça, c'est que je sais comment fonctionne le projet.

ai_usage.md

En fait ce serait une bonne pratique d'ajouter un fichier ai_usage.md dans nos projets pour expliquer quel usage de l'IA est fait dans le projet.
Les écrivains et les musiciens devraient également prendre la bonne habitude d'écrire un tel texte pour expliquer quelle est la part d'IA et quelle est la part d'invention humaine[1].

Allez go. J'écris le mien.

[1] Je soupçonne fortement celui-ci d'avoir bossé nettement plus que «écris une musique sympa avec des cuivres et des images steampunk».

Non c'est le même, en utilisant le modèle tu valide son entrainement;

Je me permet d'ajouter une nuance (qui était dans mon point de départ) : il est certain que l'utilisation PAYANTE valide l’entraînement.
Mais pour moi c'est pas clair que l'utilisation de la partie gratuite avec aucune intention de payer valide l'entraînement.

Exception 1

Si il y a une mécanique qui fait que :

1. si JE l'utilise, je crée de la pression sociale pour que LES AUTRES l'utilisent
2. les autres sont dans une situations qui les empêche d'utiliser la version gratuite.

Un cas de ce type serait un étudiant qui a une version étudiante gratuite de Word et qui enverrait des fichiers doc à d'autres personnes qui n'ont pas d'offre gratuite.

J'ai un peu du mal à voir comment ce genre de mécanisme existe avec l'utilisation de l'IA.

Exception 2

Si c'est financé par de la pub et que je n'ai pas une raison très solide de croire que la pub n'a pas d'influence sur moi.
Je considère un utilisateur qui affiche la pub comme un utilisateur payant.

Je pense que c'est pareil pour l'IA. Les requêtes gratuites font gonfler les stats, permettent la valorisation en bourse,

Ce qui est certain, c'est qu'une utilisation SANS PAYER de l'IA fait gonfler la bulle sans augmenter la valeur réelle.
Est-ce vraiment un problème ? Si des spéculateurs veulent perdre de l'argent pour me fournir les démonstrations de math qu'il me manque, c'est sympa de leur part.

légitiment l'usage et favorisent l'intégration de cette technologie dans notre quotidien.

Avec la façon dont je l'utilise pour le Frido, je suis tranquille avec ça.
Avec cette nouvelle écrire avec IA, tu as probablement raison.
Je ne crois pas que je recommencerai ce genre d'expérience, mais il y a une vérité dans le fait que j'encourage le monde à essayer.
Mais franchement, qui va payer pour ce type d'utilisation ?

As tu essayé de demander a un llm de traduire tes preuves en Rock pour les verifier automatiquement ?

Non, mais je veux bien voir un exemple.

Parce que cela est extrêmement energivore et destructeur de l'environnement ?

Quelque réflexions à ce propos.
Je tente d'utiliser le critère de «qu'est-ce qui se passerait si tout le monde faisait comme moi?».

Vu que je ne paye pas pour chatGPT et que je m'engage à ne ni pleurer ni payer si ça devenait payant, si tout le monde faisait comme moi, OpenAI aurait déjà fait faillite. Ok pour l'environnement de ce côté. (j'ai la même excuse pour youtube)

Vu que j'ai toujours tapé et publié sur internet mes notes de cours (ma thèse, mes cours de collège et d'univ), si tout le monde faisait comme moi, le Frido n'aurait pas besoin de chatGPT : tout serait facilement disponible sur internet.
De ce point de vue, chatGPT en réalité un moyen détourné d'accéder au contenu que les mathématiciens enferment dans des livres privateurs.

Ce pourquoi c'est d'après moi juste ridicule d'utiliser un LLM pour commencer, puisque ce sera souvent faux, ou pire: ce sera faux mais aura l'air d'être vrai si on n'est pas extrêmement attentif (bien plus attentif qu'on ne devrait l'être si on devait tout écrire soi-même); et dans tous les cas, on perdra énormément de temps à arriver à l'une ou l'autre des conclusions possibles.

Dans le cas très particulier des démonstrations mathématique, les réponses de chatGPT ne sont pas souvent fausses. Par contre, c'est vrai que quand elle est fausse, c'est presque toujours subtil, et l'erreur ruine généralement l'ensemble de la preuve.

C'est pourquoi je préfère toujours trouver une démonstration dans un cours publié par un humain.

MAIS MAIS MAIS MAIS MAIS …

Aussi incroyable que cela puisse paraître, il y a des trucs en math qu'on ne trouve pas sur internet. Un des plus gros pavé généré par LLM dans le Frido est toute la partie pour démontrer le théorème de Cauchy-Lipsitz analytique. À ma connaissance, le seul endroit sur internet où on donne la définition d'une application analytique entre espaces de Banach est ce document.

Et ce n'est pas faute d'avoir demandé à des humains:

https://math.stackexchange.com/questions/5113042/analytic-picard-lindel%c3%b6f-theorem
https://math.stackexchange.com/questions/5101596/analytic-picard-lindel%c3%b6f-theorem

(zéro réponses, mais les commentaires m'ont convaincu de passer par l'holomorphie, et y'avait encore pas mal de boulot)

tu as déjà fait le premier pas vers la facilité, et c'est vraiment dommage étant donné ton niveau d'implication,

Demander à un LLM n'est pas la facilité. Les démonstrations données dans les cours publiés par les profs sont toujours plus faciles à exploiter que celles données par les LLM—il y a plusieurs raisons à cela, et le fait qu'il y ait moins d'erreurs n'en est pas la principale.

Si les mathématiciens passaient un peu moins de temps à écrire le millième livre "Introduction à l'algèbre linéaire" publié chez un éditeur privateur (qui imprimera 500 exemplaires avant de le remplacer par le livre suivant exactement identique), et un peu plus de temps à publier des notes de cours bien faites, je ne serais pas réduit à demander à des LLM.

En attendant je reprécise mon flux :

1. j'ai une preuve sur mon écran (pdf, blog, mathoverflow et LLM)
2. je rédige une preuve complète sur ma feuille de brouillon (à la main, au crayon)
3. je retranscrit la preuve en LaTeX.

Prétendre que ce flux génère plus d'erreurs en partant d'un LLM que d'ailleurs est une hypothèse possible, mais elle doit être vérifiée empiriquement.

Pour l'instant l'erratum ne contient pas de fautes générées par l'IA.

Si quelqu'un veut aider à prouver le point de la médiocrité des LLM, il suffit de chercher les preuves dont les références contiennent un de ces trois :

• BIBooMistral
• BIBChatGPT
• BIBChatGPTDifficile

Et puis il faudra montrer que la densité de fautes parmi ces résultats est plus importante que parmi les autres.

Mode d'emploi: ag BIBChatGPT retourne des lignes comme:

\begin{proposition}[\cite{BIBooGIDYooKaacXf,BIBChatGPT}]    \label{PROPooYTMYooEYxuQc}

Ensuite il suffit de faire une recherche du label (PROPooYTMYooEYxuQc) dans le pdf pour trouver le résultat à vérifier.

le Frido est un livre de math libre que j'écris. Il y a beaucoup de choses, mais pas mal de théorèmes encore sans démonstration.

Il y a quelques semaines, quelqu'un m'a envoyé une "contribution" qui consiste à avoir copié-collé un énoncé sans démonstration dans Claude.

https://github.com/LaurentClaessens/mazhe/issues/269

La réponse de Claude est que l'énoncé était faux. Et effectivement, il était faux. Facile à vérifier, corrigé. Merci, une faute en moins :)

Ensuite, en l'espace de 2 heures, il m'a balancé les démonstrations de 4 théorème :

https://github.com/LaurentClaessens/mazhe/issues/271
https://github.com/LaurentClaessens/mazhe/issues/273
https://github.com/LaurentClaessens/mazhe/issues/272
https://github.com/LaurentClaessens/mazhe/issues/270

J'avoue n'avoir pas lu. Je crois que le "contributeur" est de bonne foi et croit réellement aider. Mais, comme j'ai tenté d'expliquer, en réalité ça n'aide pas du tout.

À la fin, je ne sais pas qu'en penser.

D'une part, je ne peux pas dire que je ne veux pas de preuves générées par IA, parce que moi-même j'utilise souvent chatGPT pour produire des démonstrations que je ne trouve pas sur internet.

Mais d'autre part, je veux que le contributeur me dise au moins "j'ai le niveau, je suis capable de comprendre la démonstration, je l'ai lue et elle est correcte".

Or j'ai du mal à croire qu'on puisse vraiment lire une démonstration et s'assurer qu'elle est correcte sans la re-rédiger soi-même.

Du coup je préfère quand même lire des textes rédigés par des humains.