coq


    1. isbat köməkçilərindən biri. kompüterlərdən və kodlamadan filan elə də anlamadığım üçün hələlik sadəcə üzünə baxdığım amma anlayanlar üçün əla araşdırma sahələrindən biri.

    deməli məlum teoremləri bu isbat köməkçiləri vasitəsilə formalaşdırırsız sonra da bu köməkçilər isbatı yoxlayırlar. coq da bu cür isbat köməkçilərindən biridir.

    introduction üçün: https://cel.archives-ouvertes.fr/inria-00001173v6/document

    məşhur teoremlərin isbatlarına baxıb fikir əldə edə bilərsiz. https://arxiv.org/pdf/cs/0509025.pdf

    üstdəki məqalədə yazarlar sadə ədədlər teoremini isbat ediblər.

    daha bəsit teoremlərə də baxmaq olar, məsələn calculusun fundamental teoremi kimi.

    xüsusilə computer science ilə maraqlanan yazarlar varsa baxsınlar. digər bir maraqlı mövzu da (bax: homotopy type theory) htt






hamısını göstər