Preocupa-me genuinamente quantos matemáticos me disseram esta semana "se compila no lean, sabemos que é verdade". Lean é ótimo, mas isso é perigosamente falso. Aqui estão 50 maneiras de provar que 1 == 0 no Lean. Que compilam. Dependendo da versão que você usa. (link nos comentários)