Aristoteles ile @HarmonicMath ile otomatik formalizasyon ve @OpenAI GPT Codex CLI ile tersine mühendislik (aslında GPT-5.2, xhigh ve tüm deneysel avantajlar etkinleştirilmiş durumda). Bourbaki'nin Cebirinden matrislerle ilgili bir egzersiz üzerinde çalışırken, kanıtın tüm detaylarını içeren neredeyse 900 satır tam belgelenmiş Lean 4 kodu elde ettim. Sonra uygun tasarlanmış bir ajanik kurulum kullanarak Codex CLI'ya verdim, böylece ilgili LaTeX dosyasını tersine mühendislik yaptım, ispat adımlarını doğrudan Lean'den, Leslie Lamport'un yapılandırılmış ispatları tarzında yeniden oluşturdum. Bu henüz Langlands programı değil, ama bu tür orta seviye matematiğin otomatikleştirilmesi gerekiyor. Ve bu şimdi oluyor. Doğru ajanik kurulumu kurdum, her şeyi pipeline yaptım ve Bourbaki'den metni kazadım (o kısım bile @grok 4.1 ile iyi çalıştı, bu da LaTeX'i canlı ön izleme için harika). Dokümantasyonu bitirip GitHub'a yükleyeceğim. Bağımlılık grafiğini kontrol edin - Aristoteles bunu tek başına halletti. Ve kanıt tamamen etkileşimli. Şimdi bilimin geleceğinde yaşıyoruz!