ÚLTIMA HORA: A versão para consumidores do Aristotle supera Putnam, resolvendo e verificando formalmente 10/12 problemas em @leanprover. Parabéns à matemática amadora @namrata_anand2, que usou a versão de consumo do Aristotle com um lançamento público antecipado dos problemas. Parece que o Aristotle os devorou no café da manhã, resolvendo 10/12 de forma totalmente autônoma. Atualmente, estamos analisando os arquivos e compartilharemos mais detalhes mais tarde, mas duas coisas úteis a destacar agora: ▪️ Estes parecem ser as primeiras soluções totalmente formalizadas para os problemas de Putnam de 2025 lançadas publicamente. ▪️ Todos usaram a interface de linguagem natural recentemente lançada, na qual o Aristotle recebeu a pergunta em linguagem natural, depois a autoformalizou em uma declaração Lean4 e, em seguida, completou a prova, totalmente de forma autônoma, sem intervenção humana. No passado, focamos nas capacidades de prova de teoremas de ponta do Aristotle, mas ele também está se tornando bastante capaz em autoformalização. Estamos entrando em uma nova era para a IA e a matemática. Devagar... depois tudo de uma vez!

Aristóteles da @HarmonicMath resolveu 10/12 problemas em 7 horas no Putnam, a competição de matemática de graduação mais difícil do mundo! Como sei disso? Bem, eu executei o Aristóteles eu mesmo através da API pública da Harmonic. E levei cerca de 10 minutos para começar e dar início! 9 dos 10 problemas foram completados em menos de 3 horas. O décimo (B5) levou 7 horas, uma hora a mais do que os concorrentes têm disponível. Para todos os 10 problemas, eu forneci a Aristóteles as declarações dos problemas em inglês — e ele formalizou automaticamente as declarações, provou-as e produziu saídas verificadas de forma autônoma, sem nenhum feedback humano. Como alguém que ama matemática, mas não é um especialista, é empolgante ter uma ferramenta tão poderosa ao meu alcance! 1/

Completei uma auto-formalização completa com @HarmonicMath Aristotle do seguinte problema geral de teoria de grupos Fixe três inteiros positivos n, k, m. Prove que um subgrupo H de S_{6+(n+k+m)} gerado por g1:=G!(1,6,4,3,a_1,...a_n); g2:=G!(1,2,4,5,b_1,...,b_k); g3:=G!(5,6,2,3,c_1,...,c_m); H:=sub<G|[g1,g2,g3]>; satisfaz H = S_{6+(n+k+m)} ou H = A_{6+(n+k+m)}. Temos H = S_{6+n+k+m} se e somente se pelo menos um de n, k, m é par, caso contrário H=A_{6+(n+k+m)}. Repositório GitHub com código Lean e esboço informal do ChatGPT-5.1-Pro A auto-formalização em duas execuções mistas (no total cerca de 20 horas). O código tem cerca de 2600 linhas de código Lean. O teorema não pode ser resolvido com sistemas clássicos de álgebra computacional. Ele subsume a tentativa anterior com as escolhas n=m=k=2 feitas anteriormente.