COMPUTER VERIFIED MATHEMATICS | VOEVODSKY
| | home
UNIVALENT FOUNDATIONS OF MATHEMATICS | VOEVODSKY
|| ARTICLES | TECH PAPERS | VIDEO | IAS HoTT EBOOK ||
QUANTA MAGAZINE | MATHEMATICS | MAY 2015
|| WILL COMPUTERS REDEFINE THE ROOTS OF MATHEMATICS ? ||
When legendary mathematician Vladimir Voevodsky found a mistake in work , Voevodsky embarked on a computer aided quest to eliminate human error . To succeed , Voevodsky has to rewrite the century-old rules underlying all of Mathematics .
Rather than relying on fallible human beings to check proofs , you can turn the job over to computers ( * ) , which can tell whether a proof is correct with complete certainty .
Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of Mathematics and Computer Programming closer together .
As Voevodsky sees it , the move to computer formalization is necessary because some branches of Mathematics have become too abstract to be reliably checked by people .
" The world of Mathematics is becoming very large , the complexity of Mathematics is becoming very high , and there is a danger of an accumulation of mistakes " , Voevodsky says .
Proofs rely on other proofs ; if one contains a flaw , all others that rely on it will share the error .
CLICK TO READ MAIN QUANTA ARTICLE โคโค
CLICK TO READ RELATED QUANTA ARTICLE ( * ) โคโค
NAUTILUS | NUMBERS | MATHEMATICS | MAY 2015
|| IN MATHEMATICS MISTAKES ARE NOT WHAT THEY USED TO BE ||
Voevodsky is careful to distinguish the various ways computers should or should not be put to use :
" Lots of people do not understand the difference between using computers for calculation , for computer-generated proofs , and for computer-assisted proofs . The computer-generated proofs are the proofs which teach us very little .
And there is a correct perception that if we go toward computer generated proofs then we lose all the good that there is in Mathematics โ Mathematics as a spiritual discipline , Mathematics as something which helps to form a pure mind . "
ETHZURICH | NEWS | SEPTEMBER 2014
|| A NEW FOUNDATION FOR MATHEMATICS ||
Proofs are the key method of Mathematics . Until now , it has mainly been humans who have verified whether proofs are correct .
This could change , says Russian mathematician Vladimir Voevodsky , who has developed an approach that could indeed revolutionize Mathematics and its foundations :
Voevodsky has been able to show in principle that homotopy theory , which deals with the deformation of geometric objects , expresses the same ideas as the theory of programming languages and Mathematical logic , only in a different language .
SCIENTIFIC AMERICAN | BLOGS | OCTOBER 2013
|| VOEVODSKY'S MATHEMATICAL REVOLUTION ||
Voevodsky told mathematicians that their lives are about to change .
Soon enough, they are going to find themselves doing Mathematics at the computer , with the aid of computer proof assistants .
Soon , they will not consider a theorem proven until a computer has verified it . Soon , they will be able to collaborate freely , even with mathematicians in whose skills they do not have confidence .
Soon , they will understand the foundations of Mathematics very differently .
UNIVALENT FOUNDATIONS PROJECT | TECH PDF | OCTOBER 2010 | VOEVODSKY
Eventually it became clear to me that the univalent semantics is just a first step and that I am really working on new foundations of Mathematics .
Key features of these " univalent foundations " are as follows :
1 . Univalent foundations naturally include " axiomatization " of the categorical and higher categorical thinking .
2 . Univalent foundations can be conveniently formalized using the class of languages called dependent type systems .
3 . Univalent foundations are based on direct axiomatization of the " world " of homotopy types instead of the world of sets .
4 . Univalent foundations can be used both for constructive and for non-constructive Mathematics .
IAS | MATHEMATICS | VIDEO+PDF | MARCH 2014
|| UNIVALENT FOUNDATIONS | VLADIMIR VOEVODSKY ||
" I would like to thank all of those who are trying to understand the ideas of Univalent Foundations , to develop these ideas and to communicate these ideas to others . I know it is difficult . "
In Voevodskyโs experience , the work of a mathematician is 5% creative insight and 95% self-verification . Moreover , the more original the insight , the more one has to pay for it later in self-verification work .
The Univalent Foundations project , started at the Institute a few years ago , aims to lower the price by giving mathematicians the ability to verify their constructions with the help of computers .
Voevodsky will explain how new ideas that make this goal attainable arise from the meeting of two streams of development โ one in constructive Mathematics and the theory and practice of programming languages , and the other in pure Mathematics .
AMS | BULLETIN | VOL 51 | #4 | TECH PDF | OCTOBER 2014
|| HOMOTOPY TYPE THEORY & VOEVODSKY'S UNIVALENT FOUNDATIONS ||
ABSTRACT | Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science .
This has given rise to a new field , which has been christened homotopy type theory . In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property , called the Univalence Axiom , which has a number of striking consequences .
Voevodsky has subsequently advocated a program โ called univalent foundations โ of developing Mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model .
Because type theory possesses good computational properties , this program can be carried out in a computer proof assistant .
In this paper we give an introduction to homotopy type theory in Voevodsky's setting , paying attention to both theoretical and practical issues .
In particular , the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky's work using the well-known proof assistant Coq .
The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology ; the paper does not assume any preliminary knowledge of type theory , logic, or computer science .
Because a defining characteristic of Voevodsky's program is that the Coq code has fundamental Mathematical content , and many of the Mathematical concepts which are efficiently captured in the code cannot be explained in standard Mathematical English without a lengthy detour through type theory , the later sections of this paper ( beginning with Section 3 ) make use of code ; however , all notions are introduced from the beginning and in a self-contained fashion .
IAS | HOMOTOPY TYPE THEORY | IAS HoTT EBOOK |
Homotopy type theory is a new branch of Mathematics that combines aspects of several different fields in a surprising way .
It is based on a recently discovered connection between homotopy theory and type theory . It touches on topics as seemingly distant as the homotopy groups of spheres , the algorithms for type checking , and the definition of weak โ-groupoids .
Homotopy type theory offers a new " univalent " foundation of Mathematics , in which a central role is played by Voevodsky's univalence axiom and higher inductive types .
The present book is intended as a first systematic exposition of the basics of univalent foundations , and a collection of examples of this new style of reasoning โ but without requiring the reader to know or learn any formal logic , or to use any computer proof assistant .
We believe that univalent foundations will eventually become a viable alternative to set theory as the " implicit foundation " for the unformalized Mathematics done by most mathematicians .
CLICK TO 484 PAGE BOOK | PDF โคโค
CLICK TO OTHER FORMATS OF BOOK โคโค
|| ADDITIONAL LINKS | UPDATE 10.14.2015 ||
|| VIDEOS ||
http://video.ias.edu/vladimir
http://www.youtube.com/watch?v=vcDaQTPH-Rc
http://www.youtube.com/results?search_query=%22Vladimir+Voevodsky%22
|| MISCELLANEOUS ||
http://www.math.ias.edu/vladimir/Univalent_Foundations
http://www.math.ias.edu/vladimir/home
http://github.com/vladimirias
http://github.com/HoTT/HoTT
http://baaltii1.livejournal.com/198675.html
http://baaltii1.livejournal.com/200269.html
http://en.wikipedia.org/wiki/Proof_assistant
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
SOURCE | SATYAVEDISM.ORG
OM! TAT SAT
