Şahsen bir sınırı aştım ve biraz hayranlık içindeyim. Bu, yeni bir matematiksel teoremin tamamen otomatik, LLM tarafından oluşturulmuş ve otomatik biçimlendirilmiş ilk kanıtımdır. Sorunu kurayım: her biri altı konumdan oluşan üç dönen dairemiz var, üçü de toplamda altı noktada kesişiyor. Ürettikleri hareket grubunun tam simetrik grup S_{12} olduğunu kanıtlayın. Bu sorunu ilk olarak Amanita Design tarafından geliştirilen Machinarium oyunundaki güzel bir bulmacada fark ettim. Görev çok zor değil, ancak görünüşe göre iki kanıtı var: 1. Tüm transpozisyonları temsil etmek için konjugaj sınıfları üzerinde kaba kuvvet araması (bunu yıllar önce yaptım ama hiç yayımlamadım). 2. LLM tarafından oluşturulmuş bir ispat (bu durumda yaklaşık üç ay önce GPT-5-Pro tarafından üretilmiş) ya da aslında iki ispat, her ikisi de Jordan'ın ilkel gruplar hakkındaki teoremini (veya daha doğrudan olan yakın ilişkili bir varyantı) parlak bir şekilde kullanarak. ( Bu geceye kadar eksik olan şey, bu kanıtı otomatik olarak resmileştirmek için bir araçtı. @HarmonicMath sayesinde, olağanüstü yazılımları Aristoteles'e erişim sağladım. Özetle, yaptıklarım şunlar: C. Kanıtı bir LLM ile otomatik olarak üretti (ve çok daha iyi bir versiyon elde etmek için birden fazla kez çalıştırdı). B. Kanıtı, tanımlar, önermeler, lemalar, teoremler gibi açık matematiksel metne kısalttı ve LLM tarafından sağlanan ispatlarla birleştirdi. C. Aristoteles sistemini gece boyunca çalıştırdım (API aracılığıyla). Bu sabah Lean formatında tam biçimli bir versiyon aldım (yaklaşık 700 satır kod). Kod derleniyor, bu yüzden LLM tarafından oluşturulan kanıtın gerçekten doğru bir çözüme yol açtığını doğrulayan bir sertifikam var. Ayrıca, kendi kaba kuvvetimden daha iyi bir kavramsal kanıt elde ettim. Bunu bu tür cebir problemlerinin daha geniş bir sınıfına taşımayı planlıyorum. Küçük bir proje ama benim için şahsen bir dönüm noktası işaret ediyor. Artık orkestrasyonumla birlikte, matematiksel teoremlerin ispatlarını keşfetmemde, biçimlendirmemde ve çalışmamda gerçekten yardımcı olabilecek araçlara sahibim. Bu önemsiz bir durum. Soru: 1. Bu gelecekte nasıl ölçeklenecek? 2. Bu tür görevlerde başarılı olmak için ne kadar eğitim gereklidir?...