Formalizando a Principia Mathematica de Russell usando Lean4

Este projeto visa formalizar o primeiro volume da Principia Mathematica do Prof. Bertrand Russell usando o verificador de teoremas Lean. O objetivo é garantir que a formalização se alinhe claramente com os teoremas correspondentes no livro para evitar confusão. O projeto segue rigorosamente as provas de Russell, com poucas ou nenhuma declaração adicional. Um novo tático, `Syll`, foi criado para lidar com uma forma mais geral de silogismo. Embora a Principia Mathematica seja considerada um 'fracasso monumental', o autor achou o processo de formalização enriquecedor.