  Proof assistants are computer softwares that allow us to write mathematical
proofs so as to assess their correctness. In November 2021, I started the
project of checking the simplicity of the alternating groups within the Lean
theorem prover and its mathlib library. This text aims at reviewing this
experiment.
  --
  (French) Les assistants de preuves sont des logiciels qui permettent de
r\'ediger des d\'emonstrations math\'ematiques et d'en garantir leur
correction. En novembre 2021, j'ai d\'ebut\'e un projet de v\'erification de la
simplicit\'e des groupes altern\'es au sein de l'assistant de preuve Lean, et
de sa librairie mathlib. Ce texte est un essai de compte rendu de cette
exp\'erience.
  --
  Published version in Spanish
