When I was studying in Moscow University,foundations of mathematics is a subject is extremely unfashionable.
There were different groups,a group of algebra, a group of topology,a group of analysis, a group of differential equations ...,there was also a group of foundations of mathematics.
At the end of second year every student must choose his or her group.It was an important choice, and we discuss it a lot,and different group has different reputation.
At my time the group of algebra is very cool, there were famous people in the group.the group of topology and geometry was also cool, there were also famous people in the group.
Some other groups are less cool,and the group of foundations of mathematics was almost the least group of all.(Maybe except for the history of mathematics.)
Nobody who think themself a good mathematician will considered going there.
Back then I went to the group of algebra,I still consider myself an algebraist,I am applying methods of algebra to other area of mathematics.
But now I working full time on foundations of mathematics.Why?How did I get here?Am I becoming uncool?
I am here to explain why the way we are developing the foundations of mathematicswill make it a very cool subject again.(I said "again", because it was a very cool subject during 1910s and 1920s.)
Many of us do mathematics that is a little like the Rubik Cube.
There is a problem.
And there is the search for a solution.
And when the solution is found, it is certain that it is a solution.
But the mathematics which earned me the Fields Medal of 2002 in Beijing is very different.
There is a problem.
And there is the search for a solution.
But when the solution is found, it is not certain at all that it is a solution.
(The Fields Medal was awarded to me for the proof of Milnor's Conjecture.)
Suppose you want to solve a special algebraic equation of degree 5.You found the solution by some means,then you can substitution the root into the equation to check that it is a solution.
But if you want to solve a group of 20 equations of degree 20or something as complicated like that.You found the solution by some means,then you have to do a lot of calculation to check your solution.
Nowaday no one will do it by hand,you will use some software to help you verify your solution is a solution.
Now imagine your problem is to prove some theorem.And your solution is a proof.How do you verify the proof is really a solution?
There are some conventions you learned from your teachers or professors,about what constitutes a rigorous proof,but you can not feed it to a computer to let the computer check it yet.
Back to the Milnor's Conjecture.
The problem is to find a proof of the conjecture.
The search for a solution took me about two years, from 1993 to 1995.
The solution was a proof.
In 1995 I started to work on "writing the proof down".I had the first preprint available in June of 1995.
But it was only the beginning of the story of my proof of Milnor's Conjecture.
You can see how the dynamic of the work of real mathematics unfold in time.Ideally a mathematician prove theorems, but you will see how it really goes.
Remember that I got the proof at 1995, but got my Fields Medal in 2002.
The proof that I found depend on another conjecture.That conjecture was in itself very cool and connected two areas of mathematicswhich were at that time very far apart.
I was also sure that I know how to prove this conjecture,but I know it will take long time.
Then I started to look for a modification of the first proof,to make it not depend on the new conjecture.About a year later I found it.I wrote preprint with the new proof in December 1996.The proof in the preprint contained all the main ideasbut many details were left out.
And then it took me 7 years to work out these detailsand to publish a paper with a complete proof ...
And I was lucky!
The ideas which the proof was based on turned out to be solidand the results of other people which I relied on turned out to be correct.
This is not always the case.
Let me tell you the story of another of my proofs which turned out very differently.
In 1987, I was introduced to Mikhail Kapranov.I was an undergrad at Moscow University and he was a graduate student.
We immediately discovered that we are both dreaming ofdeveloping new "higher dimensional" mathematicsinspired by the concepts of higher category theory.
We started to work together.It was great fun.Doing mathematics with someone from whom you can learn,while discovering together things which are new both for you and for the worldis an amazing and powerful experience.
In the summer of 1990, by recommendation of Kapranov,I was accepted to the graduate school of Harvard without having to apply.In the Fall of 1990 I left the Soviet Union and the american period of my life began ...
Kapranov and I wrote a paper about the key conjecture of the new "higher dimensional" mathematicsthat was due to Alexander Grothendieck,
the intuition appeared that infinity-groupoidsshould constitute particularly adequate models for homotopy types,the n-groupoids corresponding to truncated homotopy types (with pi(i) = 0 for i > n).
-- Esquisse d'un Programme 1984
The conjecture was not a precise onesince what should be the definition of an infinity-groupoid remained open.
Kapranov and I decided that we know what the definition should beand how to prove the conjecture with this definition.
We wrote a paper with a sketch of the proofand published it in one of the best Russian mathematical journalsand the paper with the complete proof was publishedin the proceedings of a conference that we have been invited to.
We felt that the issue with this conjecture is closedand that this important element of "higher dimensional" mathematics had been understood.
Then in 2003, twelve years after our proof was published in English,a preprint appeared on the web in which Carlos Simpson,very politely, claimed that he has constructed a counter-example to our theorem.
I was busy with the work on the motivic programand very sure that our proof is correctand ignored the preprint.
Then the motivic period of my life was completedand I started to work on computer proof verificationand new foundations of mathematics.
The correspondence between the infinity-groupoids and homotopy typesre-emerged as the cornerstone of the Univalent Foundations.
And then in the Fall of 2013,some sort of a block in my mind collapsedand I suddenly understood that Carlos Simpson was correctand that the proof which Kapranov and I published in 1991 is wrong.
Not only the proof was wrong but the main theorem of that paper was false!.
In this story I got lucky again.
The theorem was false with the particular definition of infinity groupoidswhich Kapranov and I have used.There were by now various other definitionswith which the statement of the theorem became correct.
The use of the Grothendieck correspondence,as it became known, in the Univalent Foundationswas not endangered.
But belief in the correctness of our false theoremplayed an important and negative rolein how I perceived, for all these years, the subject area of multidimensional category theory.
Because I believed in something which was false,I could not believe other things which were true,because they contradict each other.
So I could not understand the work of others in this area.
When I recognized that the theorem of the paper is falseI contacted Kapranov to tell him thatwe need to do something about the paperand to tell Carlos Simpson that his preprint from 2003 is correct.
An interesting feature of this story is thatCarlos Simpson did not point out where in the proof,which was about 10 pages long, the mistake was.He only showed that it can not be correctby building a counter-example to the final statement.
It took me several weeks to find which particular lemma in the paper is incorrectand to find counterexamples to that lemma.
There no ending to this story yet.
The question that we originally wanted to answer-- how to find an algebraic definition of infinity groupoidsthat would satisfy the Grothendieck correspondence,remains open...
Now let us look at this story again.
Kapranov and I have found a solution to the problem which we worked on-- the proof of the theorem.
If the problem was to solve an equationand we would have found a solutionwe would have checked that it is a solution before publishing it, right?
And if it were a complex equationwe would probably have checked it on a computer.
So why can not we check a solution which is a proof of a theorem?
I started to ask myself this question more than 10 years agowhen the solutions, proofs, which I was inventingwere becoming more and more complexand I was getting more and more worried that they may contain mistakes.
And trying to answer this questionled me to my current interest in Foundations of Mathematics.
Let me explain how.
A solution to an equation would probably be a number or a collection of numbers.
Verification in this case would consist in performing some computations with these numbersand comparing the result of these computations with some other numbers.
But what should we do when the solution is a proof of a statement?
A hint can be seen from looking at the casewhen the problem was to solve an equation in symbolic form.For example, to find a formula for solvinga general equation of the form x^3 + a*x + b = 0.
How would we check the solution in this case?We would probably use some software for symbolic computationwhich can compute not only with numbersbut also with expressions which have variables in them.
So in order to check a solution which is a proof of a statementwe need to write both the statement and the proof as some kind of symbolic expressionslet's say T for the statement, and A for the proof,and then use some software which can compute with theseexpressions in such a way as to check that A is indeed a proof of T.
Encoding of statements and proofswhich exist in our thoughtsinto symbolic expressionsis called formalization.
Formalization is, just like programming, first of all a toolthat we can use to pass on to computerssome of the mental tasks which we need to perform.
But at the moment it is much less developed than programmingand when I started to search, in 2003, for a formalization systemthat I could use to help me check my proofs I could not find any.
I decided that I need to create such a system.
The first question to answer waswhat was it that prevented the creation of such a system earlier?
What is involved in the creation of a formalization systemsfor use in mathematics?
First of all we need to have a some knowledgeabout how to design formal deduction systemswhich are for formalization what programming languages are for programming.
The theory of formal deduction systems originated, as far as I could find, withan amazing paper by Gottlob Frege from 1879 which is called"A formula language, modeled upon that of arithmetic, for pure thought".
Today it is studied mainly in Computer Science "Theory B".
By the way, it is "Theory B"not because it is less important than "Theory A"but because of a Handbook of Theoretical Computer Sciencewhich was published in two volumes "A" and "B"and the theory of formal deduction systems was discussed in the second volume.
The "Theory A", is much better knownin many country of Asia, and in America, and in Israel.It is mostly concerned with complexity and algorithms.
The "Theory B" is concerned with the theory and design of programming languages.
The "B" here actually means it is more difficult,because more simple things are discussed in the first volume,and more complex things are discussed in the second volume.
But the theory of formal deduction systemsis only one part of what we needto formalize mathematical statements and proofs.
This theory studies all possible formal deduction and computation systems.Whether a given system formally represents some actual system of reasoningwhich is used in the world of thoughtis of no concern to this theory.
It is like the theory of general differential equations,so it studies all differential equations,and does not care whether some differential equationsdescribe some actual process in real world or not.
For proof verification we need to construct a particular formal deduction systemand explain how it corresponds with the mathematical objectsand forms of reasoning which exist in our thoughts.
Constructing such systems and correspondences between their formal componentsand objects and actions in the world of our mathematical thoughtsis the main task of the field which is called Foundations of Mathematics.
This is what Foundations of Mathematics is about,it is about connecting the world of our thoughts to objects in formal systems,which will help us to manipulate our thoughts.
A formal deduction system together with a correspondencebetween its components and objects and actions in the world of mathematical thoughtswhich can be used to formalize all subject areas of mathematicsis called a foundational system for mathematics or "Foundations of Mathematics".
Of course this is not how "Foundations of Mathematics" is formulatedback when I was in Moscow University.It was formulated very differently,if it was formulated like this,I will think it would be very very cool,but it was not.
And this is how we look at it now.
If you have a system which can give you formulaecorresponding to your thoughts about numbers,that would be a numbers system.
The earliest things like Foundations of Mathematics were the number systems,these were the systems which allow people to write numbers,which were objects of their simple mathematical thoughts.
They write numbers as symbols and to manipulate symbolsto compute practical things about numbers in the world.
For example, How to compute "How many bricks is needed to build a wall of some size".
That was mathematics at that time,and the Foundations of Mathematics at that time is a number system.
Today mathematics is much wider.
And the Foundations of Mathematics,is supposed to be some analog of number systems,but for the mathematical thoughts aboutmuch more abstract objects which we are dealing with today.
The mainstream foundation of classical pure mathematicsis called Zermelo-Fraenkel Set Theory with the Axiom of Choice or ZFC,by the name of the axiomatic system of predicate logic which it uses.
ZFC is a formal deduction system,In which the way to establish the correspondence between mathematical objects and our thoughtsis called set theoretical mathematics.
That is what the Bourbaki group did for many years in some areas of mathematics.
It is a very beautiful foundation when you understand it.
It was created in the first decades of the 20th century before computers came into existenceand before the problem of formalization of actual complex proofs became relevant.
Before there were computers, no one thought about actually formalizing complex proofs,because it was too difficult to do without computers.
In part because of it was designed to be used with mathematics of that timeit is not well adapted to the mathematics of the 21st century.It is not well adapted to the task of computer proof verification.
To be able to check my proofsas one can check solutions to equationsI needed new foundations of mathematics.
And this is how I became interested in foundations of mathematics ...
I came up with the main ideas of Univalent Foundations in 2006.Only one element was missing and it took me three years to find it.
In the Fall of 2009 I gave the first public lecture about the "univalent model"-- a mathematical construction which connects Martin-Löf's Type Theory to ZFCin a new, unexpected, way.
By the Spring of 2010 I have recognized thatI had a working version of a new formalization systembased on a new foundational system that I called Univalent Foundations.
In the academic year 2012/13, Thierry Coquand, Steve Awodey and myselforganized a special program at the Institute for Advanced Study in Princeton where I work.
During that year the participants of the program wrote, together, a bookcalled "Homotopy Type Theory".
Type these words in Googleand you will be directed to a websitewhere you can learn more about this new subjectand also download the book for free.
The book is a truly collective effortand as such it does not have an author.The person who did most to make this book happenand who continues to shape the content and the style of the bookis Michael Schulman.
On June 21, 2014 Univalent Foundations passed another important milestone.Thierry Coquand gave a talk about Univalent Foundations at the Bourbaki Seminar in Paris.Being chosen for a presentation on this seminaris widely considered to be an important symbol of recognitionin the world of pure mathematics.
Thierry and his colleagues are also the authors of the most important advancein the mathematics of Univalent Foundations since their invention.They have constructed another model,similar to the original "univalent model" of 2009but based on constructive mathematics.
This model opens up the wayfor wider Univalent Synthesis of classicaland constructive mathematics ...
Questioner asked about the used of proof assistants.
Voevodsky: Proof assistants can be extremely useful,just like musical instrument,you can use it to practise,in the circumstance where you do not have a teacher.
Questioner asked about how to improve "mathematical sense".
Voevodsky: By doing a lots and lots and lots detailed proofs and computations,for hours and hours, and days and days, and month and month, and years.trying to examine different areas of mathematics,then it all some how connected in your head in some general view.
To use such "mathematical sense" to find new proofs,When I was younger I would spending lots and lots of hourswriting things on paper, thinking and writing again,and drinking a lot of strong tea,walking around and rotating these things in my head over and over again.
As I become older I do not do this much, or at least I try not to.And I usually try to just formulate a question very precisely,to make sure it only has one meaning,to place it in my head, to have it there firmly for sometime,then I forget about it and do other things,and I wait for the answer to come.