Formalisation des Principia Mathematica de Russell avec Lean4

Ce projet vise à formaliser le premier volume des Principia Mathematica du Professeur Bertrand Russell à l'aide du prouveur de théorèmes Lean. L'objectif est de garantir que la formalisation corresponde clairement aux théorèmes correspondants du livre afin d'éviter toute confusion. Le projet suit rigoureusement les preuves de Russell, avec peu ou pas d'énoncés supplémentaires. Une nouvelle tactique, `Syll`, a été créée pour gérer une forme plus générale de syllogisme. Bien que les Principia Mathematica soient considérés comme un « échec monumental », l'auteur a trouvé le processus de formalisation enrichissant.