350 yıllık bilmece "Fermat'nın Son Teoremi" için bilgisayar destekli ispat hazırlığı
(dongascience.com)Fermat'nın Son Teoremi, bilgisayar diliyle yeniden ispatlanacak
- Imperial College London'dan Prof. Kevin Buzzard, 2024 Ekim ayından itibaren Fermat'nın Son Teoremi (FLT) için Lean teorem ispatlayıcısı ile bir biçimsel ispat yazmayı planlıyor.
- Birleşik Krallık'taki Mühendislik ve Fizik Bilimleri Araştırma Konseyi[EPSRC], Prof. Buzzard'a o aydan başlayarak 5 yıl boyunca araştırma desteği sağlamaya karar verdi.
- Lean blueprints adlı, plasTeX eklentisi kullanılarak hazırlanan proje planının 2024 Nisan ayı sonunda yayımlanması bekleniyor.
Fermat'nın Son Teoremi zaten ispatlanmadı mı?
Evet, ispatlandı. Britanyalı matematikçi Andrew Wiles, ispatı 1994'te duyurdu ve bu ispat 1995'te resmî olarak yayımlandı. Ancak etkileşimli teorem ispatlayıcı[ITP] dilinde yazılmış bir biçimsel ispat hâlâ yok.
Etkileşimli teorem ispatlayıcı? Biçimsel ispat? Bunlar ne?
- Etkileşimli teorem ispatlayıcı[ITP]: İnsanların biçimsel ispat yazmasına yardımcı olan bilgisayar programı. Kanıt asistanı [proof assistant] olarak da adlandırılır.
- Biçimsel ispat: Kanıt doğrulayıcı [proof verifier] adlı bir bilgisayar programıyla doğrulanabilen ispat. Kanıt asistanları genelde kanıt doğrulayıcı işlevini de görür.
Teorem ispatlayıcılar yapay zeka mı?
Nöral teorem ispatlayıcı[NTP] için bu söylenebilir, ancak Lean dahil birçok etkileşimli teorem ispatlayıcı makine öğrenmesi tabanlı programlar değildir.
Lean teorem ispatlayıcısını tanıtır mısın?
- Hem etkileşimli teorem ispatlayıcı hem de saf fonksiyonel programlama dili.
- Bağımlı tip kuramına dayanır.
- Tip sınıfları, genişletilebilir sözdizimi, makrolar ve metaprogramlama gibi özelliklere sahiptir.
- Diğer kanıt asistanlarıyla karşılaştırıldığında, Lean kullanıcıları arasında (matematiğin temelleri dışındaki alanlarda çalışan) matematikçiler özellikle fazladır.
Fermat'nın Son Teoremi için neden biçimsel ispat yazılmak isteniyor?
Prof. Kevin Buzzard'ın X'te paylaştığı gönderiyi alıntılarsak: "Amaç, bilgisayarın modern sayı teorisini anlamasını sağlamak ve sonunda sayı kuramcılarına yardımcı olabilmesini mümkün kılmak."
Bağlantılar
- Kevin Buzzard'ın 3 Ekim 2023'te Lean Zulip sohbetine gönderdiği mesaj: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
- Lean matematik kütüphanesi: https://github.com/leanprover-community/mathlib4
- New Scientist haberi: https://institutions.newscientist.com/article/…
- Popular Mechanics haberi: https://popularmechanics.com/science/math/…
1 yorum
Destekliyorum. Formal proof ile ilgilenenlere, Prof. Terrence Tao'nun Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0) dersini izlemelerini de tavsiye ederim.