Muito boa a postagem, vale muito a pena ver a palestra promovida pelo IMPA, (instituto de matemática pura e aplicado), eles promoveram uma live sobre isso, que vai muito a pena ver se ainda não viu. PS: não sei se já tenteou fazer algum código em Lean se ainda não fez vale a pena fazer, nessa horas vc da graças a deus que a IA existe kkkk
Mas muito bom o post