Ο Claude απέδειξε το Θεώρημα του Φερμά σε 11 ημέρες. Ετυμηγορία: SHIP IT.

Τι καλύπτει αυτό το βίντεο

• Ο Claude επισημοποιεί το Τελευταίο Θεώρημα του Φερμά στο Lean 4
• Chromium sandbox RCE (CVE-2026-85046), που εκμεταλλεύτηκε στην πράξη, $1.000 ανταμοιβή
• Ο Shin Jin-seo κερδίζει τον KataGo με μειονέκτημα δύο λίθων

Μεταφρασμένη μεταγραφή

Μεταφράστηκε από την πρωτότυπη αγγλική αφήγηση. Ο διαθέσιμος ήχος και οι υπότιτλοι ελέγχονται από το YouTube.

0:00 Ο Φερμά είπε ότι η θαυμάσια απόδειξή του δεν θα χωρούσε στο περιθώριο, και σήμερα η Anthropic δημοσίευσε το περιθώριο: δεκατρία εκατομμύρια γραμμές Lean, πέντε φορές το μέγεθος του Mathlib, αποδεικνύοντας ένα θεώρημα που κάθε μαθηματικός ήδη πίστευε. Ήταν δέκα με έντεκα στην Τιφλίδα όταν η Anthropic δημοσίευσε, οπότε φυσικά ήμουν ξύπνιος. Χθες η Google κυκλοφόρησε τον Chrome 152 με δώδεκα διορθώσεις ασφαλείας, ένα από αυτά ένα σφάλμα V8 που ήδη εκμεταλλεύτηκε στην πράξη, και πλήρωσε τον αναφέροντα ένα χιλιάδες δολάρια, που είναι λιγότερα από το σεντάν που θα δούμε αργότερα.

0:26 Επίσης χθες, η Mullvad είπε ότι κλείνει το δημόσιο κρυπτογραφημένο DNS της στις 2 Νοεμβρίου και πληρώνει την Quad9 για να το κάνει αντ' αυτού, και σήμερα το Rust React Ο μεταγλωττιστής έγινε native στο Vite, ενώ το Hacker News ανακάλυψε τον IBM Bob, έναν πράκτορα κωδικοποίησης AI. Τότε ο Claude επισημοποίησε το Τελευταίο Θεώρημα του Φερμά, και στην ίδια πρώτη σελίδα ένας Κορεάτης grandmaster νίκησε τον ισχυρότερο κινητήρα Go στη Γη, οπότε σήμερα η ανθρωπότητα πήγε ένα στα δύο. Σε αυτό το βίντεο: τι απέδειξε πραγματικά ο Claude, τι κόστισε,

0:52 γιατί ο μαθηματικός που αφιέρωσε την καριέρα του σε αυτό λέει ότι δεν αλλάζει τίποτα και είναι ενθουσιασμένος παρόλα αυτά, και πώς ένας άνθρωπος νίκησε τη μηχανή στο Go. Είναι Παρασκευή, 4 Σεπτεμβρίου, και αυτό είναι το The Daily Diff. Τελευταίο Θεώρημα του Φερμά: κανένας θετικός ακέραιος a, b, c δεν ικανοποιεί το α εις την ν συν β εις την ν ίσον γ εις την ν για οποιοδήποτε ν πάνω από 2. Ο Φερμά το σκάλισε σε ένα περιθώριο γύρω στο 1637 και πέθανε χωρίς να δείξει την εργασία του, κάνοντάς τον τον πρώτο προγραμματιστή που έκλεισε ένα ticket με works on my machine. Ένα βραβείο 100.000 χρυσών μάρκων το 1908 προσέλκυσε 621 λανθασμένες

1:25 αποδείξεις τον πρώτο χρόνο του, και ο Andrew Wiles το κατάφερε τελικά το 1995, σε 129 σελίδες που χρειάστηκαν μήνες στους κριτές για να επαληθεύσουν. Επισημοποίηση σημαίνει αναγραφή αυτής της απόδειξης έτσι ώστε το Lean, ένας βοηθός απόδειξης, μπορεί να ελέγξει κάθε βήμα μηχανικά, και ο Kevin Buzzard στο Imperial ηγήθηκε μιας ανθρώπινης προσπάθειας να το κάνει ακριβώς αυτό από το 2024. Το προσχέδιο μόνο είναι 86 σελίδες. Ο ερευνητής της Anthropic Tianyi Peng κατεύθυνε δεκάδες πράκτορες Claude σε αυτό αντ' αυτού, σε μια πλατφόρμα που ονομάζεται Prove2Me, η οποία διατηρεί ένα DAG θεωρημάτων δηλώσεις ώστε οι πράκτορες να γνωρίζουν τι να αποδείξουν στη συνέχεια, γιατί χωρίς αυτήν οι πρώτες

2:00 σμήνη έχασαν την παρακολούθηση του ποιος αποδείκνυε τι, που είναι αυτό που συμβαίνει όταν το επίπεδο ενορχήστρωσης είναι regex με προϋπολογισμό μάρκετινγκ. Έντεκα ημέρες αργότερα ο ριζικός κόμβος έγραφε PROVED: δεκατρία εκατομμύρια γραμμές Lean, 29.500 ενδιάμεσα θεωρήματα, περίπου έξι δισεκατομμύρια διακριτικά εξόδου από ένα εσωτερικό μοντέλο περίπου συγκρίσιμο με τον Claude Fable 5.1. Η κατασκευή αποτυγχάνει εκτός εάν η απόδειξη βασίζεται ακριβώς στα τρία τυπικά αξιώματα του Lean: όχι συγγνώμη, όχι native decide, όχι cheating. Ο έλεγχος δεν είναι φθηνός ούτε: ένας

2:29 από την αρχή build χρειάστηκε πέντε και μισή ώρες σε 96 πυρήνες και 153 gigabytes RAM, και τα ονόματα των θεωρημάτων είναι παράγονται από μηχανή, οπότε το repo περιγράφει τον εαυτό του ως γραμμένο για να ελεγχθεί παρά να διαβαστεί, που είναι επίσης το πώς θα περιέγραφα την enterprise Java. Τώρα η αντίφαση. Η ανάρτηση της Anthropic λέει ότι το Lean αποδεικνύει την ορθότητα πέρα από κάθε αμφιβολία. Ο Kevin Buzzard, ο άνθρωπος που τον πρόλαβαν, μεταγλώττισε το repo σε ένα μηχάνημα 500 gigabyte που του δάνεισε η Anthropic, επιβεβαίωσε ότι ελέγχεται, και μετά έγραψε,

2:56 παράθεση, μαθηματικά αυτή η εργασία δεν μας λέει ουσιαστικά τίποτα. Ήταν ήδη 99,9 τοις εκατό σίγουρος ότι το θεώρημα ήταν αληθές, και η απόδειξη δεν προσθέτει νέα μαθηματικά. Αυτό που δείχνει είναι τι μπορεί να κάνει τώρα η αυτόματη επισημοποίηση, και για αυτό το κομμάτι είναι πραγματικά ενθουσιασμένος. Του δόθηκαν ένα εκατομμύριο λίρες σε πέντε χρόνια. Ο Claude χρειάστηκε έντεκα ημέρες, και τα πρόχειρα υπολογισμοί ενός σχολιαστή τοποθετούν έξι δισεκατομμύρια διακριτικά εξόδου στην τιμή καταλόγου περίπου 300.000 δολάρια, οπότε η μηχανή ήταν φθηνότερη, εκτός αν υπολογίσετε την εκπαίδευση της μηχανής, κάτι που κανείς δεν κάνει.

3:24 Καλύτερη λεπτομέρεια: το email έφτασε ενώ ήταν σε ένα μουσικό φεστιβάλ στην Ουαλία με μία γραμμή 4G, από ένα όνομα που δεν είχε ακούσει ποτέ, οπότε το θεώρησε ως φάρσα και το διάβασε μια εβδομάδα αργότερα, που είναι η σωστή απάντηση σε οποιαδήποτε γραμμή θέματος που περιέχει πλήρη επισημοποίηση. Εν τω μεταξύ, οι άνθρωποι πήραν μια νίκη. Ο Shin Jin-seo, ο νούμερο ένα στον κόσμο στο Go, νίκησε τον KataGo, την ισχυρότερη μηχανή Go ανοιχτού κώδικα, δύο παιχνίδια προς ένα στη Σεούλ με μειονέκτημα δύο λίθων, περίπου το χάσμα μεταξύ ενός κορυφαίου επαγγελματία και ενός αρχάριου επαγγελματία.

3:50 Ο καθοριστικός αγώνας ήταν μια νίκη 11,5 πόντων σε 221 κινήσεις, διατηρώντας 99 τοις εκατό πιθανότητα νίκης από τα μέσα του παιχνιδιού και κέρδισε 250 εκατομμύρια γουόν, περίπου 170.000 δολάρια, συν ένα Genesis G90, οπότε η αμοιβή για το να νικήσει μια υπεράνθρωπη τεχνητή νοημοσύνη είναι 170 φορές η αμοιβή της Google για μια διαφυγή από το sandbox του Chrome. Η εξήγησή του: στην αρχή αντέγραψε κινήσεις τεχνητής νοημοσύνης και έχασε. Νίκησε χτίζοντας τον πίνακα με το δικό του στυλ, που είναι η πιο χρήσιμη συμβουλή για την τεχνητή νοημοσύνη που έχω ακούσει όλο το χρόνο, και προήλθε από ένα επιτραπέζιο παιχνίδι. Δύο ακόμη γραμμές στο diff.

4:22 Ο μεταγλωττιστής Rust React από την oxc είναι πλέον εγγενής στο Vite πίσω από μία σημαία. Ένας κώδικας 1.036 αρχείων πήγε από 14,3 δευτερόλεπτα σε 0,81 στο βήμα μεταγλώττισης, κυρίως διαγράφοντας το Babel από το package.json, που είναι επίσης η ρουτίνα περιποίησης της επιδερμίδας μου. Και η IBM λάνσαρε τον Bob, έναν συνεργάτη κωδικοποίησης AI που σας χαιρετά με το «Γεια, Είμαι ο Bob», δημιουργεί υποπράκτορες, εκσυγχρονίζει τον κώδικα του mainframe, και κυκλοφορεί ένα προϊόν ανάλυσης που ονομάζεται Bobalytics, οπότε κάπου μια τράπεζα είναι πολύ ενθουσιασμένη και κανείς δεν διάβασε την άδεια.

4:51 Αυτό είναι πολύ περιθώριο για μια Παρασκευή. Αν προτιμάτε να το διαβάσετε αυτό παρά να με ακούσετε να το λέω, το diff φτάνει στα εισερχόμενά σας κάθε πρωί — δωρεάν στο the daily diff dot dev, σύνδεσμος παρακάτω. Λοιπόν, η σημερινή ετυμηγορία: SHIP IT. Ο πυρήνας λέει ναι, ο Buzzard λέει ναι, τα μαθηματικά δεν άλλαξαν, αλλά ο τρόπος που ελέγχουμε τα μαθηματικά μόλις άλλαξε. Αυτό είναι το σημερινό diff. Είμαι ο Νίκος από την Axrisi.

5:09 Συγχωνεύστε υπεύθυνα.

Πηγές

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com