Un experimento de demostración formal de un teorema de nivel intermedio en álgebra (Formalizing the proof of an intermediate-level algebra theorem -- An experiment)

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édiger des démonstrations mathématiques et d’en garantir leur correction. En novembre 2021, j’ai débuté un projet de vérification de la simplicité des groupes alternés au sein de l’assistant de preuve Lean, et de sa librairie mathlib. Ce texte est un essai de compte rendu de cette expérience. – Published version in Spanish