კლოდმა ფერმას თეორემა 11 დღეში დაამტკიცა. ვერდიქტი: SHIP IT.

რას მოიცავს ეს ვიდეო

• კლოდი აფორმალებს ფერმას ბოლო თეორემას Lean 4-ში
• Chromium sandbox RCE (CVE-2026-85046), ექსპლოიტირებული ველურ ბუნებაში, 1,000 აშშ დოლარი ჯილდო
• შინ ჯინ-სეო ამარცხებს KataGo-ს ორქვიან ჰანდიკაპით

ნათარგმნი ტრანსკრიპტი

ნათარგმნია ორიგინალური ინგლისური ნარატივიდან. ხელმისაწვდომი აუდიო და სუბტიტრები კონტროლდება YouTube-ის მიერ.

0:00 ფერმამ თქვა, რომ მისი შესანიშნავი მტკიცებულება ზღვარზე არ მოთავსდებოდა, და დღეს Anthropic-მა გამოაქვეყნა ზღვარი: ცამეტი მილიონი ხაზი Lean-ში, ხუთჯერ მეტი ვიდრე Mathlib-ის ზომა, ამტკიცებს თეორემას, რომლისაც ყველა მათემატიკოსს უკვე სჯეროდა. თბილისში ათი-თერთმეტი საათი იყო, როცა Anthropic-მა გამოაქვეყნა, ამიტომ, ბუნებრივია, მე არ მეძინა. გუშინ Google-მა გამოუშვა Chrome 152 თორმეტი უსაფრთხოების შესწორებით, ერთ-ერთი მათგანი V8-ის ხარვეზი იყო, რომელიც უკვე ექსპლოიტირებულია ველურ ბუნებაში, და რეპორტიორს გადაუხადეს ათასი დოლარი, რაც ნაკლებია იმ სედანზე, რომელზეც მოგვიანებით ვისაუბრებთ.

0:26 ასევე გუშინ, Mullvad-მა თქვა, რომ 2 ნოემბერს თიშავს თავის საჯარო დაშიფრულ DNS-ს და Quad9-ს უხდის ამის გასაკეთებლად, და ამ დილით Rust React კომპილერი გახდა ნეიტიური Vite-ში, ხოლო Hacker News-მა აღმოაჩინა IBM Bob, AI კოდირების აგენტი. შემდეგ კლოდმა ფორმალურად ჩამოაყალიბა ფერმას ბოლო თეორემა, და იმავე პირველ გვერდზე კორეელმა დიდოსტატმა დაამარცხა დედამიწაზე ყველაზე ძლიერი Go ძრავა, ამიტომ დღეს კაცობრიობამ ერთი-ორში მოიგო. ამ ვიდეოში: რა დაამტკიცა კლოდმა სინამდვილეში, რა დაჯდა,

0:52 რატომ ამბობს მათემატიკოსი, რომელმაც მთელი კარიერა ამას მიუძღვნა, რომ ეს არაფერს ცვლის და მაინც აღფრთოვანებულია, და როგორ დაამარცხა ადამიანმა მანქანა Go-ში. პარასკევია, 4 სექტემბერი, და ეს არის The Daily Diff. ფერმას ბოლო თეორემა: არცერთი დადებითი მთელი რიცხვი a, b, c არ აკმაყოფილებს a ხარისხში n-ს პლუს b ხარისხში n-ს უდრის c ხარისხში n-ს ნებისმიერი n-ისთვის 2-ზე მეტი. ფერმამ ის ზღვარზე დაახლოებით 1637 წელს მიაწერა და თავისი ნამუშევრის ჩვენების გარეშე გარდაიცვალა, რაც მას პირველ დეველოპერად აქცევს, ვინც ბილეთი „ჩემს მანქანაზე მუშაობს“-ით დახურა. 1908 წლის 100 000 ოქროს მარკის პრიზმა პირველ წელს 621 არასწორი

1:25 მტკიცებულება მიიზიდა, და ენდრიუ უაილსმა საბოლოოდ მიიღო ის 1995 წელს, 129 გვერდში, რომელთა გადამოწმებას რეფერენტებს თვეები დასჭირდა. ფორმალურად ჩამოყალიბება ნიშნავს ამ მტკიცებულების გადაწერას ისე, რომ Lean-მა, მტკიცებულების ასისტენტმა, შეძლოს ყოველი ნაბიჯის მექანიკურად შემოწმება, და კევინ ბაზარდმა იმპერიალში 2024 წლიდან ადამიანური ძალისხმევა მიუძღვნა ზუსტად ამის გაკეთებას; მხოლოდ გეგმა 86 გვერდს შეადგენს. Anthropic-ის მკვლევარმა ტიანი პენგმა ათობით Claude აგენტი მიმართა მასზე ამის ნაცვლად, პლატფორმაზე, სახელად Prove2Me, რომელიც ინახავს თეორემათა DAG-ს განცხადებებს, რათა აგენტებმა იცოდნენ რა უნდა დაამტკიცონ შემდეგ, რადგან მის გარეშე პირველმა გუნდებმა დაკარგეს თვალყური, ვინ რას ამტკიცებდა, რაც ხდება მაშინ, როცა თქვენი

2:00 ორკესტრირების ფენა არის regex მარკეტინგული ბიუჯეტით. თერთმეტი დღის შემდეგ ძირეულ კვანძზე ეწერა PROVED: ცამეტი მილიონი ხაზი Lean-ში, 29,500 შუალედური თეორემა, დაახლოებით ექვსი მილიარდი გამომავალი ტოკენი შიდა მოდელიდან, რომელიც დაახლოებით შედარებადია Claude Fable 5.1-თან. აგება ვერ ხერხდება, თუ მტკიცებულება ზუსტად Lean-ის სამ სტანდარტულ აქსიომას არ ეყრდნობა: არა, ბოდიში, არანაირი მშობლიური decide, არანაირი მოტყუება. მისი შემოწმება ასევე არ არის იაფი: ნულიდან აშენებას ხუთნახევარი საათი დასჭირდა

2:29 96 ბირთვზე და 153 გიგაბაიტ ოპერატიულ მეხსიერებაზე, და თეორემის სახელები მანქანურად გენერირებულია, ამიტომ რეპოზიციონირება თავის თავს აღწერს, როგორც შემოწმებისთვის დაწერილს და არა წასაკითხად, რასაც მეც ასე აღვწერდი საწარმოო Java-ს. ახლა კი წინააღმდეგობა. Anthropic-ის პოსტი ამბობს, რომ Lean უტყუარად აჩვენებს სისწორეს. კევინ ბაზარდმა, კაცმა, ვინც ამაში დამარცხდა, შეადგინა რეპოზიციონირება 500-გიგაბაიტიან მანქანაზე, რომელიც Anthropic-მა მას მიაქირავა, დაადასტურა მისი შემოწმება და შემდეგ დაწერა, ციტატა, მათემატიკურად ეს ნამუშევარი არსებითად არაფერს გვეუბნება.

2:56 ის უკვე 99.9 პროცენტით დარწმუნებული იყო, რომ თეორემა ჭეშმარიტი იყო, და მტკიცებულება არ ამატებს ახალ მათემატიკას; ის რასაც აჩვენებს, არის ის, რისი გაკეთებაც ავტოფორმალობას შეუძლია ახლა, და ამ ნაწილით ის ნამდვილად აღფრთოვანებულია. მას მილიონი ფუნტი გადაეცათ ხუთი წლის განმავლობაში; Anthropic-ს თერთმეტი დღე დასჭირდა, და კომენტატორის სწრაფი გამოთვლებით ექვსი მილიარდი გამომავალი ტოკენი საბაზრო ფასად ფასდება. დაახლოებით 300 000 დოლარი, ამიტომ მანქანა უფრო იაფი იყო, თუ არ ჩავთვლით მანქანის ვარჯიშს, რასაც არავინ აკეთებს.

3:24 საუკეთესო დეტალი: ელფოსტა მივიდა მაშინ, როდესაც ის უელსში მუსიკალურ ფესტივალზე იმყოფებოდა ერთი 4G ანტენით, მისთვის უცნობი სახელისგან, ამიტომ მან ეს ხუმრობად მიიღო და წაიკითხა ერთი კვირის შემდეგ, რაც სწორი რეაგირებაა ნებისმიერ სათაურზე, რომელიც შეიცავს სრულ ფორმალიზაციას. ამასობაში, ადამიანებმა ერთი გამარჯვება მოიპოვეს. შინ ჯინ-სეომ, Go-ს მსოფლიო ნომერ პირველმა, დაამარცხა KataGo, ყველაზე ძლიერი ღია კოდის Go ძრავა, ორი თამაში ერთი სეულში, ორქვიანი ჰანდიკაპით, დაახლოებით ისეთივე სხვაობა, როგორიც არის ტოპ პროფესიონალსა და ახალბედა პროფესიონალს შორის.

3:50 გადამწყვეტი იყო 11.5 ქულიანი გამარჯვება 221 სვლაში, 99 პროცენტიანი მოგების ალბათობით შუა თამაშიდან მოყოლებული, და მან სახლში წაიღო 250 მილიონი ვონი, დაახლოებით 170 000 დოლარი, პლუს Genesis G90, ამიტომ ჯილდო სუპერადამიანური ხელოვნური ინტელექტის დამარცხებისთვის 170-ჯერ აღემატება Google-ის ჯილდოს Chrome sandbox-ის გაქცევისთვის. მისი განმარტება: თავიდან ის ხელოვნური ინტელექტის სვლებს აკოპირებდა და აგებდა; მან მოიგო დაფის საკუთარი სტილით აგებით, რაც ყველაზე სასარგებლო რჩევაა ხელოვნური ინტელექტის შესახებ, რაც მთელი წლის განმავლობაში მომისმენია, და ის სამაგიდო თამაშიდან მოვიდა. კიდევ ორი სტრიქონი diff-ში.

4:22 Rust React კომპილატორი oxc-დან ახლა მშობლიურია Vite-ში ერთი დროშის მიღმა; 1036-ფაილიანი კოდის ბაზა 14.3 წამიდან 0.81-მდე შემცირდა კომპილაციის ეტაპზე, ძირითადად Babel-ის წაშლით package.json-დან, რაც ასევე ჩემი კანის მოვლის რუტინაა. და IBM-მა გამოუშვა ბობი, ხელოვნური ინტელექტის კოდირების პარტნიორი, რომელიც გესალმება „გამარჯობა, მე ვარ ბობი“, ქმნის ქვეაგენტებს, ათანამედროვებს მეინფრეიმის კოდს, და ავრცელებს ანალიტიკურ პროდუქტს სახელწოდებით Bobalytics, ასე რომ სადღაც ბანკი ძალიან აღფრთოვანებულია და არავის წაუკითხავს ლიცენზია.

4:51 ეს არის დიდი ზღვარი ერთი პარასკევისთვის; თუ გირჩევნიათ ამის წაკითხვა, ვიდრე ჩემი მოსმენა, The Daily Diff თქვენს შემოსულებში ხვდება ყოველ დილით — უფასოდ thedailydiff.dev-ზე, ბმული ქვემოთ. ასე რომ, დღევანდელი ვერდიქტი: SHIP IT. Kernel ამბობს დიახ, Buzzard ამბობს დიახ, მათემატიკა არ შეცვლილა, მაგრამ ის, თუ როგორ ვამოწმებთ მათემატიკას, ახლახან შეიცვალა. ეს არის დღევანდელი diff. მე ვარ ნიკო Axrisi-დან.

5:09 Merge responsibly.

წყაროები

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