ක්ලෝඩ් දින 11කින් ෆර්මැට්ගේ ප්‍රමේයය ඔප්පු කළේය. තීරණය: SHIP IT.

මෙම වීඩියෝවෙන් ආවරණය වන දේ

• ක්ලෝඩ් Lean 4 හි ෆර්මැට්ගේ අවසාන ප්‍රමේයය විධිමත් කරයි
• ක්‍රෝමියම් සැන්ඩ්බොක්ස් 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 Compiler Vite හි native වූ අතර, Hacker News විසින් IBM Bob සොයා ගන්නා ලදී, AI කේතන නියෝජිතයෙක්. ඉන්පසු ක්ලෝඩ් ෆර්මැට්ගේ අවසාන ප්‍රමේයය විධිමත් කළ අතර, එම ඉදිරිපස පිටුවේම කොරියානු මහාචාර්යවරයෙක් පෘථිවියේ බලවත්ම Go එන්ජිම පරාජය කළේය, අද මනුෂ්‍යත්වය දෙකෙන් එකක් විය. මෙම වීඩියෝවේ: ක්ලෝඩ් ඇත්ත වශයෙන්ම ඔප්පු කළේ කුමක්ද, එයට කොපමණ මුදලක් වැය වූවාද,

0:52 ඔහුගේ වෘත්තිය මේ සඳහා වැය කළ ගණිතඥයා පවසන්නේ එය කිසිවක් වෙනස් නොකරන බවත් කෙසේ හෝ සතුටින් සිටින බවත්, Go ක්‍රීඩාවෙන් යන්ත්‍රය පරාජය කළේ කෙසේද යන්නත්. අද සැප්තැම්බර් 4 සිකුරාදා, මෙය The Daily Diff. ෆර්මැට්ගේ අවසාන ප්‍රමේයය: ධන පූර්ණ සංඛ්‍යා a, b, c නොමැත n ට වඩා වැඩි ඕනෑම n සඳහා a හි n ධන b හි n සමාන c හි n තෘප්තිමත් කරයි. ෆර්මැට් එය 1637 පමණ වන විට ආන්තිකයකට සටහන් කර, තම වැඩ පෙන්වීමකින් තොරව මිය ගියේය, ඔහු තම යන්ත්‍රයේ වැඩ කරන බව පවසමින් ටිකට් පතක් වසා දැමූ පළමු සංවර්ධකයා බවට පත් විය. 1908 දී රන් ලකුණු 100,000ක ත්‍යාගයක් එහි පළමු වසර තුළ වැරදි සාධන 621ක් ආකර්ෂණය කර ගත් අතර,

1:25 ඇන්ඩෲ වයිල්ස් අවසානයේ 1995 දී එය ලබා ගත්තේය, විමර්ශකයන්ට සත්‍යාපනය කිරීමට මාස ගණනක් ගත වූ පිටු 129කින්. විධිමත් කිරීම යනු එම සාධනය Lean, සාධන සහායකයෙකුට සෑම පියවරක්ම යාන්ත්‍රිකව පරීක්ෂා කළ හැකි වන පරිදි නැවත ලිවීමයි, Imperial හි කෙවින් බසාර්ඩ් 2024 සිට හරියටම එය කිරීමට මානව උත්සාහයකට නායකත්වය දී ඇත; සැලැස්ම පමණක් පිටු 86කින් යුක්ත වේ. Anthropic පර්යේෂක Tianyi Peng ඒ වෙනුවට ක්ලෝඩ් නියෝජිතයන් දුසිම් ගණනක් ඒ වෙත යොමු කළේය, තේරම් ප්‍රකාශනවල DAG එකක් තබා ගන්නා Prove2Me නම් වේදිකාවක් මත, නියෝජිතයන් ඊළඟට කුමක් ඔප්පු කළ යුතුදැයි දැන ගැනීමට, මන්ද එය නොමැතිව පළමු

2:00 රංචු කවුරුන් කුමක් ඔප්පු කරන්නේද යන්න පිළිබඳව අවධානය යොමු කිරීම අත්හැර දැමූ අතර, ඔබේ සංවිධාන ස්ථරය අලෙවිකරණ අයවැයක් සහිත regex වූ විට මෙය සිදු වේ. දින එකොළහකට පසු මූල නෝඩය PROVED ලෙස කියවන ලදී: මිලියන දහතුනක Lean රේඛා, අන්තර්මධ්‍යම ප්‍රමේය 29,500ක්, ක්ලෝඩ් Fable 5.1 ට සමාන අභ්‍යන්තර ආකෘතියකින් ටෝකන බිලියන හයක් පමණ ප්‍රතිදානය. සාධනය Lean හි සම්මත ප්‍රත්‍යක්ෂ තුන මත පදනම් නොවන්නේ නම් ගොඩනැගීම අසාර්ථක වේ: නැත කණගාටුයි, native decide නැත, වංචා නැත. එය පරීක්ෂා කිරීම ද ලාභදායී නොවේ: මුල සිටම

2:29 ගොඩනැගීමට පැය පහහමාරක් ගත විය 96 cores සහ 153 gigabytes RAM මත, සහ ප්‍රමේය නම් යන්ත්‍රයෙන් ජනනය කර ඇත, එබැවින් repo විසින් එය කියවීමට වඩා පරීක්ෂා කිරීමට ලියා ඇති බව විස්තර කරයි, එය ව්‍යවසාය Java විස්තර කරන ආකාරය ද වේ. දැන් ප්‍රතිවිරෝධය. Anthropic ගේ පළ කිරීම පවසන්නේ Lean නිවැරදි බව සැකයකින් තොරව පෙන්නුම් කරන බවයි. එය අත්පත් කරගත් කෙවින් බසාර්ඩ්, Anthropic ඔහුට ලබා දුන් 500-gigabyte යන්ත්‍රයක repo සම්පාදනය කර, එය පරීක්ෂා කරන බව තහවුරු කර, පසුව ලිවීය,

2:56 උපුටා දැක්වීම, ගණිතමය වශයෙන් මෙම කාර්යය අපට කිසිවක් නොකියයි. ඔහු දැනටමත් 99.9% ක්ම ප්‍රමේයය සත්‍ය බව විශ්වාස කළේය, සහ සාධනය කිසිදු නව ගණිතයක් එකතු නොකරයි; එය පෙන්වන්නේ autoformalization ට දැන් කළ හැකි දේ වන අතර, ඒ කොටස ගැන ඔහු සැබවින්ම උද්යෝගිමත් වේ. ඔහුට වසර පහක් පුරා පවුම් මිලියනයක් ලබා දෙන ලදී; Anthropic හට දින එකොළහක් ගත විය, සහ අදහස් දක්වන්නෙකුගේ ගණනය කිරීම් අනුව ටෝකන බිලියන හයක් ලැයිස්තු මිලට සමාන වේ. ආසන්න වශයෙන් ඩොලර් 300,000ක්, ඒ නිසා යන්ත්‍රය ලාභදායී විය, ඔබ යන්ත්‍රය පුහුණු කිරීම ගණන් නොගන්නේ නම් මිස, එය කිසිවෙකු කරන්නේ නැත.

3:24 හොඳම විස්තරය: ඔහු වේල්සයේ සංගීත උළෙලක සිටින විට විද්‍යුත් තැපෑල ලැබී ඇත. 4G එක් තීරුවකින්, ඔහු කිසිදා අසා නැති නමකින්, ඒ නිසා ඔහු එය පිස්සුවක් ලෙස බැහැර කළේය. සතියකට පසුව එය කියවා, එය ඕනෑම විෂය මාතෘකාවකට නිවැරදි ප්‍රතිචාරයයි. අන්තයෙන්-අන්තය දක්වා විධිමත් කිරීම අඩංගු වේ. මේ අතර, මිනිසුන් එකක් ආපසු ලබා ගත්හ. Go හි ලෝකයේ අංක එකේ Shin Jin-seo, KataGo පරදවා ඇත. ශක්තිමත්ම විවෘත මූලාශ්‍ර Go එන්ජිම, සෝල් හි ක්‍රීඩා දෙකක් එකකට, ගල් දෙකක ආබාධයක් සහිතව, ඉහළ වෘත්තිකයෙකු සහ නවක වෘත්තිකයෙකු අතර පරතරය ආසන්න වශයෙන් සමාන වේ.

3:50 තීරණාත්මක තරගය 11.5-ලකුණු ජයග්‍රහණයක් විය, චලනයන් 221කින්, එයින් තරගය මැද සිට 99%ක ජයග්‍රාහී සම්භාවිතාවක් පවත්වා ගෙන ගියේය, ඔහු මිලියන 250ක් දිනා ගත්තේය. වොන්, ඩොලර් 170,000ක් පමණ, ප්ලස් Genesis G90 එකක්, ඒ නිසා ත්‍යාගය අධි-මානුෂික AI පරාජය කිරීම Google හි Chrome sandbox එකකට ඇති ත්‍යාගයට වඩා 170 ගුණයක් වැඩියි. ගැලවීම. ඔහුගේ පැහැදිලි කිරීම: මුලදී ඔහු AI චලනයන් පිටපත් කර පරාජය විය; ඔහු ජයග්‍රහණය කළේ ඔහුගේම ශෛලියකින් පුවරුව ගොඩනැගීමෙන්, එය AI ගැන මා ලද වඩාත්ම ප්‍රයෝජනවත් උපදෙස්ය. මම මේ වසර පුරාම අසා ඇත, එය පුවරු ක්‍රීඩාවකින් පැමිණියේය. වෙනසෙහි තවත් පේළි දෙකක්.

4:22 oxc හි Rust React Compiler දැන් Vite හි එක් කොඩියක් පිටුපස ස්වදේශීයයි; අ ගොනු 1,036ක කේත පදනමක් තත්පර 14.3 සිට 0.81 දක්වා අඩු විය. සම්පාදන පියවරේදී, බොහෝ දුරට Babel ඉවත් කිරීමෙන් package.json, එය මගේ සම ආරක්ෂණ චර්යාව ද වේ. තවද IBM විසින් Bob දියත් කරන ලදී, ඔබට Hi, සමඟින් ආචාර කරන AI කේතන සහකරුවෙකි. මම Bob, උප-ඒජන්සි බිහි කරයි, මේන්ෆ්‍රේම් කේතය නවීකරණය කරයි, සහ Bobalytics නම් විශ්ලේෂණ නිෂ්පාදනයක් නිකුත් කරයි, එබැවින් කොතැනක හෝ බැංකුවක් ඉතා උද්යෝගිමත් වන අතර කිසිවෙකු බලපත්‍රය කියවා නැත.

4:51 ඒ එක් සිකුරාදාට විශාල මායිමකි; මට කියනවාට වඩා මෙය කියවීමට ඔබ කැමති නම්, වෙනස සෑම උදෑසනකම ඔබගේ එන ලිපි වෙත පැමිණේ - daily diff dot හි නොමිලේ dev, පහත සබැඳිය. එබැවින්, අද තීන්දුව: එය නැව්ගත කරන්න. කර්නලය ඔව් කියයි, Buzzard ඔව් කියයි, ගණිතය වෙනස් වී නැත. නමුත් අපි ගණිතය පරීක්ෂා කරන ආකාරය දැන් වෙනස් විය. ඒ අද දවසේ වෙනසයි. මම Axrisi හි Niko.

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