> More recently he became interested in type-theoretic formalizations of mathematics and automated proof verification. He was working on new foundations of mathematics based on homotopy-theoretic semantics of Martin-Löf type theories. His new "Univalence Axiom" has had a dramatic impact in both mathematics and computer science.
And some of his online lectures outlining his reasoning and motivations became greatly influential on my own interests.
It's quite technical to describe what that is, but the general idea is that he imported homotopy theory, a fundamental concept in mathematics which allows you to describe topology with an algebra of paths in that geometry, to algebraic geometry. This allowed him to solve some major open problems in the field.
Topology is essentially the study of continuity and the properties that are invariant of objects under continuous deformation. The prototypical example of a topological space is the continuum although the concept of continuity has been generalized a great deal. Homotopy is the study of continuous paths which are defined as continuous functions from the unit interval into topological spaces, as well as higher dimensional "paths". It turns out that these paths have a rich algebraic structure which give you a strong idea of what the "shape" of the space is like.
Classically algebraic geometry is the study of solutions to systems of polynomial equations over systems of numbers related to the integers, rationals, reals, and complex numbers. More modernly, it is the study of models of theories that resemble the previously mentioned theory in fundamental ways. For example, the theory of elliptic curves which underlies some of our modern cryptography is part of algebraic geometry.
I think topology is mentioned in recent Microsoft Ignite Quantum Computing discussions from at least 1 panel who is a mathematician. I wonder how it might be related.
Since you didn't include it, but it's relevant to the topic at hand -- Michael Freedman is also a Fields medalist that did substantial work in topology. Which is, ultimately, why he's involved with Station Q -- he was part of the group that realized you could use the topological structure of certain interactions to encode general computations, and was part of convincing MS to pursue that.
Not sure who else might have a device that can instantiate in some physical way a Quantum Superposition, but Microsoft showed such a device during that discussion: https://youtu.be/d7f_GZsQMpA?t=1h3m6s
Not the op, but basically Voevodsky realized that the notion of equality in type theories as implemented in Coq or Agda is fundamentally more fine grained than what mathematicians are used to thinking of. This mismatch causes problems when formalizing mathematics in type theory.
Voevodsky proposed the univalence axiom which can be used to obtain more equalities and gave rise to the field of homotopy type theory (HoTT).
An intuition about the univalence axiom is that it allows to regard isomorphic types as equal. (This isn't entirely correct but gives a good intuition). The consequences of the axiom are severe (probably in a good way) but a lot more research is needed.
The hopes are that the work on HoTT will make it easier to formalize mathematics and in turn make it easier to verify software.
I became familiar with his work through HoTT --
> More recently he became interested in type-theoretic formalizations of mathematics and automated proof verification. He was working on new foundations of mathematics based on homotopy-theoretic semantics of Martin-Löf type theories. His new "Univalence Axiom" has had a dramatic impact in both mathematics and computer science.
And some of his online lectures outlining his reasoning and motivations became greatly influential on my own interests.