Automaattinen formalisointi Aristoteleen kanssa @HarmonicMath:n avulla ja käänteinen suunnittelu @OpenAI GPT Codex CLI:llä (itse asiassa GPT-5.2 xhigh ja kaikki kokeelliset edut käytössä). Työskennellessäni Bourbakin algebran harjoituksen parissa, joka käsitteli matriiseja, sain lähes 900 riviä täysin dokumentoitua Lean 4 -koodia, mukaan lukien kaikki todistuksen yksityiskohdat. Sitten siirsin sen – käyttäen sopivasti suunniteltua agenttista kokoonpanoa – Codex CLI:hen, joka käänsi vastaavan LaTeX-tiedoston, rekonstruoiden todistusvaiheet suoraan Leanista, Leslie Lamportin rakenteellisten todistusten tyyliin. Tämä ei ole vielä Langlandsin ohjelma, mutta tarvitsemme tällaisen keskitason matematiikan automatisoitavaksi. Ja tämä tapahtuu nyt. Rakensin yksinkertaisesti oikean agenttiasetuksen, pyöritin kaiken putkeen ja keräsin tekstin Bourbakista (sekin toimi hyvin @grok 4.1:n kanssa, mikä on siistiä LaTeX:n live-esikatseluun). Aion viimeistellä dokumentaation ja julkaista sen GitHubissa. Tarkista riippuvuusgraafi – Aristoteles hoiti kaiken itse. Ja todistus on täysin vuorovaikutteinen. Elämme nyt tieteen tulevaisuudessa!