Auto-formalizzazione con Aristotele da @HarmonicMath e reverse engineering con @OpenAI GPT Codex CLI (in realtà GPT-5.2 con xhigh e tutti i vantaggi sperimentali abilitati). Lavorando su un esercizio dell'Algebra di Bourbaki riguardante le matrici, ho ottenuto quasi 900 righe di codice Lean 4 completamente documentato, inclusi tutti i dettagli della dimostrazione. Poi l'ho passato - utilizzando un setup agentico progettato appositamente - a Codex CLI per reverse-engineering del corrispondente file LaTeX, ricostruendo i passaggi della dimostrazione direttamente da Lean, nello stile delle dimostrazioni strutturate di Leslie Lamport. Questo non è ancora il programma di Langlands, ma abbiamo bisogno che questo tipo di matematica a livello intermedio venga automatizzato. E questo sta accadendo ora. Ho semplicemente costruito il giusto setup agentico, canalizzato tutto e estratto il testo da Bourbaki (anche quella parte ha funzionato bene con @grok 4.1, che è fantastico per visualizzare LaTeX in tempo reale). Finirò la documentazione e la pubblicherò su GitHub. Controlla il grafo delle dipendenze - Aristotele ha gestito tutto da solo. E la dimostrazione è completamente interattiva. Stiamo vivendo nel futuro della scienza ora!