Η σημασία της τυπικής επαλήθευσης στα μαθηματικά
Το πρόβλημα της διάταξης 11 τετραγώνων σε ένα μεγαλύτερο τετράγωνο αποτελεί κλασική πρόκληση στη γεωμετρία. Η πρόσφατη εργασία που δημοσιεύτηκε στο αποθετήριο 11SquaresFormalized δεν περιορίζεται σε μια απλή αριθμητική προσέγγιση, αλλά παρέχει μια πλήρως τυπική απόδειξη (formal proof) που έχει επαληθευτεί από τον proof assistant Lean 4. Η χρήση τυπικών μεθόδων εξαλείφει την πιθανότητα ανθρώπινου σφάλματος στη λογική αλυσίδα, καθιστώντας το αποτέλεσμα μαθηματικά αδιαμφισβήτητο.
Αρχιτεκτονική της απόδειξης και υπολογιστική ισχύς
Η αρχιτεκτονική της λύσης διαχωρίζει τα γεωμετρικά επιχειρήματα από τους αριθμητικούς ελέγχους. Ενώ η γεωμετρία και η συναρμολόγηση της απόδειξης βασίζονται σε παραδοσιακές αποδείξεις του Lean, τα υπολογιστικά ακριβή πιστοποιητικά (numerical certificates) χρησιμοποιούν το native_decide. Αυτή η προσέγγιση επιτρέπει την εκτέλεση κώδικα σε native επίπεδο, διατηρώντας παράλληλα την ακεραιότητα του συστήματος μέσω του Lean kernel.
Αναπαραγωγιμότητα και εργαλεία
Η διασφάλιση της αναπαραγωγιμότητας αποτέλεσε προτεραιότητα για την ομάδα. Με τη χρήση του lake-manifest.json και συγκεκριμένων εκδόσεων του Lean (4.34.1) και του Mathlib, οι χρήστες μπορούν να εκτελέσουν το script επαλήθευσης (run_verification.sh). Η διαδικασία ελέγχει κάθε module ξεχωριστά, διασφαλίζοντας ότι δεν υπάρχουν «παραδοχές» (admissions) και ότι το τελικό αποτέλεσμα είναι πλήρως επαληθευμένο από τον compiler.