Strumento utile

Il percorso gratuito Learn Lean parte dal Natural Number Game e prosegue con manuali e risorse per formalizzare matematica. È utile per capire concretamente la differenza fra testo convincente e prova controllata, cominciando da enunciati piccoli. Non occorre iscriversi a un prodotto AI; gli esempi insegnano anche a riconoscere ipotesi e passaggi. Per chi affronta manoscritti avanzati serve comunque competenza matematica: il gioco è un ingresso, non certifica una ricerca.

Fonti: lean-lang