# COMPUTER VERIFIED MATHEMATICS | VOEVODSKY

| | homeUNIVALENT 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.COM