Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

Асисте нт дове дення теоре м англ proof assistant або інструмент інтерактивного доведення теорем англ interactive theore

Асистент доведення теорем

Асистент доведення теорем

Асисте́нт дове́дення теоре́м (англ. proof assistant) або інструмент інтерактивного доведення теорем (англ. interactive theorem prover) — програмне забезпечення, яке дозволяє користувачам займатися математикою на комп'ютері, але не стільки обчисленнями (чисельними чи символьними), як визначеннями і доведеннями. За допомогою такої системи, користувач може формалізовано будувати математичну теорію на основі визначених аксіом та здійснювати логічні операції над визначеннями.

До пропонентів використання асистентів доведення теорем належать такі математики як Володимир Воєводський, та Кевін Баззард. Водночас, станом на 2021 рік, асистенти доведення теорем використовуються у передових математичних дослідженнях рідко.

Історія

Цей розділ потребує доповнення.

У 2017 році в науковому журналі було опубліковане формалізоване доведення гіпотези Кеплера, виконане у системах та .

У 2021 році асистент Lean було використано для формалізації доведення нової теореми Петера Шольце в галузі [en], у доведенні якої він не був цілком упевнений. Формалізацію було здійснено групою волонтерів під керівництвом Йогана Коммеліна (Johan Commelin). Таким чином було показано, що система Lean може бути корисною у передовій математиці.

Список асистентів доведення теорем

Примітки

  1. Geuvers, Herman (February 2009). Proof assistants: History, ideas and future. Sādhanā. 34 (1): 3—25. doi:10.1007/s12046-009-0001-5. S2CID 14827467.
  2. Moura, Leonardo de; llrich, Sebastian. The Lean 4 Theorem Prover and Programming Language (PDF). Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. Springer International Publishing: 625—635.
  3. Hartnett, Kevin (19 травня 2015). Will Computers Redefine the Roots of Math?. Quanta Magazine.
  4. Voevodsky, Vladimir (Summer 2014). The Origins and Motivations of Univalent Foundations: A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes (PDF). The Institute Letter. Institute for Advanced Study: 8—9.
  5. Hales, Thomas (18 вересня 2018). A Review of the Lean Theorem Prover. Процитовано 6 жовтня 2020.
  6. Buzzard, Kevin. The Future of Mathematics? (PDF). Процитовано 6 жовтня 2020.
  7. Hartnett, Kevin (28 липня 2021). Proof Assistant Makes Jump to Big-League Math. Quanta Magazine.
  8. ; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland (29 травня 2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi. 5: e2. doi:10.1017/fmp.2017.1.
  9. Hartnett, Kevin (28 липня 2021). Proof Assistant Makes Jump to Big-League Math. Quanta Magazine.
  10. Commelin, Johan (2022). Liquid Tensor Experiment (PDF). Mitteilungen der Deutschen Mathematiker-Vereinigung. 30 (3): 166—170. doi:10.1515/dmvm-2022-0058.

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

Asiste nt dove dennya teore m angl proof assistant abo instrument interaktivnogo dovedennya teorem angl interactive theorem prover programne zabezpechennya yake dozvolyaye koristuvacham zajmatisya matematikoyu na komp yuteri ale ne stilki obchislennyami chiselnimi chi simvolnimi yak viznachennyami i dovedennyami Za dopomogoyu takoyi sistemi koristuvach mozhe formalizovano buduvati matematichnu teoriyu na osnovi viznachenih aksiom ta zdijsnyuvati logichni operaciyi nad viznachennyami Do proponentiv vikoristannya asistentiv dovedennya teorem nalezhat taki matematiki yak Volodimir Voyevodskij ta Kevin Bazzard Vodnochas stanom na 2021 rik asistenti dovedennya teorem vikoristovuyutsya u peredovih matematichnih doslidzhennyah ridko IstoriyaCej rozdil potrebuye dopovnennya U 2017 roci v naukovomu zhurnali bulo opublikovane formalizovane dovedennya gipotezi Keplera vikonane u sistemah ta U 2021 roci asistent Lean bulo vikoristano dlya formalizaciyi dovedennya novoyi teoremi Petera Sholce v galuzi en u dovedenni yakoyi vin ne buv cilkom upevnenij Formalizaciyu bulo zdijsneno grupoyu volonteriv pid kerivnictvom Jogana Kommelina Johan Commelin Takim chinom bulo pokazano sho sistema Lean mozhe buti korisnoyu u peredovij matematici Spisok asistentiv dovedennya teoremAgda Coq LeanPrimitkiGeuvers Herman February 2009 Proof assistants History ideas and future Sadhana 34 1 3 25 doi 10 1007 s12046 009 0001 5 S2CID 14827467 Moura Leonardo de llrich Sebastian The Lean 4 Theorem Prover and Programming Language PDF Automated Deduction CADE 28 28th International Conference on Automated Deduction Virtual Event July 12 15 2021 Proceedings 28 Springer International Publishing 625 635 Hartnett Kevin 19 travnya 2015 Will Computers Redefine the Roots of Math Quanta Magazine Voevodsky Vladimir Summer 2014 The Origins and Motivations of Univalent Foundations A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes PDF The Institute Letter Institute for Advanced Study 8 9 Hales Thomas 18 veresnya 2018 A Review of the Lean Theorem Prover Procitovano 6 zhovtnya 2020 Buzzard Kevin The Future of Mathematics PDF Procitovano 6 zhovtnya 2020 Hartnett Kevin 28 lipnya 2021 Proof Assistant Makes Jump to Big League Math Quanta Magazine Adams Mark Bauer Gertrud Dang Tat Dat Harrison John Hoang Le Truong Kaliszyk Cezary Magron Victor McLaughlin Sean Nguyen Tat Thang Nguyen Quang Truong Nipkow Tobias Obua Steven Pleso Joseph Rute Jason Solovyev Alexey Ta Thi Hoai An Tran Nam Trung Trieu Thi Diep Urban Josef Vu Ky Zumkeller Roland 29 travnya 2017 A Formal Proof of the Kepler Conjecture Forum of Mathematics Pi 5 e2 doi 10 1017 fmp 2017 1 Hartnett Kevin 28 lipnya 2021 Proof Assistant Makes Jump to Big League Math Quanta Magazine Commelin Johan 2022 Liquid Tensor Experiment PDF Mitteilungen der Deutschen Mathematiker Vereinigung 30 3 166 170 doi 10 1515 dmvm 2022 0058

Дата публікації:
Топ