Fermat'nın Son Teoremi'nin biçimselleştirilmesinde son durum

 (xenaproject.wordpress.com)
2 puan yazan GN⁺ 2024-12-13 | 1 yorum | WhatsApp'ta paylaş
  • FLT ispatını Lean'e aktarma çalışması ikinci ayında; Wiles'ın “R=T” teoremi için gereken R ve T tanımları henüz tamamlanmadı, ancak soyut değişmeli cebire ait bir sonuç şimdiden ispatlandı
  • Amaç, 1990'lardaki özgün ispatı aynen kopyalamak değil; Diamond/Fujiwara, Kisin, Taylor, Scholze ve diğerlerinin sonraki çalışmalarıyla genelleştirilmiş ve sadeleştirilmiş ispatı Lean ve mathlib üzerinde kurmak
  • Modern ispat için gereken crystalline cohomology biçimselleştirilirken, divided power yapılarının standart literatürü olan Roby'nin 1965 tarihli makalesinde kilit bir yardımcı önermenin hatalı göründüğü ortaya çıktı
  • Brian Conrad, Berthelot-Ogus kitabının ekinde alternatif bir ispat buldu; Arthur Ogus da bu ekteki hataları nasıl düzelteceğini bildiğini söyleyince proje yeniden ilerleyebilir hale geldi
  • Bu örnek, modern matematikte ayrıntılı ispatların uzman hafızasına ve örtük bilgiye dayanmasının riskini gösteriyor; ispatları biçimsel sistemlere kaydetmenin pratik gerekçesini güçlendiriyor

Lean ile FLT ispatını aktarmada mevcut durum

  • Fermat'nın Son Teoremi (FLT) ispatını bilgisayara öğretme çalışması ikinci ayında
  • Wiles ispatının merkezindeki “R=T” teoreminde R ve T'nin ne olduğunu Lean'de tanımlamak ciddi çalışma gerektiriyor; iki tanım da henüz tamamlanmış değil
  • Doktora öğrencisi Andrew Yang, gereken soyut değişmeli cebir sonucunu şimdiden ispatladı
    • Bu, “soyut halkalar R ve T bir dizi teknik koşulu sağlıyorsa birbirine eşittir” biçiminde bir sonuç
  • Mevcut taslak blueprint olarak yayımlanmış durumda
  • Kullanılan sistem Lean ve matematik kütüphanesi mathlib
  • Lean ve sayılar teorisi hakkında biraz bilgisi olanlar contribution guidelines, project dashboard ve issue üzerinden katkıda bulunabilir

1990'lardaki ispat neden aynen aktarılmıyor

  • Proje, Wiles'ın 1990'lardaki ispatını aynen biçimselleştirmiyor
  • Sonrasında Diamond/Fujiwara, Kisin, Taylor, Scholze ve diğerlerinin çalışmalarıyla ispat daha genelleştirilip sadeleştirildi
  • Amaç yalnızca FLT'yi ispatlamakla kalmayıp, Lean içinde daha genel ve güçlü sonuçlar da inşa etmek
  • Yapay zeka matematik devrimi gerçekten yaşanır ve Lean önemli bir bileşen haline gelirse, bilgisayarın modern sayılar teorisinin temel tanımlarını anlayabileceği bir biçimde barındırması faydalı olabilir

Crystalline cohomology için gereken divided powers

  • Biçimselleştirilmeye çalışılan ispatta, Wiles'ın özgün ispatında bulunmayan crystalline cohomology kullanılıyor
  • Bu teori 1960'lar ve 70'lerde Paris'te gelişti; Grothendieck'in fikirlerine dayanarak temellerini Berthelot attı
  • Klasik üstel fonksiyon ve logaritma fonksiyonu, diferansiyel geometriyi ve de Rham cohomology'yi anlamada önemlidir; ancak characteristic p gibi aritmetik durumlarda aynı şekilde işlemez
  • 1960'lardaki Roby makalelerinde geliştirilen divided power structures, aritmetik durumlarda kullanılabilecek benzer fonksiyonlar kurmada kilit rol oynar
  • Lean'e crystalline cohomology öğretmek için önce divided powers'ın biçimselleştirilmesi gerekir

Lean çalışması sırasında Roby literatüründe ortaya çıkan sorun

  • Antoine Chambert-Loir ve Maria Ines de Frutos Fernandez, Lean'de divided powers teorisini biçimselleştiriyordu
  • Yaz boyunca Lean, standart literatürdeki insan tarzı argümanda bir sorun ortaya çıkardı; doğrulama sonucunda Roby'nin çalışmasındaki kilit bir yardımcı önermenin hatalı göründüğü anlaşıldı
  • Teknik olarak Berthelot'nun makalesi, divided powers teorisini sıfırdan geliştirmiyor; Roby'nin “Les algebres a puissances divisees” çalışmasını kullanıyor
    • Bu makale Bull Sci Math, 2ième série, 89, 1965, s. 75-91'de yayımlandı
    • s. 86'daki Lemme 8 yanlış görünüyor; ispatın nasıl düzeltileceği de açık değildi
    • Bu ispat, Roby'nin 1963 tarihli Ann Sci ENS makalesindeki başka bir yardımcı önermeye yanlış atıf yapıyor
    • Doğru önerme Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), ancak uygulama sırasında bir tensor product eksik kalmıştı
  • Bu sorun, bir module'ün divided power algebra'sının divided powers'a sahip olduğuna dair Roby ispatını bozdu ve bunun sonucunda A_cris halkasının tanımlanmasını engelledi

“Teori yanlış”tan çok “ispatta boşluk var” durumu

  • Bu, crystalline cohomology'nin kendisinin fiilen yanlış olduğu anlamına gelmiyor
  • Ana teoremler hâlâ doğru görünüyor; ancak Antoine ve Maria Ines'in izlediği ispat eksikti
  • Roby, Grothendieck ve Berthelot'un hepsi vefat ettiği için asıl uzmanlara doğrudan sormak mümkün değildi
  • Birçok uzman, ara yardımcı önerme yanlış olsa bile ana sonucun ispatının düzeltilebileceğini düşünüyor
  • Biçimselleştirmede “düzeltilebilir olmalı” yargısı yeterli değildir; gerçekten düzeltilmiş bir ispat gerekir

Berthelot-Ogus ekiyle açılan dolambaçlı yol

  • Tadashi Tokieda bu hikâyeyi Stanford'da Brian Conrad'a aktardı; Conrad da crystalline cohomology'nin yanlış olduğu söylenen meselenin ne olduğunu sordu
  • Teknik ayrıntıları dinleyen Conrad, bir sorun var gibi göründüğünü kabul etti ve incelemeye başladı
  • Birkaç saat sonra Conrad, Berthelot-Ogus'un crystalline cohomology kitabının ekinde, bir module'ün universal divided power algebra'sının divided powers'a sahip olduğuna dair başka bir ispat bulunduğunu bildirdi
  • Conrad'ın bakış açısından bu yaklaşım iyi görünüyordu ve bu sayede ispat yeniden ilerleyebilir hale geldi
  • Daha sonra Berkeley'de Arthur Ogus ile öğle yemeğinde bu ekin sorunu çözdüğünü anlatınca Ogus, o ekte de birkaç hata olduğunu, ancak bunları nasıl düzelteceğini bildiğini söyledi

Modern matematik literatürü neden biçimselleştirmeye ihtiyaç duyuyor

  • Bu süreç, insanların modern matematiği belgeleme biçiminin yeterince sağlam olmayabileceğini gösteriyor
  • Pek çok olgu “uzmanların bildiği şey” olarak kalıyor ve literatürde tam olarak düzenlenmiş olmayabiliyor
  • Önemli fikirler bu tür sarsıntılara dayanacak kadar sağlam olsa bile, fiili ayrıntılı ispat beklenen yerde bulunmayabilir
  • Matematiği biçimsel sistemlere düzgün biçimde kaydetmek hata olasılığını büyük ölçüde azaltabilir
  • Biçimci olmayan matematikçiler için bile, makinelerin insan argümanlarını öğrenip kendi başına matematik yapmasını istiyorsak önce argümanları makineye öğretme süreci gerekir
  • Maria Ines, Cambridge Formalization of Mathematics seminar'da divided powers biçimselleştirmesi üzerine sunum yaptı; söz konusu sorunların çözüme kavuşturulduğu anlaşılıyor
  • Proje yeniden rayına oturdu, ancak literatürün tekrar engel çıkarma olasılığı hâlâ var

İlgili okumalar

1 yorum

 
GN⁺ 2024-12-13
Hacker News yorumları

  • Lisansüstü öğrenciliğimde danışman hocamın Birch–Swinnerton-Dyer sanısı için yaptığı hesaplamalı yaklaşımı desteklemek amacıyla hızlı kod yazdığım günleri hatırladım
    Yakın bir şehirdeki sayılar kuramı seminerinde bana “sanıyı destekleyen kanıtları güçlendirmeye mi çalışıyorsun?” diye sormuşlardı; ben de gülerek “Hayır, daha çok bir karşı örnek bulmak istiyorum” diye cevap verince uzmanlar epey öfkelenmişti
    Sayılar kuramı o kadar eski ve derin bir alan ki, bu konuda doktora tezi yazmak bile acemiliğin ilk adımı gibi geliyor; gösterimleri ve tanımları bilseniz de onların altındaki sezgiye ulaşmak kolay değil
    Bu yüzden uzmanların “karşı örnek umuyorum” sözüne gösterdiği öfke bende korkudan çok merak uyandırdı; henüz söze dökemedikleri ama gördükleri şeyin ne olduğunu merak ettim
    Bu tür formelleştirme ilerlemeleri, programlamaya daha aşina insanlar için matematiği çok daha erişilebilir hale getiriyor
    Yeterince biçimsel olmama konusundaki kaygı haklı, ama bence bu kaygıya verilecek doğru tepki kaçınmak değil, merak duymaktır

    • Sayılar kuramcısı değilim ama o uzmanlar muhtemelen henüz kanıtlanmamış bir sanıya araştırma hayatlarının fazlasıyla büyük bir kısmını yatırmışlardı
      Sizin gibi toy bir yeni gelenin kaba hesaplamalarla bir karşı örnek bulup bir gecede ünlü olması, bütün o emeklerini ve kurdukları yapıyı bir anda yıkabilirdi; bu yüzden kızmış olmaları muhtemel
      Geçmişteki genç halime matematik yüksek lisansı konusunda tavsiye verecek olsam, önemsiz olmayan her “X'i kanıtla” ödevinde zamanın en az dörtte birini karşı örnek aramaya ayırmasını söylerdim
      Ödevlerde bunun %99'unda başarısız olursunuz, ama problem hakkındaki sezginiz çok daha derinleşir; kalan %1'lik durumda ise dahi gibi görünebilirsiniz
      Gerçek matematik araştırmasına geçtiğinizde bu olasılık, karşı örnek öncelikli yaklaşım lehine çok daha fazla değişir

  • Öğrenciyken bir arkadaşım, birinin seminerin ilk gününü tamamladığını ve herkesin onun Fermat'nın Son Teoremini kanıtlayacağı düşüncesiyle heyecanlandığını anlatmıştı
    O kişi Andrew Wiles'dı; sonra yayımdan önce bulunan bir sorunu birkaç ay boyunca düzelttikten sonra çalışma nihayet bütünüyle yayımlandı
    Matematik okuyan biri olarak bu inanılmaz derecede heyecan verici bir olaydı; bu yüzden “eski usul 1990'lar kanıtı” ifadesini görünce kendimi gerçekten yaşlı hissediyorum

    • 90'larda Berkeley'de bilgisayar bilimi lisans öğrencisiydim ve ileri düzey matematik dersleri alıyordum; o sırada yeni ve heyecan verici olan bu eski kanıtı birlikte takip etmiştik
      Sınıfın neredeyse tamamı matematik lisansüstü öğrencilerinden oluşuyordu ve sanırım materyalin %20'sini bile anlayamamıştım
    • Bu hikâyeyi ele alan harika bir TV belgeseli vardı

  • Lean'in bazen yaptığı sinir bozucu şeyi yapmış olması hoşuma gitti: standart literatürdeki insan usulü argüman sunumundan şikâyet etmiş ve yakından bakınca insan argümanında gerçekten eksik parçalar olduğu görülmüş
    Şakayla karışık söylenen bu rahatsızlığın ötesinde, bu çok büyük bir başarı ve Lean ile diğer teorem ispatlayıcıların gelecekte matematikte önemli araçlar haline geleceğini düşünüyorum

    • Derleyiciler de tam olarak aynı alışkanlığa sahiptir

  • Modern matematik dokümantasyonunun yetersizliği kısmı bana UI/UX/web tasarımını hatırlatıyor
    Tasarımcı, biçimsel olmayan ve tam kesinlik taşımayan mockup'lar, prototipler ve etkileşim akışları üretip bunları geliştiriciye teslim ediyor; geliştirici de bunları kod içinde formelleştirip makineye tam olarak anlatmak zorunda kalıyor
    Bu süreçte tasarımın hesaba katmadığı etkileşim senaryoları veya kod yolları gibi boşluklar kaçınılmaz olarak ortaya çıkıyor; bazen büyük tasarım kusurları görünür hale geliyor ve geliştirici ya da tasarımcı bunları kapatmak zorunda kalıyor
    Tasarım ve geliştirme farklı roller ve farklı düşünme biçimleri gerektirir; çoğu tasarımcı da geliştiriciler gibi çalışmaya ve düşünmeye güçlü biçimde direnç gösterir

    • “Matematiği düzgün biçimde, yani formel bir sistem içinde kayda geçirelim” girişimini daha önce Hilbert denemişti ve başarısız olmuştu
      Bu başarısızlıktan sonra matematiği tamamen formelleştiremeyeceğimizi öğrendik; bu da yapay zeka ile matematik yapmaya yönelik yaklaşımın temel sorununa işaret ediyor

  • Bu konuyla ilgileniyorsanız gerçek koda bakmak iyi olur
    Örneğin: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
    Kodun genel yapısını açıklayan plan da bakmaya değer: https://imperialcollegelondon.github.io/FLT/blueprint/
    Dışarıdan bakan biri olarak Lean kodunun nasıl göründüğünü ve insanların nasıl katkıda bulunduğunu görmek bana çok ilginç geliyor
    Birim testlere ihtiyaç olmaması da hoşuma gidiyor. Bir anlamda, nihai ispat önermesi birim testin kendisi

    • Büyük Lean projelerinin çoğunda yine de “birim testler” vardır
      Örneğin, bir tanımın boş olmadığını kontrol etmeye yarayan basit örnekler ve karşı örnekler bu rolü oynar

  • Saf matematik yapmış biri olarak, büyük sorun matematikçilerin neredeyse hiç kendi kendine yeterli ispatlar sunmaması
    Bunu yapmaları için bir teşvik yok ve yazarların “ayrıntılar atlandı” ifadesiyle gurur duyduğu durumlar bile var
    Sonuçta, tüm mantıksal adımların izlenebildiği titiz bir ispat istiyorsanız, literatürde kolayca bulunmayan boşlukları bir uzmanın doldurması gerekiyor
    Bu, ancak böyle birinin her şeyi açıklayan bir kitap yazmasıyla mümkün hale gelebiliyor; bazen o bile yeterli olmuyor
    Sadece kayda geçmiş olana bakınca, modern matematiğin büyük bir kısmı istikrarsız bir temel üzerinde duruyor gibi görünüyor

    • Şu anda saf matematik araştırmacısı olarak bunun doğru olduğunu söyleyebilirim, ama kolay çözülecek bir mesele olduğunu sanmıyorum
      Matematik araştırma makaleleri o alandaki diğer uzmanlar için yazılır ve bazen ayrıntı çok az olduğundan hakemlikte sık sık bundan şikâyet ederim
      Ama bütün ayrıntıları gerçekten verirseniz makale çok daha uzun olur
      Lise matematik altyapısı sağlam olan birinin çözebileceği bir örnek olarak, bazı reel sayılar x > X için log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx olacak şekilde C, X > 0 sabitlerinin var olduğunu ispatlama problemi verilebilir
      Bu tür önermeler analitik sayı teorisinde sürekli ortaya çıkar ve uzman için apaçıktır, bu yüzden makalelerde neredeyse her zaman ispatsız yazılır
      Tam ve titiz bir ispat yazarsanız uzun ve sıkıcı olur, hiçbir uzman da onu okumak istemez
      Bu yaklaşımın bir ödünleşim maliyeti var, ama yönetilebilir düzeyde görünüyor
    • Birinin ünlü bir matematikçinin, sanırım Euler’in çalışmalarını derlerken çok sayıda hata bulduğuna dair bir hikâye var; bunların bazıları oldukça ciddiydi ama teoremlerin kendisi yine de doğruydu
      Bu, Tao’nun sözünü ettiği üçüncü aşama olan bilgili sezgi gibi geliyor
    • Uzun zaman önce matematik okumuştum; bir profesör ayrıntılarla uğraşmamayı gururla anlatırdı
      “Bir şeyi 100 kez yaptıysan, ‘kolayca görülebileceği gibi’ deyip geçebilirsin” derdi
    • Matematik geçmişim yok, o yüzden safça bir düşünce olabilir ama bir ispat denetleyicisinin bir teorem veritabanına sahip olup ara adımları tamamlayabildiğini ya da eksik adımları doldurabildiğini doğrulayabilmesi gerekmez mi diye düşünüyorum
      Yani bunu, zihninde bir veritabanı taşıyan bir insanın belirli bir teoremin önkoşullarıyla sonraki cümlenin sonucunun uyuşup uyuşmadığını bulması gereken iş olarak anlamıştım
      Ya da mevcut ispat denetleyicilerinin değerlendirebileceği biçimde ifade edilemeyen matematik var mı diye merak ediyorum
      Belki de ispat denetleyicilerinin kullanımı düşündüğüm kadar yaygın değildir. Programlamadaki statik tipli dillerin konumuna benziyor gibi geliyor
    • Bu yaklaşımın pratikte gerçekten büyük bir patlamaya yol açtığı oldu mu diye merak ediyorum
      Yani, el sallayıp geçilen bir bölüm yüzünden yaygın kabul görmüş bir ispatta ölümcül bir kusur çıktığı örnekler oldu mu diye soruyorum
      Böyle bir şey hiç olmadıysa, ayrıntıları açıkça yazma konusunda neden gevşek davranıldığını da anlayabilirim

  • “crystalline cohomology 1970’lerden beri çok fazla kullanıldı; bir sorun olsaydı çoktan ortaya çıkardı” şeklindeki sezginin gerçekten doğru olup olmadığını hep merak etmişimdir
    Kusurlu bir ispatın üzerine matematiğin bütün bir alanı inşa edilip o alanın gerçekten sadece yanlış çıkması o kadar imkânsız mı

    • Başka yerde de söylediğim gibi, Vladimir Voevodsky’nin Homotopy Type Theory ve Univalent Foundations programını başlatmasının büyük nedenlerinden biri buydu
      Kendisi, temel bir makalenin “ilk sayfasındaki ilk yardımcı lemmadaki” bir hata yüzünden bir alanın çöktüğünü bizzat görmüştü
      UniMath üzerindeki ilk çalışmalar, IAS’teki özel yıl ve ardından HoTT kitabına uzanan akışın, matematiğin biçimselleştirilmesi konusunu bugün bulunduğu noktaya taşıdığını söyleyebilirsiniz
    • İnsanlar üzerinde çalıştıkları ispatlara karşı örnek arar
      Temel yanlışsa, bu karşı örneklerden biri temel teoremi de çürütebilir; dolayısıyla yanlış bir temel üzerine inşa etmek, aslında o temeldeki kusuru ortaya çıkarma olasılığını artırır
      Benzer şekilde, matematik bazen tahmin üretmek için uygulanır; matematik yanlışsa tahminler de yanlış olur ve bu yanlış tahminler çok dikkat çeker
    • Bunun, o matematik alanının ne kadar yaygın kullanıldığına bağlı olduğunu düşünüyorum
      Aslında “alan” sözcüğü biraz yanıltıcı; birçok teori, matematiğin genelindeki başka teorilerle bağlanmış bir düğüme daha çok benzer
      O teoriler de başka teorilerle bağlantılıdır
      Bu düğümün diğer kısımlarını hiç etkilemeden yalnızca temelin mantıksal olarak çökmesi çok tuhaf bir durum olurdu
      İçten içe tamamen tutarlı ama sadece tek bir hatası olan, devasa ve havada duran bir matematik kütlesini bu yazıdaki kohomoloji örneğinde hayal etmek zor
      Kesin konuşmak gerekirse bu daha çok felsefi bir tutum, ama günümüzde matematiğin büyük kısmının bir anlamda doğal biçimde keşfedildiğine inanmak istiyorum
    • Bunun örnekleri geçmişte de oldu; Vladimir Voevodsky’nin biyografisine bakabilirsiniz
      Spoiler vermek gerekirse, dünya yine de dönmeye devam etti

  • Son yaklaşık 1 yıldır lisans düzeyi karmaşık analiz dersinin bazı kısımlarını Lean ile biçimselleştirmeyi aralıklı olarak deniyordum
    Öğrenecek çok şey vardı ve ödüllendiriciydi, ama zaman zaman da sinir bozucuydu
    Ancak yakın zamanda, C*'den (-pi,pi] x R'ye giden bir birebir-örten eşleme olarak kutupsal biçimi tamamen tanımlayabildim; çünkü karmaşık sayılar, kuvvet serileri, exp ve sin mathlib'de zaten varken bunları “sıfırdan” tanımlamakta ısrar ettim
    Zorlukların önemli bir kısmı muhtemelen yalnızca matematik lisansına sahip olmamdan, Lean/mathlib'e alışkın olmamamdan ve yol gösterecek kimsenin olmamasından kaynaklandı. Yine de Zulip topluluğu çok yardımcı oldu
    mathlib'deki birçok sonuç oldukça soyut biçimde ifade ediliyor; bu yüzden bunların standart lisans düzeyi teoremlerle nasıl bağlantılı olduğunu ya da böyle teoremlerin mathlib'de bulunup bulunmadığını anlamak zor
    Bu, araştırma matematiği topluluğu için makul olabilir, ama benim için büyük bir engeldi ve Lean eğitimde daha fazla kullanılırsa benzer bir sorun olabilir. Yine de zamanla düzeltilebilecek bir şey
    Kanıt otomasyonu bana göre hâlâ yeterince iyi değil
    Gereğinden fazla şey, olması gerekenden daha zor kanıtlanıyor ve özellikle tip dönüşümü en büyük şikâyetim
    Normal matematikte reel sayılar karmaşık sayıların bir altkümesi olduğundan, tüm karmaşık sayılar için doğru olan bir şey otomatik olarak tüm reel sayılar için de doğrudur; ama Lean'de bunlar farklı tipler ve aralarında birebir fonksiyonlar/tip dönüşüm işlemleriyle gidip gelmek gerekiyor, bu da kanıtın özünü gölgeliyor
    Doğal sayıları reellere, sonra tekrar karmaşık sayılara çevirmek gibi tip dönüşümleri birikince özellikle dağınık hale geliyor
    Elbette bu konuya özgü bir sorun olabilir ve cebir gibi açık fonksiyonlarla çalışılan alanlarda muhtemelen çok daha doğal olur

    • Bu durumdaysan Zulip'te daha fazla soru sormalısın
      mathlib'in nasıl kullanılacağı, nelerin var olduğu ve nerede bulunduğu konusunda yönlendirme almak gerçekten çok kolay
      Katman katman birikmiş tip dönüşümü sorunları genellikle norm_cast taktiğiyle çözülür
      Belirli bir soru olmasa bile, araya sıkıştırılmış bir yorumda ya da kodda gereksiz yere karmaşık bir kanıt stili görüldüğünde, daha önce bilmediğin taktikler hakkında öneriler alabilirsin
      Biçimselleştirme sana fazla zor geliyorsa ama hangi tekniği kullanacağını bilmiyorsan, emek verip yazdığın ama memnun kalmadığın bir kanıtı izole bir örnek olarak çıkarıp insanların onu daha kısa hale getirmeye çalışmasını isteyerek soru sorabilirsin
      Bu tür sorular genellikle memnuniyetle karşılanır ve herkes çok şey öğrenir

  • Bu başlık, matematiği iyi yazma meselesiyle ilgiliymiş gibi görünüyor
    Onlarca yıldır matematik okudum, yazdım, öğrettim, uyguladım ve yayımladım; ayrıca uygulamalı matematik doktorası aldım
    Matematik yazımında sorunlar olduğu doğru ve bazı matematik metinleri gerçekten kötü yazılıyor
    Ama oldukça iyi yazılmış matematik de var
    En azından tüm semboller kullanılmadan önce tanımlanmalı ve matematiği sunmadan önce motivasyon vermek yardımcı olur; bazen sezgisel açıklamalar da faydalıdır
    İyi yazılmış matematiği dikkatle okumak, matematik yazımı öğrenmeye yardımcı olur
    Örnek olarak Paul R. Halmos'un Finite-Dimensional Vector Spaces, R. Creighton Buck'ın Advanced Calculus, Tom M. Apostol'un Mathematical Analysis, H. L. Royden'ın Real Analysis, Walter Rudin'in Real and Complex Analysis, Leo Breiman'ın Probability, Jacques Neveu'nün Mathematical Foundations of the Calculus of Probability kitapları verilebilir

    • Bu yalnızca matematiği iyi yazma meselesi değil
      Yazar, literatürde geliştirildiği biçimiyle Fermat'nın Son Teoremini doğrulamaya çalışıyordu ve bu süreçte bir alt alanı ayakta tutan yardımcı teoremin, kullanıldığı biçimiyle doğru olmadığını keşfetti
      Yine de o alanın büyük ölçüde kurtarılabilir olduğuna inanmasının nedeni, gerçekten yanlış olsaydı birilerinin şimdiye kadar olumsuz bir sonuç bulmuş olacağına dair güveni
      Şimdi o alanı ayakta tutacak uygun bir yerine koyma bulması gerekiyordu

  • Yazar oldukça eğlenceli yazan biri; yarısını pek anlamamış olsam da okunması kolay olduğu için tuhaf bir deneyimdi
    Bir kanıt çürütüldüğünde ya da onda bir kusur bulunduğunda kullanılabilecek iyi bir sözcük olarak vitiated kelimesini öğrendim
    Bunun, sonucun yanlış olarak kanıtlandığı gibi bir yanlış anlamayı daha az çağrıştırırken, söz konusu kanıtın zarar gördüğü ve yeni bir kanıt ya da onarım gerektiği anlamını taşımasını sevdim

    • Kanıtın bağırsaklarının dışarı döküldüğünü söylemek kulağa daha hoş gelebilir belki