Lean teorem sübutçüsü etibarlılıq suallarının qarşısında durur, AI avtoformalizasiya inkişaf edərkən

Formalizasiya və avtoformalizasiya

Lean, riyaziyyatçı Thomas Halesin qonaq yazısına görə riyaziyyatçılar arasında ən məşhur teorem sübutçüsü oldu. Onu Leo de Moura 2013-cü ildə Microsoft-da işləyərkən yaratdı; Microsoft daha sonra proqramı açıq kod ilə nəşr etdi. Lean növ nəzəriyyəsinə, daha dəqiq, induktiv qurmalar hesablaması dialektikasına əsaslanır. 2017-ci ildə başlayan ümumi kitabxanası mathlib indiyə qədər təxminən 300 000 teorem, 100 000-dən çox müəyyən, 2,5 milyon kod sətri və 700-dən çox iştirakçı əhatə edir. mathlib-in istənilən teoremi sonrakı sübutlərdə yenidən sübut etmək əvəzinə istinad edilə bilər.

Avtoformalizasiya, AI məqalə oxuyub formal sübut hazırladığı halda, 2026-cı ildə praktiki reallığa çevrildi. Əhəmiyyətli mərhələlər: Math Inc.-in 2025-ci il sentyabrda səthi ədədlər teoremi üzrə yarı-avtoformalizasiyası, Munkres topologiya dərsliyinin hissəsinin böyük formalizasiyası, 24 ölçülə sferlərin bükülməsi məsələsi, Anthropic-in 4 sentyabrda Ferma son teoremi üzrə avtoformalizasiyası — 11 gün ərzində 13 milyon sətr Lean kodu istehsal etdi — və OpenAI-in 8 sentyabrda elan edilən Navier-Stokes partlaması formalizasiyası.

Dizayn və etibarlılıq modeli

Lean ümumi təyinatlı proqramlaşdırma dilini riyaziyyat dili ilə birləşdirir — müəyyənlər, teorem ifadələri və sübut skriptləri üçün. Sübut skriptləri Lean nüvəsi tərəfindən təhlil edilə, emal və yoxlanır, bir neçə min C++ kod sətri ilə. Yazıda vurğulanıb ki, Lean sübutları heç vaxt nüvənin yoxlamasından əvvəl saxlanmamalıdır və sübut edilən teoremın riyaziyyatçılar nəzərində olanı olduğunu təsdiq etmək üçün ayrı insan auditu lazımdır.

Etibarlılıq problemlərinin yayı

Etibarlılıq problemi "False" sübutunu buraxan nüvə problemidir və görə hər hansı iddianın sübutunu verir. Bir neçə belə problem 2026-cı il iyul və avqustda Lean-də aşkar edildi ki, indi "etibarlılıq problemlərinin yayı" adlanır. Bir problem Kolatsi hipotezinin qeyri-qanuni rəddinə, digəri isə Kepler hipotezinin qısa qeyri-qanuni sübutuna səbəb oldu. Hamısı tez düzəldildi və mathlib düzəldilmiş nüvə ilə yoxlandı.

Təkliflər və açıq problemlər

Üç cavab nəzərdən keçirilir. Birincisi, əlavə Lean nüvələri yazın və sübutları qarşılıqlı yoxlayın; təxminən 25 nüvə mövcuddur və Navier-Stokes formalizasiyası ondan çox sübut yoxlayanı təsdiqlədi. İkincisi, nüvəni Joachim Breitner-in Con-Leche ilə etdiyi kimi formal yenidən yoxlayın — sübut edilmiş Lean nüvəsi ilə, ardıcıllığı Claude tərəfindən yaradılmış və mathlib-i yoxlamışdı. Üçüncüsü, Lean növ nəzəriyyəsinin nəzəri başa düşüşünü dərinləşdirin; unikal tipləşdirmə, Pi-nin həqiqəti, dəyişdirilmiş Church-Rosser xüsusiyyəti və tam açıq nisbəti ardıcıllığın sübutu hələ açıqdır. Yazı Ken Thompson-un "Reflections on Trusting Trust" sitatı ilə başa çatır və Lean kimi sistemlərə kor etibar mümkün deyil deyə xəbərdar edir.

Mənbələr: terrytao.wordpress.com