Qui presento una completa auto-formalizzazione di un recente articolo di matematica (di nuovo!) Barańczuk, Stefan. "Ridurre il numero di equazioni che definiscono un sottoinsieme dello spazio n su un campo finito." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Ho trascorso alcuni giorni su questo progetto. Prima, ho eseguito Aristotle di @HarmonicMath, che in circa 15 ore ha completamente auto-formalizzato la dimostrazione. Poi, con l'ottimo aiuto di @PietroMonticone, sono riuscito a impostare una versione blueprint della dimostrazione. Questa è una versione in cui tutte le parti della documentazione in LaTeX diventano interattive e possono essere ispezionate e studiate. Possiamo vedere le dipendenze nella dimostrazione e studiare le loro relazioni. Nella fase di post-elaborazione, ho anche utilizzato Grok Heavy e Codex CLI con GPT-5.2 in modalità xhigh per scrivere un'analisi riga per riga della dimostrazione formale. Questo è un grande aiuto per le persone che non sono programmatori professionisti di Lean 4. Puoi davvero interiorizzare tutti i passaggi della dimostrazione. Voglio riassumere le mie impressioni e ciò che ho imparato da questa esperienza. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei