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]

"Voevodsky's Unachieved Project", by Andrei Rodin https://arxiv.org/abs/2012.01150

"In view of the second goal Voevodsky in 2004 started to develop a mathematical theory of Population Dynamics, which involved the Categorical Probability theory. This latter project did not bring published results and was abandoned by Voevodsky in 2009 when he decided to focus his efforts on the Univalent foundations and closely related topics. In the present paper, which is based on Voevodsky's archival sources, I present Voevodsky's views of mathematics and its relationships with natural sciences, critically discuss these views, and suggest how Voevodsky's ideas and approaches in the applied mathematics can be further developed and pursued. A special attention is given to Voevodsky's original strategy to bridge the persisting gap between the pure and applied mathematics where computers and the computer-assisted mathematics have a major role."

[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.

[timelets]

Thanks!

[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

[juan_gandhi]

I have the link at wowiki

[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

[dmm]

Thanks!

[dmm]

I finally finished posting them :-)

(I was looking at all this a week ago, except for the first of those links (I was looking at that one a week before the New Year))

[timelets]

Appreciate it. Good to have the references in one place.