isbat köməkçiləri

kepler hipotezi

proof assistant

coq

1. coq və s. kimiləri olan və riyaziyyat teoremlərininin isbatlarını kompyuter proqramlaşdırma dillərinə çevirə bildiyimiz və bununla da asanlıqla isbatın doğru olub olmadığını yoxlaya biləcəyimiz vasitələr. voevodsky tərəfindən yaradılmış və topologiyadakı homotopiya anlayışına söykənən homotopy type theory hal-hazırda bu isbat köməkçiləri ilə işləmək üçün ən rahat namizəd nəzəriyyədir. azca kompyuter bilgisi, az-maz topologiya bilən varsa bu kitabı oxusun: https://www.heidelberg-laureate-forum.org/wp-content/uploads/2013/10/homotopy-type-theory_univalent-foundations-of-mathematics.pdf

qeyd. homotopiya haqda asan öyrənmək üçün buyurun:

(youtube:

)

şərhlər: