on dirait que Lean est populaire aujourd'hui, alors voici un petit post sur comment/pourquoi cela fonctionne et comment implémenter une version mini de cela en Julia.

vous n'avez vraiment pas besoin de connaître Julia pour cela car c'est très simple ! (et vous _n'avez définitivement_ pas besoin de connaître Lean)

de toute façon, voici le post

si vous êtes plutôt du genre à apprécier les livestreams :

@outputlayer rosé pine dawn (sans italique), la police est berkeley mono de l'inimitable @usgraphics

@frang_u99393 oh oui, les types dépendants apparaissent pleinement ici, alors Lean serait un effet secondaire facile du système de types avec un peu de convivialité supplémentaire en ce sens que vous pouvez réellement écrire des logiciels en Julia.

@frang_u99393 "Lean" comme substitut pour "systèmes de preuve interactive de type Lean"