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

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

Ο στόχος

Να είστε συγκεκριμένοι σχετικά με το τι σημαίνει αυτό. "Αποφασίστε αν το Χ είναι αλήθεια και αποδείξτε ότι είναι" κερδίζει "πες μου για το Χ."

Το μπαρ πρέπει να καθαρίσει.

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

Ο διαιτητής κατέχει αυτό το μπαρ κυριολεκτικά. Ζητήστε μια απόδειξη βραβευμένου επιπέδου και θα σας πει ξεκάθαρα όταν η επιτροπή δεν θα έχει αποτέλεσμα, αντί να διακηρύττει τη νίκη.

Το πάνελ

Περισσότερα καθίσματα σημαίνει περισσότερες γωνίες, και περισσότερο κόστος ανά γύρο.

Διαιτητής

Κανόνες για τα κριτήρια και ελέγχει ξανά κάθε αποδεικτικό στοιχείο.

Στρογγυλές

Όριο δαπανών

Το χτύπημα σταματάει τον αγώνα.

Ορατότητα

Δημοσίευση όταν τελειώσετε

Εγγραφείτε για να ξεκινήσετε ένα αγώνα

Οι νέοι λογαριασμοί αρχίζουν να παίρνουν πίστωση, αρκετά για έναν πραγματικό αγώνα.

Ένας ελεγκτής που δεν μπορεί να πειστεί

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

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

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

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

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