Hangi hata basit bir dikkatsizliktir

Hangi hata basit bir dikkatsizliktir

Ana noktalar

1. Bir tanımda ya da ispatta bulunan bir hata, düzeltilmesi kolay olsa bile fark edilmesi zorsa, bu hata basit değildir.
2. Bazı hatalar ancak ispat asistanlarının yardımıyla bulunabilir.

Kısa metin

• Geçen yılın Aralık ayından bu yıl 16 Nisan'a kadar yaklaşık 170 saat harcayarak Lean ispat asistanı için standart kütüphane içindeki String.splitOn_of_valid teoremini kanıtladım.
• Bu teoremi kanıtlarken String.splitOn fonksiyonunun tanımında bir hata keşfettim.
• Bu hatayı düzeltmek çok zor değildi. İlgili tanımda i yerine yalnızca i - j yazmak yeterliydi.
• Ama bu, söz konusu hatanın basit bir dikkatsizlik olduğu anlamına gelmiyor. Çünkü bu tanıma göre splitOn fonksiyonu çoğunlukla doğru çalışsa da, bazı özel durumlarda yanlış sonuç üretiyor.
• Lean gibi bir ispat asistanı kullanmasaydım, böylesine incelikli bir hatayı asla bulamazdım.