“INFORMATIKADA SUN’IY INTELLEKT YORDAMIDA MATEMATIK TEOREMALARNI AVTOMATIK ISBOTLASH”
Keywords:
Kalit so’zlar: Sun’iy intellekt, avtomatik teorem isbotlash, formal mantiq, mashinali o‘rganish, informatika, evristik algoritmlar, matematik isbotlash, Coq, Lean, Isabelle/HOL, AlphaTensor, kompyuter matematikasi.Abstract
Annotatsiya: Mazkur maqola informatika va sun’iy intellekt (SI) sohalarining kesishgan nuqtasida joylashgan dolzarb muammoni — matematik teoremalarni avtomatik isbotlash masalasini yoritadi. Unda avtomatik teorem isbotlash tizimlarining mantiqiy asoslari, ishlash prinsiplari hamda mashinali o‘rganish, evristik algoritmlar va formal tizimlar kabi SI yondashuvlari orqali qanday amalga oshirilishi tahlil qilinadi. Shuningdek, Coq, Lean, HOL Light kabi zamonaviy platformalarning amaliy ahamiyati va ularning ilmiy-tadqiqotda qo‘llanilishi ko‘rsatib o‘tiladi. Maqolada sun’iy intellekt yordamida matematik tafakkurni avtomatlashtirish imkoniyatlari, bu yo‘nalishdagi so‘nggi tadqiqotlar va istiqbolli yo‘nalishlar haqida ham fikr yuritiladi.
References
1. Russell, S., & Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4th ed.). Pearson.
2. Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.
3. Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer.
4. Avigad, J., & Harrison, J. (2014). Formally Verified Mathematics. Communications of the ACM, 57(4), 66–75.
5. Hales, T. C. et al. (2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi, 5, e2
6. Gonthier, G. (2008). Formal Proof—The Four-Color Theorem. Notices of the AMS, 55(11), 1382–1393.
7. Geuvers, H. (2009). Proof Assistants: History, Ideas and Future. Sadhana, 34(1), 3–25.
8. DeepMind’s AlphaTensor project — sun’iy intellekt yordamida matematik algoritmlarni optimallashtirish bo‘yicha zamonaviy tadqiqot.
9. O‘zbekiston axborot texnologiyalari va kommunikatsiyalarini rivojlantirish vazirligi: Sun’iy intellekt va teoremalarni isbotlash — mahalliy kontekstda sun’iy intellektning qo‘llanilishi haqida.
