Vladimir Voevodsky - What if Current Foundations of Mathematics are Inconsistent

Talk given at the Institute of Advanced Studies at Princeton in 2010.

It's good that some people were allowed to talk about this. See About Logic Interview with Urs Schreiber and in particular Lawvere's Cohesive Toposes and Cantor's 'iaufcer Einsen'. 

The answer is to use a plurality of formal systems and a plurality of formal translations between those systems. Then the provable sentences are not vulnerable to such accidental coincidences of interpretation which are constructed by diagonalisations such the Gödel sentences. This is just a greatest fixpoint. Unfortunately it depends upon mathematicians and logicians actually speaking to one another. 

See An Excellent Talk about Computability and Hilbert's Entscheidungsproblem. 

Subscribe to Institute of Advanced Studies. 

Talk at the he IMU in September 2016, a year before he died. 

"... it came out, as a result of practical work on formalization we just discovered that the law of excluded middle and axiom of choice can be avoided in the univalent foundations much more successfully than they can be avoided in set theory, so things which can not be done without them in set theory can be done without them in the univalent foundations, so then there was this understanding that the classical mathematics appears as a subset of this new constructive mathematics. That is actually kind of an easy easy thing to see, but it's important to emphasize that one obtains the view of mathematics as constructive and then the classical mathematics as a subset of this constructive mathematics, a very important subset, and it's kind of a retract: it's not only a subset but it's it's a retract, but it's still a subset" And he goes on: "The understanding that the MLTT extended with the UA is an imperfect formalization system for this constructive mathematics and that it should be possible to integrate the UA into the MLTT obtaining a new type theory with better computational properties." See Emily Riehl on Univalent Foundations. 

Voevodsky's slides for this talk are still available from the IAS. 

Subscribe to Heidelberg Laureate Forum. 

Lecture given at University of Cambridge on 10th Jul 2017

7:43 

This appeared on YouTube on 15th December 2025:

Abstract: UniMath refers to several things. It is a univalent foundation of mathematics. It is the subset of Coq in which this foundation is currently implemented and it is a library of formalized mathematics written using this implementation. My talk will be mostly about the library. I will give examples of problems whose constructions have been recently formalized in the UniMath as study problems by graduate students. I will give an example of a more complex problem whose construction has been recently formalized as a part of a paper accepted to a conference proceedings. Finally, I will outline a direction for the future development of the UniMath that requires constructions to considerably more complex problems that can only be stated in the univalent type theory and, as far as I know, have never been solved either formally or informally.

Subscribe to INI Seminar Room 1.

Recent talk on HoTT by Steve Awodey at Cambridge, two months ago,... 

36:53 Question about metrics on homotopy spaces and an answer about synthetic differential geometry. See About Logic Interview with Urs Schreiber. 

Subscribe to Tiansi Dong. 

He is still alive, or he was a couple of days ago,...

Subscribe to Topos Institute. 

Andrej Bauer a few months ago. Starts at 5:22, if you pay them.

See his blog https://math.andrej.com/ and this entry for October 11th 2022 Happy birthday, Dana!. Also Selected Papers of Dana S. Scott. 

20:05 He explains how sheaf toposes motivate constructive mathematics in physics. On denotational stability, see Assumptions of Physics - Symplectic Group and Uncertainty on continuous functions on measure spaces and Frederic Schuller on Metric and Topological Spaces on observables and measurements. 

9:48 On relativistic views on mathematics. See my remark above. 

51:21 On using foundational methods to do interesting mathematics. Examples are countable models of the real numbers (see The Countable Reals by Andrej Bauer and James E. Hanson) and synthetic differential geometry (see Outline of synthetic differential geometry by F.W. Lawvere). See also About Logic Interview with Urs Schreiber. 

1:59:16 Discussion about the direction lean/mathlib took and why it made a bigger impact on the mathematics community as a whole. See the discussion in their leanprover-community / mathlib archive. 

Subscribe to Type Theory for All.