Não consigo acreditar que os humanos escrevem código Lean manualmente, cara. E que as coisas estavam a ser formalizadas nele antes dos LLMs. Formalizar qualquer coisa em Lean é tão agradável quanto descascar a pele com um descascador de batatas e tão interessante quanto ver a tinta secar.

Não me venham falar sobre a "alegria do jogo" / "é tão interativo" ou o que quer que seja. Existem jogos com tudo para ver, assim como há ra*e em todo lado, e eu sei a diferença.

@notmoeezm "Eu nem me importo se as máquinas verificam provas" fonte: cara que ajusta algoritmos de busca no espaço de provas por diversão, usando Lean😞