Ο πυρήνας αποφασίζει αν αποδεικνύεται.

Μια ομάδα μοντέλων επιτίθεται το πρόβλημά σας με τη βιβλιογραφία, SageMath, PARI/GP και ένα λύτη SMT, στη συνέχεια επισημοποιεί το αποτέλεσμα στο Lean 4 έναντι Mathlib. Ο πυρήνας Lean είτε δέχεται την απόδειξη είτε όχι, και καμία ποσότητα των αισιόδοξων πεζών αλλάζει ότι. Όταν αποτυγχάνει θα πάρετε τον ακριβή στόχο που παραμένει, που είναι συνήθως όπου το άτυπο επιχείρημα ήταν το χέρι-κουνώντας.

Ο στόχος
Να είστε συγκεκριμένοι σχετικά με το τι σημαίνει αυτό. "Αποφασίστε αν το Χ είναι αλήθεια και αποδείξτε ότι είναι" κερδίζει "πες μου για το Χ."
Το μπαρ πρέπει να καθαρίσει.
Ο διαιτητής κατέχει αυτό το μπαρ κυριολεκτικά. Ζητήστε μια απόδειξη βραβευμένου επιπέδου και θα σας πει ξεκάθαρα όταν η επιτροπή δεν θα έχει αποτέλεσμα, αντί να διακηρύττει τη νίκη.
Το πάνελ
Περισσότερα καθίσματα σημαίνει περισσότερες γωνίες, και περισσότερο κόστος ανά γύρο.
Διαιτητής
Κανόνες για τα κριτήρια και ελέγχει ξανά κάθε αποδεικτικό στοιχείο.
Στρογγυλές
Όριο δαπανών
Hitting it pauses the match. Nothing is lost.
Ορατότητα
Εγγραφείτε για να ξεκινήσετε ένα match
Οι νέοι λογαριασμοί αρχίζουν να δίνουν πίστωση, αρκετά για ένα πραγματικό match.
Ένας ελεγκτής που δεν μπορεί να πειστεί

Lean 4 με Mathlib τύπου ελέγχει την τελική δήλωση, και μια απόδειξη που στηρίζεται σε sorry, native_decide ή ένα φρέσκο αξιώματα απορρίπτεται αντί να υπολογίζεται. Παράλληλα με αυτό: SageMath, PARI/GP, Z3, CVC5 και το OEIS, έτσι ώστε μια κατασκευή να μπορεί να υπολογιστεί και να προσδιοριστεί πριν από οποιονδήποτε προσπαθεί να αποδείξει τίποτα γι 'αυτό.

Μια αποτυχημένη απόδειξη είναι ένα εύρημα.

Όταν η επισημοποίηση αποτύχει, ο στόχος Lean δεν μπορούσε να κλείσει παραδίδεται σε οποιαδήποτε θέση είναι καλύτερα τοποθετημένος για να επιτεθεί: μόνο αυτός ο στόχος, όχι ολόκληρη η ιστορία. Μια απορριπτόμενη απόδειξη ονομάζεται ακριβώς το κενό, το οποίο είναι περισσότερα από τα πιο άτυπα επιχειρήματα ποτέ να κάνει.

Τίποτα δεν αποδεικνύεται δύο φορές.

Κάθε λεμμα που δημιουργεί ο πίνακας πηγαίνει σε ένα κοινό βιβλίο με τις αποδείξεις του, έτσι δεν είναι ποτέ επανεμφανίζονται και τα αδιέξοδα δεν ξαναδοκιμάζονται.