Lean v4.35.0 doğrulanmış yeni çekirdeklerle yayımlandı

Lean ekibi, yapay zeka ajanlarının yazılımdaki açıkları bulma konusundaki etkinliğinin artması üzerine Lean kanıt asistanı için doğrulanmış yeni çekirdekler sundu. Lean v4.35.0 sürümüyle birlikte dağıtıma eklenen araçlar, projelerin bağımsız ve resmi çekirdeklerle harici olarak yeniden doğrulanmasını sağlıyor. Güncelleme kapsamında sisteme "lake check" komutu eklenirken kullanıcıların kanıtlarını yalıtılmış bir ortamda güvenle denetlemesine imkan tanındı.

Yeni sürüm; nanoda, lean4lean, con-leche ve con-ron olmak üzere dört ek çekirdek içeriyor. Lean diliyle yazılan ve tutarlılığı kanıtlanan ilk çekirdek olan con-leche, yapay zeka desteğiyle geliştirildi ve Lean FRO bünyesindeki Joachim Breitner denetiminde doğrulandı. Tüm Mathlib kütüphanesini sekiz iş parçacığıyla yaklaşık 100 saniyede denetleyen çekirdek, resmi çekirdeğe kıyasla yüzde 31 daha az komut çalıştırıyor. Çalışma zamanı ve derleyici hatalarını önlemek için con-leche'nin Rust sürümü olan con-ron çekirdeği de dağıtıma dahil edildi.

Lean FRO, lean4lean çekirdeğinin doğrulama sürecinin birkaç ay içinde tamamlanacağını ve doğrulanmış çekirdek sayısının üçe çıkacağını açıkladı. Geliştiriciler ayrıca devasa boyutlara ulaşan matematik kütüphanelerini denetleyebilmek adına ölçeklenebilirlik sorunlarına odaklanıyor. Anthropic'in 13 milyon satırı aşan FLT projesi ve 50 milyon satırlık Courtade-Kumar deposu gibi büyük yapılar için ikili dışa aktarma formatları ve artımlı denetim mekanizmaları üzerinde çalışılıyor.