Lean (provador de teoremas)

Em Lean, uma prova matemática vira código. Se compila, cada passo foi checado pela máquina. Isso importa na era da IA: quando um modelo propõe uma prova formalizada em Lean, não é preciso confiar no modelo, porque a verificação é automática. Veja o caso dos resultados matemáticos da OpenAI e do fundo da Simons Foundation.