MaxCut, çizge teorisinde önemli bir kombinatoryal optimizasyon problemidir ve çizgedeki kenarları iki ayrı küme arasında bölen en büyük kesimi bulmayı hedefler. Çizelgeleme, bölümlendirme ve finansal portföy optimizasyonu gibi çeşitli alanlarda uygulamaları bulunur. Problem NP-Zor olmasına rağmen, pratikte iyi sonuçlar veren yaklaşık algoritmalar mevcuttur. Bu makale, MaxCut için basit bir rastgele yaklaşım algoritmasını ve bu algoritmanın beklenen performans sınırlarının nasıl kanıtlandığını ele almaktadır.
Algoritma oldukça basittir: bir çizgedeki her bir köşeyi %50 olasılıkla iki kümeden (A veya B) birine atar. Bu rastgele atama, bir kesim oluşturur. Makale, bu algoritmanın beklenen kesim boyutunun, toplam kenar sayısının yarısı kadar olduğunu matematiksel olarak kanıtlar. Doğrusallık beklentisi ilkesini kullanarak, herhangi bir kenarın kesimde olma olasılığının 1/2 olduğu gösterilir. Bu da algoritmanın, optimal kesimin en az yarısı kadar bir kesim boyutu sağlayacağını garanti eder.
Yazar, algoritmalar dersinde karşılaştığı bu zarif algoritmayı ve kanıtını Lean4 adlı programlama dili ve kanıt asistanı ile biçimselleştirmeye karar vermiştir. Lean4, matematiksel ve bilgisayar bilimi kavramlarını biçimsel olarak doğrulamak için kullanılan güçlü bir araçtır. Bu çalışma, rastgeleleştirilmiş algoritmaların biçimsel doğrulamasına olan ilgiyi ve MathLib ile CSLib gibi kütüphanelerdeki gelişmeleri vurgulamaktadır. Bu tür biçimselleştirmeler, algoritmaların doğruluğunu kesin bir şekilde kanıtlama ve güvenilirliğini artırma potansiyeli taşır.
Bu çalışma, rastgele algoritmaların teorik garantilerini biçimsel doğrulama araçlarıyla kanıtlamanın önemini ve potansiyelini göstermektedir.