Voevodsky links

[dmm]

I have been looking at some links related to Voevodsky in recent weeks, and the easiest way to share a collection of links is to put them into comments in a blog post...

Comments

[dmm]

I was reading this

https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

and this led me to https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/

[dmm]

The memorial site: https://www.math.ias.edu/Voevodsky/

Some of the links there were of particular interest to me.

[dmm]

This newsletter https://www.ias.edu/sites/default/files/pdfs/publications/letter-2014-summer.pdf

has Voevodsky's interesting text on pages 8-9, and also a text on neurophenomenology called "Neurophilosophy and Its Discontents" on pages 5-6.

[dmm]

Voevodsky teacher and co-author was my math analysis teacher in a Moscow math high school during the two final years of high school and influenced me quite a bit.

Here is an interview with him (in Russian):

https://otr-online.ru/programmy/gamburgskii-schet/georgii-shabat-voevodskii-30754.html

https://www.youtube.com/watch?v=RRcJCF4AwPU

English translation: https://www.math.ias.edu/Voevodsky/other/Orlova.pdf

[dmm]

Then on related topics, in connection with other senior people in the Univalent foundations program and Homotopy Type Theory and on their involvement with sheaves.

Of course, what Voevodsky had being doing with motives was closely related to Grothendieck, for whom sheaves were quite central.

And I knew about Steve Awodey https://www.andrew.cmu.edu/user/awodey/ and, among other things, his work on sheaf-based topological "possible worlds" interpretation of first-order predicate modal logic: https://www.andrew.cmu.edu/user/awodey/preprints/FoS4.phil.pdf (a statement at a world which is a fiber over a base space point is necessary (necessarily true), if there is a neighborhood around that base space point such that this statement is true in all worlds over all base space points in that neighborhood; similarly, a statement at a world over a base space point is possible (possibly true), if there are base points arbitrarily close to our selected base points, such that this statement is actually true in those worlds).

But it turns out that Thierry Coquand (Coq is named after him) also uses sheaves quite a bit in his work: http://www.cse.chalmers.se/~coquand/

E.g. http://www.cse.chalmers.se/~coquand/potential.pdf also http://www.cse.chalmers.se/~coquand/notes.txt etc.

[dmm]

Finally, less related to Voevodsky, but more related to "How Close Are Computers to Automating Mathematical Reasoning?"

"Explosive Proofs of Mathematical Truths", https://arxiv.org/abs/2004.00055

"Mathematical Reasoning via Self-supervised Skip-tree Training", https://arxiv.org/abs/2006.04757