Paralipomeni di Alice: MathGPT e il mah-jong

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.
Questi video possono essere generati in due modi: a partire da una richiesta esplicita di realizzare un video su un dato argomento, oppure inserendo un testo e chiedendo di trasformarlo in un video. C'è comunque il limite sulla lunghezxza (stiamo parlando di video intorno ai 2 minuti), ma a parte questo direi che l'esperimento che ho realizzato con il mio articolo sul Mah-jong non è andato male: potete vederlo qui sotto.
E' quindi possibile che ogni tanto trasformerò i miei post in video utilizzando proprio MathGPT, ma non così spesso come pensavo, visto che altri esperimenti, che non pubblicherò, non sono andati esattamente come volevo. Su tutti il video dedicato alle proprietà del 185, di cui speravo di poter utilizzare almeno le animazioni, ma così non è stato.
Detto ciò, vi lascio al video: buona visione!

---

Immagine di apertura generata con Canva