Anatomia di una dimostrazione
Tempo fa si è parlato di proof assistants, e oggi ho notato questo breve articolo che mostra in cosa consiste la dimostrazione "certificata" di un fatto estremamente noto: autovettori di autovalori distinti sono linearmente indipendenti.
https://arxiv.org/pdf/2411.11885
Credo sia educativo vedere una di queste dimostrazioni, se non l'avete mai fatto. Da lì, è possibile essere ancora più elaborati, e scrivere articoli dove quasi tutte o tutte le dimostrazioni sono state "meccanizzate", ad esempio, qui https://arxiv.org/abs/2409.10237
https://arxiv.org/pdf/2411.11885
Credo sia educativo vedere una di queste dimostrazioni, se non l'avete mai fatto. Da lì, è possibile essere ancora più elaborati, e scrivere articoli dove quasi tutte o tutte le dimostrazioni sono state "meccanizzate", ad esempio, qui https://arxiv.org/abs/2409.10237
Risposte
Con Lean si riesce a formalizzare la dimostrazione del teorema di Lagrange per i gruppi finiti, per esempio?
Qui invece i teoremi di Sylow. https://leanprover-community.github.io/ ... sylow.html
Del resto ci sono definizioni per un po' tutta la matematica elementare (comunque troppo poche), perché il teorema di Lagrange dovrebbe essere speciale/diverso?
Del resto ci sono definizioni per un po' tutta la matematica elementare (comunque troppo poche), perché il teorema di Lagrange dovrebbe essere speciale/diverso?
Sì, è che non conoscevo questo Lean, poi lo provo.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo