Grazie a un
articolo su MaddMaths! relativo alla dimostrazione di
Andrew Wiles sull'
ultimo teorema di Fermat, ho recentemente scoperto l'interessante
Lean, un
proof assistant, ovvero una rete neurale specializzata nelle dimostrazioni matematiche. Non è ancora al livello di realizzare da zero una dimostrazione, o almeno così si dice, ma è un utile strumento per verificare i passaggi più ostici delle dimostrazioni. Ho provveduto a installarlo, ma ancora non l'ho provato.
Ho, invece, iniziato a provare alcune reti neurali conversazionali di tipo matematico. In effetti sono un po' più che semplici reti conversazionali, visto che sono in grado di risolvere equazioni, impostare dimostrazioni semplici, realizzare grafici e in alcuni casi, come quello di
MathGPT, anche realizzare dei video.
