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

você realmente não precisa conhecer Julia para isso, pois é muito simples! (e você _definitivamente_ não precisa conhecer Lean)

De qualquer forma, aqui está o post

Se você gosta mais de transmissões ao vivo:

@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 o Lean seria um efeito colateral fácil do sistema de tipos com alguma gentileza adicional em que você pode realmente escrever software em Julia

@frang_u99393 "Lean" como um substituto para "Sistemas de prova de teorema interativo do tipo Lean"