Diario di un matematico non praticante

Con le intelligenze artificiali che dimostrano teoremi e i programmi che formalizzano le dimostrazioni non ci si divertirà più a fare matematica? I commenti sono di tipo opposto.

Un professore ha “dimostrato” che un LLM non potrà mai superare la creatività di un bravo dilettante. Ma stiamo facendo la domanda corretta?

Sir Roger Penrose pensa che le IA non siano intelligenti, ma solo ingegnose. Vedendo gli ultimi risultati, il mio commento è: probabilmente sì, ma è comunque tanta roba.

Perché i matematici odiano i cavallucci e i cagnolini? Non è una battuta, ma la conseguenza del voler spesso essere estremamente formali.

AxiomProver non solo dimostra teoremi, ma dimostra formalmente la dimostrazione. Ma non basta ancora per fare il matematico.