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)

Antoine Chambert-Loir

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 simpli…