parece que o Lean está popular hoje, então aqui está um pequeno post sobre como/por que funciona e como implementar uma mini versão dele em Julia

você não precisa realmente saber Julia para isso, já que é muito simples! (e você _definitivamente_ não precisa saber Lean)

de qualquer forma, aqui está o post

se você é mais um apreciador de livestreams:

@outputlayer rosé pine dawn (sem itálico), a fonte é berkeley mono do inimitável @usgraphics

@frang_u99393 oh sim, os tipos dependentes aparecem totalmente aqui, então Lean seria um efeito colateral fácil do sistema de tipos com um adicional de que você pode realmente escrever software em Julia.

@frang_u99393 "Lean" como um substituto para "sistemas de prova interativa de teoremas semelhantes ao Lean"