Post

Article sur un sujet potentiellement intéressant, mais… qui parle d'un forum de maths sans nommer ce forum de maths — ce qui est quand même du “journalist slop” caractérisé (mais POURQUOI font-ils ce genre de choses? 🤬). Mais sinon, le problème est bien réel, et sérieux.

Certainement leanprover.zulipchat.com

Pour ce que ça vaut, j'ai testé ChatGPT plusieurs fois sur les mini-tests en Rocq que je donnais à mes étudiants en début de TP ce semestre (pour voir s'il y avait risque de triche), et les exercices étaient parfaitement résolus à chaque fois, sauf une où il a fait une erreur au premier coup.

J'ai d'ailleurs été un peu perturbé car j'avais moi-même fait exactement la même erreur au début. Je lui ai donné le message d'erreur et sa deuxième tentative était correcte. Les exercices ne pouvaient pas être dans le corpus d'entraînement vu que je venais de les créer.

C'étaient des exercices relativement simples et qui ne nécessitaient pas d'utiliser de lemmes de la stdlib, mais tout de même.

J'en parlais à l'instant ici bsky.app/profile/lips...