Bewijsassistent
Een bewijsassistent (Engels: proof assistant) of interactieve stellingbewijzer is een computerprogramma dat gebruikers helpt wiskundige bewijzen te schrijven.[1] Een bewijsassistent staat alleen correcte bewijzen toe, waardoor menselijke fouten worden vermeden. Voorbeelden van bewijsassistenten zijn Rocq, Isabelle, HOL Light, Lean en Mizar.
Bewijsassistenten maken gebruik van een formele theorie, bijvoorbeeld een hogere-orde predicatenlogica of een typetheorie[2]. Zowel stellingen als bewijzen worden in een formele taal aangegeven. Bewijzen worden interactief opgesteld door zogenaamde bewijstactieken (proof tactics), kleine subroutines waarmee bewijzen tot nieuwe bewijzen worden gecombineerd, aan te roepen.
Veel bewijsassistenten werken binnen het kader van de Curry–Howard-correspondentie, waarin stellingen overeenkomen met de datatypes van termen (meestal een soort lambdatermen), en deze termen overeenkomen met bewijzen.
Geschiedenis
[bewerken | brontekst bewerken]Een voorloper van moderne bewijsassistenten was Automath, een in 1967 door N.G. de Bruijn ontwikkelde formele taal waarin wiskundige theorieën en bewijzen konden worden uitgedrukt. Met een bijbebehorende bewijschecker konden de bewijzen op correctheid worden getoetst. In tegenstelling tot een bewijsassistent beschikte Automath niet over een interactieve modus. Automath werd nooit in brede kring gebruikt, maar was wel zeer invloedrijk voor latere bewijsassistenten.
Onafhankelijk daarvan ontwikkelde een onderzoeksgroep rond Robin Milner begin jaren 70 de interactieve stellingbewijzer LCF (Logic for Computable Functions). In het kader daarvan ontstond ook de programmeertaal ML. Niet alleen LCF zelf werd in ML geschreven, ML kon ook worden gebruikt om LCF uit te breiden door nieuwe bewijstactieken te schrijven. Moderne nakomelingen van LCF zijn bewijsassistenten uit de HOL-familie, waaronder Isabelle en HOL Light.
Automatische stellingbewijzers en computerondersteunde bewijzen
[bewerken | brontekst bewerken]Er zijn ook nog andere manieren hoe computers bij het bewijzen van wiskundige stellingen kunnen worden ingezet:
- Automatische stellingbewijzer. Een automatische stellingbewijzer probeert automatisch een bewijs van een wiskundige stelling te vinden. Een bewijsassistent, daarentegen, helpt een gebruiker bij het construeren van een bewijs, en is in staat te controleren dat dat bewijs ook geldig is.
- Computerondersteunde bewijzen. Bij sommige bewijzen worden computerprogramma's gebruikt om een groot aantal gevallen te controleren. Een bekend voorbeeld van zo'n bewijs is het eerste bewijs van de vierkleurenstelling van Kenneth Appel en Wolfgang Haken. Veel wiskundigen bekijken dergelijke bewijzen met argusogen, omdat de computerberekeningen moeilijk of helemaal niet met de hand te controleren zijn.
De grenzen hiertussen zijn niet heel scherp. De meeste bewijsassistenten kunnen eenvoudige stellingen bijvoorbeeld ook automatisch bewijzen, en bewijsassistenten kunnen worden ingezet om de resultaten van de computerondersteunde bewijzen te controleren.
Bekende formele bewijzen
[bewerken | brontekst bewerken]Bekende bewijzen waarbij een bewijsassistent werd toegepast zijn:
| Stelling | Gebruikte bewijsassistent | Jaar |
|---|---|---|
| Vierkleurenstelling[3] | Rocq | 2005 |
| Stelling van Feit-Thompson[4] | Rocq | 2012 |
| Vermoeden van Kepler[5] | Isabelle en HOL Light | 2017 |
- ↑ Geuvers, Herman (2009). Proof assistants: History, ideas and future. Sādhanā 34 (1). DOI:10.1007/s12046-009-0001-5.
- ↑ Henk Barendregt, Herman Geuvers (2001), 'Proof-assistants using Dependent Type Systems in: Alan J. A. Robinson, Andrei Voronkov (eds.), Handbook of Automated Reasoning, Vol 2. ISBN 978-0-444-50812-6.
- ↑ Gonthier, Georges (2008). Formal Proof—The Four-Color Theorem. Notices of the American Mathematical Society 55 (11)
- ↑ (2013). A Machine-Checked Proof of the Odd Order Theorem. Interactive Theorem Proving
- ↑ Thomas Hales et al. (2017). A formal proof of the kepler conjecture A formal proof of the Kepler conjecture. Forum of Mathematics, Pi 5. DOI:10.1017/fmp.2017.1.