SMF

Exposé Bourbaki 1086 : Preuves formelles : développements récents

Exposé Bourbaki 1086 : Developments in formal proofs

Thomas C. HALES
Exposé Bourbaki 1086 : Preuves formelles : développements récents
  • Consulter un extrait
  •  
                
  • Année : 2015
  • Tome : 367-368
  • Format : Électronique
  • Langue de l'ouvrage :
    Anglais
  • Class. Math. : 03B15, 03B35, 68T15.
  • Pages : 387-410
  • DOI : 10.24033/ast.952

A formal proof is a proof that can be read and verified by computer, directly from the fundamental rules of logic and the foundational axioms of mathematics. The technology behind formal proofs has been under development for decades and grew out of efforts in the early twentieth century to place mathematics on secure foundations. In recent years, this technology has made remarkable advances. Notably, a project led by Georges Gonthier has produced a complete formal verification of the odd-order theorem of Feit and Thompson. This presentation will describe major recent developments in this field.

Une preuve formelle est une preuve qui peut être lue et vérifiée par un ordinateur, directement à partir des règles fondamentales de la logique et des axiomes fondateurs des mathématiques. Issue des efforts du début du xxe siècle visant à placer les mathématiques sur des fondations sûres, la technologie qui sous-tend les preuves formelles s'est développée depuis des dizaines d'années et a fait des progrès remarquables ces dernières années. Notamment, un projet dirigé par Georges Gonthier a abouti à une vérification formelle complète du théorème de Feit-Thompson selon lequel tout groupe fini d'ordre impair est résoluble. Cet exposé décrira les principaux développements récents du sujet.


Électronique
Electronic
Prix public Public price 10.00 €
Prix membre Member price 7.00 €
Quantité
Quantity
- +