En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.
Le Frido est un livre de mathématique dont le but est d’aller de la théorie des ensembles (non comprise) jusqu’à finir l’agrégation. Giulietta est une extension qui va de l’agrégation jusqu’à tout ce que je sais en mathématique.
Le Frido est un livre de mathématique en quatre volumes reprenant à peu près tout de la construction des naturels (non incluse) jusqu’à la fin de l’agrégation, tant en algèbre qu’en analyse.
Le Frido 2018 est un livre libre de mathématique destiné à l’agrégation et plus. Il suppose connue la théorie des ensembles, puis fait tout en détail de la constructions des ensembles de nombres jusqu’aux statistiques en passant par les corps, les groupes, l’analyse, les probabilités et un peu de numérique.
