Autoformalização

Treze milhões de linhas na margem: o que faz deste o bom caso

Claude formalizou em onze dias a primeira demonstração do último teorema de Fermat verificada por computador. O teorema não é o mais interessante: aquele domínio tinha um …