Η μαθηματική απόδειξη
από τον Ευκλείδη και τα αξιώματα έως τον Gödel, τους υπολογιστές και την τεχνητή νοημοσύνη
Από όλες τις μορφές γνώσης, η μαθηματική βεβαιότητα μοιάζει ίσως η πιο απόλυτη. Ένα θεώρημα δεν θεωρείται αληθινό επειδή επιβεβαιώθηκε πολλές φορές ούτε επειδή κανείς δεν έχει καταφέρει μέχρι σήμερα να το διαψεύσει. Θεωρείται αληθινό επειδή έχει αποδειχθεί. Τι είναι όμως αυτό που κάνει μια απόδειξη ισχυρότερη από οποιονδήποτε αριθμό παρατηρήσεων;
Ας φανταστούμε έναν υπολογιστή που ελέγχει αν μια μαθηματική πρόταση ισχύει για καθέναν από τους πρώτους ένα δισεκατομμύριο φυσικούς αριθμούς και δεν βρίσκει ούτε μία εξαίρεση. Την ίδια στιγμή, ένας μαθηματικός γράφει δέκα γραμμές και υποστηρίζει ότι το ζήτημα έχει κλείσει οριστικά. Ο πρώτος προσφέρει ένα δισεκατομμύριο επιβεβαιώσεις· ο δεύτερος, μία απόδειξη. Ποιο από τα δύο αποτελέσματα αρκεί για να είμαστε βέβαιοι ότι η πρόταση ισχύει πάντοτε;
Στην καθημερινή ζωή, ένα δισεκατομμύριο επιβεβαιώσεις μοιάζουν ακαταμάχητες. Στα μαθηματικά, όμως, δεν παύουν να αποτελούν παρατηρήσεις — πάρα πολλές, αλλά πεπερασμένες. Αν μια πρόταση αφορά όλους τους φυσικούς αριθμούς, μετά το δισεκατομμύριο ακολουθούν άπειροι ακόμη. Μία και μόνο εξαίρεση, όσο μακριά κι αν κρύβεται, αρκεί για να καταρρεύσει ολόκληρος ο ισχυρισμός.
Η απόδειξη είναι η απάντηση των μαθηματικών σε αυτό το πρόβλημα. Δεν δηλώνει απλώς ότι κάτι φαίνεται να είναι αληθινό· δείχνει γιατί πρέπει να είναι αληθινό, εφόσον αποδεχθούμε συγκεκριμένες αφετηρίες και κανόνες. Γι’ αυτό η ιστορία της μαθηματικής απόδειξης δεν αποτελεί απλώς ένα κεφάλαιο της γεωμετρίας ή της λογικής. Είναι η ιστορία μιας ανθρώπινης μεθόδου για τη δημιουργία ελέγξιμης εμπιστοσύνης.
Πριν από την απόδειξη
Οι Βαβυλώνιοι και οι Αιγύπτιοι διέθεταν εντυπωσιακές μαθηματικές γνώσεις. Υπολόγιζαν εμβαδά και όγκους, έλυναν πρακτικά προβλήματα και παρακολουθούσαν αστρονομικούς κύκλους. Οι πινακίδες και οι πάπυροι που σώθηκαν περιέχουν αλγορίθμους και κανόνες με αξιοθαύμαστη ακρίβεια. Επομένως, δεν υπήρχε ένας κόσμος χωρίς μαθηματική σκέψη πριν από τους Έλληνες.
Η αλλαγή ήταν κυρίως στον τρόπο με τον οποίο ζητούσαν να στηριχθεί ένα συμπέρασμα. Η πρακτική οδηγία «κάνε αυτά τα βήματα και θα πάρεις το αποτέλεσμα» άρχισε να συνοδεύεται από ένα αυστηρότερο αίτημα: «δείξε γιατί το αποτέλεσμα ακολουθεί αναγκαστικά».
Η μετάβαση δεν έγινε σε μία στιγμή και δεν ήταν έργο ενός μόνο ανθρώπου. Ωστόσο, γύρω στο 300 π.Χ., ο Ευκλείδης οργάνωσε στα «Στοιχεία» ένα μεγάλο σώμα γνώσης με πρωτοφανή πειθαρχία: πρώτα οι ορισμοί και τα αιτήματα, έπειτα οι προτάσεις, καθεμία βασισμένη σε όσα είχαν ήδη γίνει δεκτά ή αποδειχθεί. Τα «Στοιχεία» δεν ήταν απλώς ένα βιβλίο γεωμετρίας. Ήταν μια αρχιτεκτονική του λόγου.
Τι ακριβώς κάνει μια απόδειξη;
Ας δούμε ένα από τα διασημότερα παραδείγματα: την απόδειξη ότι υπάρχουν άπειροι πρώτοι αριθμοί. Πρώτοι είναι οι αριθμοί μεγαλύτεροι από το 1 που διαιρούνται ακριβώς μόνο με το 1 και με τον εαυτό τους, όπως οι 2, 3, 5, 7 και 11.
Το επιχείρημα δεν επιχειρεί να μετρήσει όλους τους πρώτους. Δείχνει ότι οποιαδήποτε πεπερασμένη λίστα πρώτων κι αν θεωρήσουμε πλήρη, μπορούμε να αποδείξουμε ότι της λείπει τουλάχιστον ένας.
Βήμα 1: Υποθέτουμε ότι η λίστα είναι πλήρης
Ας υποθέσουμε, για χάρη του επιχειρήματος, ότι έχουμε γράψει όλους τους πρώτους αριθμούς:
p₁, p₂, p₃, …, pₙ
Η υπόθεση αυτή είναι ακριβώς εκείνη που θα ελέγξουμε.
Βήμα 2: Πολλαπλασιάζουμε τα μέλη της λίστας
Ονομάζουμε P το γινόμενο όλων αυτών των πρώτων:
P = p₁ × p₂ × p₃ × … × pₙ
Βήμα 3: Προσθέτουμε μία μονάδα
Κατασκευάζουμε έναν νέο αριθμό N:
N = P + 1
Άρα:
N = (p₁ × p₂ × p₃ × … × pₙ) + 1
Βήμα 4: Εξετάζουμε ποιος μπορεί να διαιρεί τον N
Αν διαιρέσουμε τον N με οποιονδήποτε πρώτο της λίστας, θα μείνει υπόλοιπο 1. Ο λόγος είναι απλός: το P διαιρείται ακριβώς με κάθε pᵢ, ενώ ο N είναι κατά μία μονάδα μεγαλύτερος από το P.
Επομένως, κανένας πρώτος της υποτιθέμενης πλήρους λίστας δεν διαιρεί τον N. Ο N μπορεί να είναι πρώτος. Μπορεί επίσης να είναι σύνθετος — αυτό δεν χαλά το επιχείρημα. Αν είναι σύνθετος, τότε έχει τουλάχιστον έναν πρώτο διαιρέτη, και αυτός ο διαιρέτης δεν βρίσκεται στη λίστα μας.
Άρα, σε κάθε περίπτωση, υπάρχει ένας πρώτος που λείπει. Η αρχική υπόθεση ότι είχαμε καταγράψει όλους τους πρώτους οδηγεί σε αντίφαση. Συνεπώς, οι πρώτοι αριθμοί δεν τελειώνουν.
Ένα μικρό αριθμητικό παράδειγμα κάνει τη λογική πιο ορατή. Ας προσποιηθούμε ότι οι μόνοι πρώτοι είναι οι 2, 3, 5 και 7:
P = 2 × 3 × 5 × 7 = 210
N = 210 + 1 = 211
Ο 211 δεν διαιρείται με κανέναν από τους 2, 3, 5 ή 7. Στη συγκεκριμένη περίπτωση είναι και ο ίδιος πρώτος. Σε άλλα παραδείγματα ο νέος αριθμός μπορεί να μην είναι πρώτος, αλλά οι πρώτοι παράγοντές του θα βρίσκονται πάντως έξω από την αρχική λίστα.
Η δύναμη της απόδειξης δεν προέρχεται από το πλήθος των παραδειγμάτων. Δεν χρειάζεται να ελέγξουμε ούτε εκατό ούτε ένα δισεκατομμύριο αριθμούς. Μία γενική ιδέα καλύπτει κάθε δυνατή πεπερασμένη λίστα. Μετατρέπει το «φαίνεται ότι οι πρώτοι συνεχίζονται» στο «είναι αδύνατον να τελειώσουν».
Πού στηρίζεται μια απόδειξη;
Κάθε απόδειξη πρέπει να αρχίζει από κάπου. Αν κάθε πρόταση χρειαζόταν να στηριχθεί σε μια προηγούμενη, και εκείνη σε μια ακόμη παλαιότερη, δεν θα φτάναμε ποτέ σε αφετηρία. Γι’ αυτό τα μαθηματικά χρησιμοποιούν ορισμούς, κανόνες λογικής και αξιώματα.
Οι ορισμοί εξηγούν με ακρίβεια τι σημαίνουν οι λέξεις. Οι κανόνες λογικής καθορίζουν ποια συμπεράσματα επιτρέπεται να βγάλουμε. Τα αξιώματα είναι οι αρχικές προτάσεις που δεχόμαστε χωρίς να τις αποδεικνύουμε μέσα στο ίδιο σύστημα. Η απόδειξη δεν δημιουργεί αλήθεια από το τίποτα. Δείχνει τι ακολουθεί αναγκαστικά από τις αφετηρίες που επιλέξαμε.
Αυτό είναι κρίσιμο: ένα συμπέρασμα μπορεί να είναι απολύτως σωστό μέσα σε ένα σύστημα, αλλά το σύστημα να μην αποτελεί τη μοναδική δυνατή περιγραφή της πραγματικότητας.
Το παράξενο πέμπτο αίτημα
Για αιώνες, τα αξιώματα του Ευκλείδη θεωρούνταν σχεδόν αυτονόητες περιγραφές του χώρου. Ένα από αυτά, όμως, προκαλούσε αμηχανία: το πέμπτο αίτημα, που σχετίζεται με τις παράλληλες ευθείες, ήταν πολύ πιο περίπλοκο από τα υπόλοιπα.
Πολλοί μαθηματικοί προσπάθησαν να το αποδείξουν χρησιμοποιώντας μόνο τα άλλα αιτήματα. Οι προσπάθειες αποτύγχαναν, συνήθως επειδή κάπου χρησιμοποιούσαν κρυφά μια ισοδύναμη μορφή εκείνου που ήθελαν να αποδείξουν.
Τον 19ο αιώνα οι Nikolai Lobachevsky και János Bolyai δοκίμασαν κάτι ριζοσπαστικό: αντί να αποδείξουν το πέμπτο αίτημα, το αντικατέστησαν. Το αποτέλεσμα δεν ήταν χάος, αλλά μια συνεπής μη ευκλείδεια γεωμετρία. Αργότερα, ο Bernhard Riemann άνοιξε τον δρόμο προς ακόμη γενικότερους καμπύλους χώρους.
Η ανακάλυψη άλλαξε βαθιά το νόημα των αξιωμάτων. Δεν είναι πάντοτε αλήθειες που επιβάλλονται από την κοινή εμπειρία. Είναι δηλωμένες αρχικές παραδοχές. Στην επίπεδη ευκλείδεια γεωμετρία ισχύουν ορισμένα θεωρήματα· πάνω σε μια σφαίρα ή σε έναν υπερβολικό χώρο, ισχύουν άλλα. Η απόδειξη παραμένει αυστηρή, αλλά το συμπέρασμά της συνοδεύεται πάντα από ένα σιωπηλό «εφόσον δεχθούμε αυτές τις αφετηρίες».
Το όνειρο μιας τέλειας μαθηματικής μηχανής
Στα τέλη του 19ου και στις αρχές του 20ού αιώνα, η συμβολική λογική και η θεωρία συνόλων έδωσαν την ελπίδα ότι ολόκληρα τα μαθηματικά θα μπορούσαν να γραφτούν ως ένα πλήρες σύστημα συμβόλων και κανόνων. Ταυτόχρονα, παράδοξα όπως εκείνο του Russell έδειξαν πόσο εύκολα μια φαινομενικά αθώα έννοια μπορεί να οδηγήσει σε αντίφαση.
Ο David Hilbert οραματίστηκε ένα πρόγραμμα θεμελίωσης των μαθηματικών. Ήθελε ένα τυπικό σύστημα αρκετά ακριβές ώστε κάθε σωστό βήμα να μπορεί να ελεγχθεί μηχανικά, καθώς και μια απόδειξη ότι το ίδιο το σύστημα είναι συνεπές — ότι δεν μπορεί δηλαδή να αποδείξει ταυτόχρονα μια πρόταση και την άρνησή της.
Ήταν ένα όνειρο απόλυτης τάξης: κάθε καλά διατυπωμένο μαθηματικό ερώτημα θα είχε, τουλάχιστον κατ’ αρχήν, μια οριστική απάντηση. Και τότε εμφανίστηκε ο Kurt Gödel.
Τα όρια της απόδειξης
Το 1931 ο Gödel έδειξε ότι κάθε συνεπές, αποτελεσματικά αξιωματοποιημένο σύστημα που είναι αρκετά ισχυρό ώστε να περιλαμβάνει βασική αριθμητική έχει αναπόφευκτα όρια. Υπάρχουν προτάσεις στη γλώσσα του που δεν μπορούν ούτε να αποδειχθούν ούτε να διαψευστούν μέσα στο ίδιο σύστημα. Επιπλέον, υπό τις κατάλληλες προϋποθέσεις, ένα τέτοιο σύστημα δεν μπορεί να αποδείξει τη δική του συνέπεια χρησιμοποιώντας μόνο τα δικά του μέσα.
Η βασική ιδέα ήταν εντυπωσιακή. Ο Gödel βρήκε τρόπο να κωδικοποιήσει προτάσεις και αποδείξεις ως αριθμούς. Έτσι, η αριθμητική μπορούσε έμμεσα να μιλήσει για τον ίδιο της τον μηχανισμό. Κατασκεύασε μια πρόταση που, σε πολύ απλουστευμένη διατύπωση, λέει: «Δεν είμαι αποδείξιμη μέσα σε αυτό το σύστημα».
Το αποτέλεσμα συχνά παρερμηνεύεται. Ο Gödel δεν απέδειξε ότι «τίποτα δεν είναι βέβαιο» ούτε ότι η λογική απέτυχε. Απέδειξε ένα ακριβές όριο για συγκεκριμένα τυπικά συστήματα. Μπορούμε να προσθέσουμε νέα αξιώματα και να λύσουμε ορισμένα από τα προηγούμενα αδιέξοδα. Τότε, όμως, έχουμε δημιουργήσει ένα ισχυρότερο σύστημα, το οποίο θα έχει τα δικά του νέα όρια.
Η απόδειξη δεν χάνει την αξία της. Απλώς παύει να εμφανίζεται ως μια μηχανή που μπορεί να κλείσει για πάντα ολόκληρο τον μαθηματικό ορίζοντα.
Όταν ένας άνθρωπος δεν μπορεί να ελέγξει ολόκληρη την απόδειξη
Το 1976 οι Kenneth Appel και Wolfgang Haken απέδειξαν το θεώρημα των τεσσάρων χρωμάτων: κάθε επίπεδος χάρτης μπορεί να χρωματιστεί με το πολύ τέσσερα χρώματα, έτσι ώστε δύο περιοχές με κοινό σύνορο να μην έχουν το ίδιο χρώμα. Ένα σημαντικό μέρος της απόδειξης απαιτούσε τον υπολογιστικό έλεγχο πολλών διαφορετικών περιπτώσεων.
Η στιγμή ήταν ιστορική αλλά και άβολη. Για πρώτη φορά, η μαθηματική κοινότητα έπρεπε να δεχθεί μια απόδειξη της οποίας κρίσιμο τμήμα κανένας άνθρωπος δεν μπορούσε να ελέγξει γραμμή προς γραμμή με τον παραδοσιακό τρόπο. Η εμπιστοσύνη μεταφέρθηκε εν μέρει από το χαρτί στο πρόγραμμα, στο υλικό και στη διαδικασία επαλήθευσης.
Παρόμοιο πρόβλημα εμφανίστηκε στην απόδειξη της εικασίας του Kepler για την πυκνότερη δυνατή συσκευασία ίσων σφαιρών. Η αρχική απόδειξη του Thomas Hales ήταν τόσο μεγάλη και υπολογιστικά απαιτητική ώστε οι κριτές δεν μπορούσαν να πιστοποιήσουν κάθε λεπτομέρεια. Το πρόγραμμα Flyspeck μετέφερε αργότερα ολόκληρη την απόδειξη σε συστήματα τυπικής επαλήθευσης και ολοκληρώθηκε το 2014.
Τι είναι ένας βοηθός αποδείξεων;
Εργαλεία όπως τα Lean, Isabelle, HOL Light και Rocq ονομάζονται proof assistants, δηλαδή βοηθοί αποδείξεων. Δεν «καταλαβαίνουν» ένα θεώρημα όπως ένας άνθρωπος. Ελέγχουν αν κάθε μικρό βήμα επιτρέπεται από τους δηλωμένους κανόνες.
Στο Lean, για παράδειγμα, μια μαθηματική πρόταση αναπαρίσταται ως ένας τύπος και η απόδειξή της ως ένα αντικείμενο αυτού του τύπου. Ένας μικρός ελεγκτικός πυρήνας εξετάζει το τελικό αντικείμενο. Αν κάποιο βήμα δεν ακολουθεί από τους κανόνες, η απόδειξη απορρίπτεται.
Το πλεονέκτημα είναι ότι δεν χρειάζεται να εμπιστευτούμε ένα τεράστιο και περίπλοκο πρόγραμμα στο σύνολό του. Μπορούμε να βασίσουμε τον τελικό έλεγχο σε έναν πολύ μικρότερο πυρήνα. Βέβαια, η εμπιστοσύνη δεν εξαφανίζεται εντελώς: εξακολουθούμε να εμπιστευόμαστε τον ορισμό του συστήματος, την υλοποίηση του πυρήνα, τον μεταγλωττιστή και το υλικό. Όμως οι κρίσιμες προϋποθέσεις γίνονται σαφέστερες και πιο περιορισμένες.
Η τεχνητή νοημοσύνη και οι νέες αποδείξεις
Η τεχνητή νοημοσύνη μπορεί να βοηθήσει στην αναζήτηση αποδείξεων: να προτείνει ενδιάμεσα λήμματα, να επιλέγει κατάλληλες τακτικές, να μεταφράζει ένα άτυπο επιχείρημα σε τυπική γλώσσα και να εξερευνά γρήγορα πολλούς πιθανούς δρόμους.
Αυτό δεν σημαίνει ότι γίνεται αυτομάτως αλάνθαστη μαθηματική αυθεντία. Ένα σύστημα μπορεί να προτείνει ένα πειστικό αλλά λανθασμένο βήμα, όπως μπορεί να παραγάγει μια σωστή ακολουθία χωρίς να εξηγεί γιατί είναι ενδιαφέρουσα. Γι’ αυτό η πιο αξιόπιστη χρήση της τεχνητής νοημοσύνης συνδέει την παραγωγή ιδεών με ανεξάρτητο τυπικό έλεγχο: η τεχνητή νοημοσύνη προτείνει, ο ελεγκτικός πυρήνας επαληθεύει και ο άνθρωπος κρίνει τη σημασία.
Η ανθρώπινη δημιουργικότητα δεν εξαφανίζεται. Μετακινείται προς την επιλογή των ερωτημάτων, τη διατύπωση των κατάλληλων ορισμών και την αναζήτηση μιας απόδειξης που δεν είναι μόνο σωστή, αλλά και κατανοητή. Η ορθότητα και η κατανόηση είναι συγγενείς έννοιες, όχι όμως ταυτόσημες.
Η απόδειξη ως κοινή γλώσσα εμπιστοσύνης
Συχνά φανταζόμαστε την απόδειξη ως κάτι εντελώς απρόσωπο: μια ακολουθία λογικών βημάτων που θα ήταν έγκυρη ακόμη κι αν δεν υπήρχε κανείς να τη διαβάσει. Στην πράξη, όμως, οι αποδείξεις γράφονται για κοινότητες. Χρησιμοποιούν κοινή γλώσσα, αποδεκτές συμβάσεις, βιβλιοθήκες παλαιότερων θεωρημάτων, κρίση ειδικών και θεσμούς ελέγχου.
Αυτή είναι ίσως η βαθύτερη αξία τους. Η απόδειξη δεν μας προσφέρει μια μαγική έξοδο από κάθε αμφιβολία. Μας υποχρεώνει να δηλώσουμε από πού ξεκινάμε, ποια βήματα επιτρέπουμε και πού ακριβώς στηρίζεται το συμπέρασμα. Μετατρέπει την αυθεντία σε διαδρομή που μπορεί να ελεγχθεί από άλλους.
Επίλογος: ένα δημόσιο «επειδή»
Οι ένα δισεκατομμύριο επιβεβαιώσεις της αρχικής μας εικόνας μπορεί να είναι εξαιρετικά πειστικές. Οι δέκα γραμμές μιας σωστής απόδειξης κάνουν κάτι διαφορετικό: δεν προσθέτουν ακόμη μία παρατήρηση. Αλλάζουν το είδος της γνώσης που έχουμε.
Από τα σχήματα του Ευκλείδη έως τον κώδικα ενός proof assistant, η απόδειξη εξελίχθηκε χωρίς να χάσει τον πυρήνα της. Είναι ο τρόπος με τον οποίο μετατρέπουμε το «πιστεύω ότι ισχύει» στο «μπορώ να δείξω από πού προκύπτει». Οι μη ευκλείδειες γεωμετρίες μάς έμαθαν ότι κάθε συμπέρασμα εξαρτάται από τις αφετηρίες του. Ο Gödel έδειξε ότι κανένα αρκετά ισχυρό τυπικό πλαίσιο δεν κλείνει οριστικά τον ορίζοντα. Οι υπολογιστές και η τεχνητή νοημοσύνη επεκτείνουν την κλίμακα της αναζήτησης και του ελέγχου, χωρίς να καταργούν την ανάγκη για σαφείς κανόνες και ανθρώπινη κρίση.
Η μαθηματική απόδειξη δεν είναι απλώς μια σφραγίδα αλήθειας. Είναι ένα δημόσιο «επειδή» — μια πρόσκληση προς οποιονδήποτε να ακολουθήσει τον δρόμο, να εξετάσει τα βήματα και, αν βρει κενό, να τα απορρίψει. Σε μια εποχή όπου η πληροφορία πολλαπλασιάζεται γρηγορότερα από την εμπιστοσύνη, αυτή η παλιά τέχνη ίσως είναι πιο σύγχρονη από ποτέ.
Change is the only Constant
