Auto-formalização com Aristóteles pela @HarmonicMath e engenharia reversa com @OpenAI CLI do GPT Codex (na verdade GPT-5.2 com xhigh e todos os benefícios experimentais ativados). Trabalhando em um exercício do Álgebra de Bourbaki sobre matrizes, obtive quase 900 linhas de código Lean 4 totalmente documentado, incluindo todos os detalhes da demonstração. Depois, passei nele — usando uma configuração agential adequadamente projetada — para Codex CLI para fazer engenharia reversa do arquivo LaTeX correspondente, reconstruindo os passos da prova diretamente a partir do Lean, no estilo das provas estruturadas de Leslie Lamport. Esse ainda não é o programa Langlands, mas precisamos que esse tipo de matemática de nível intermediário seja automatizada. E isso está acontecendo agora. Simplesmente construí a configuração agente certa, pipelineei tudo e raspei o texto do Bourbaki (até essa parte funcionou bem com @grok 4.1, que é legal para pré-visualizar LaTeX ao vivo). Vou terminar a documentação e postá-la no GitHub. Verifique o grafo de dependências — Aristóteles lidou com tudo sozinho. E a prova é totalmente interativa. Estamos vivendo no futuro da ciência agora!

Neste post da comunidade, quero colocar links para alguns jogos altamente envolventes e ambientes interativos (disponíveis gratuitamente) que ajudam as pessoas a explorar conceitos sofisticados tanto em programação quanto em matemática. Se você conhece algum outro lugar divertido para visitar, basta postar abaixo. Divertir-se! Lean: Uma coleção de quebra-cabeças de programação altamente envolventes que ajudam você a aprender como a matemática é comprovada e formalizada. Você nunca mais verá da mesma forma a dureza de 5*7=7*5. NandGame: Você cria seu próprio processador do zero (até a NAND é feita de circuitos mais simples). Altamente viciante e super divertido! Armadilha Quântica: É aqui que você finalmente vai entender melhor as computações quânticas. Colorido, ilimitado, envolvente e matematicamente muito profundo. Scratch: Aprenda programação do jeito divertido. Euclidea: Aprenda a realizar construções com régua e bússola. Antes fazia parte da educação escolar, mas agora é um aplicativo. Divertido e muito informativo. Planaridade: Tente encontrar um embedding de grafo que mostre que ele é realmente planar. Caramba: O explorador definitivo de autômatos celulares. Se quiser aprofundar: SageMath: É um sistema poderoso de álgebra computacional com sintaxe em Python. É ideal para cursos e a sintaxe do SageMath é muito mais próxima do discurso matemático regular. Gosto de dar aulas com SageMath. GeoGebra: Você pode fazer provas, cálculos e applets interativos. É uma forma divertida de aprender várias facetas da matemática universitária. Projetos de Demonstração Wolfram: Uma coleção de applets matemáticos que pode ajudar você a entender tópicos muito sofisticados. Você não precisa do Mathematica para rodar, mas precisa dele para projetar seus próprios applets. A Mecânica da Prova (por Heather Macbeth): É um livro com um repositório interativo no GitHub onde você pode aprender de forma mais abrangente a estrutura e a sintaxe do Lean. Uma Teoria Ilustrada dos Números (por Martin H. Weissman): Este é um livro didático sobre teoria elementar dos números com aplicações. E esses aplicativos estão disponíveis no site como uma coleção de Jupyter Notebooks gratuitos que ensinam os conceitos-chave. Álgebra Linear Gráfica: De forma ilustrada e, em certa medida, interativa de aprender conceitos profundos em álgebra. HomotopyContinuation.jl: Esta é uma forma incrivelmente bonita e interativa (com Julia) de aprender ideias altamente complexas da geometria algébrica (componentes conexos, método de continuação por homotopia) e com aplicações para sistemas algébricos muito especiais que vêm de aplicações. Você pode aprender a Julia no caminho. Mathamaze: É uma experiência de Helena Verrill. Geometria linda, azulejos, padrões. Simplesmente maravilhoso. Difícil de explicar: N: O Caminho do Ninja: Se você acha matemática difícil. Aprenda a paciência do jeito difícil. Aviso: altamente viciante HyperRogue: Você pode aprender geometria hiperbólica em um ambiente rogue-like.

Aqui apresento uma auto-formalização completa de um artigo recente de matemática (novamente!) Barańczuk, Stefan. "Reduzindo o número de equações que definem um subconjunto do espaço n-dimensional sobre um corpo finito." Annales de la Faculté des sciences de Toulouse: Mathématiques, ser. 6, vol. 33, nº 1 (2024): 177–182. Passei alguns dias nesse projeto. Primeiro, rodei Aristóteles por @HarmonicMath , que em cerca de 15 horas formalizou completamente a demonstração. Então, com a grande ajuda de @PietroMonticone, consegui configurar uma versão blueprint da prova. Esta é uma versão em que todas as partes da documentação em LaTeX se tornam interativas e podem ser inspecionadas e estudadas. Podemos ver as dependências na prova e estudar suas relações. Na etapa de pós-processamento, também usei Grok Heavy e Codex CLI com GPT-5.2 em modo xhigh para escrever uma análise linha por linha da prova formal. Isso é uma grande ajuda para quem não é programador Lean 4 profissional. Você realmente pode internalizar todas as etapas da prova. Quero resumir minhas impressões e o que aprendi com essa experiência. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei