[FOM] fom topics in Notices of AMS

David Roberts david.roberts at adelaide.edu.au
Sun Sep 7 19:45:10 EDT 2014

Note also, in the Bulletin, something that I hope would be interesting
to fom readers.

Homotopy type theory and Voevodsky’s univalent foundations
Álvaro Pelayo and Michael A. Warren.
Bull. Amer. Math. Soc. 51 (2014), 597-648

Note that the paper, with a few omissions that are supplied in
supplemental files attached to the arXiv version of the article, goes
from nothing to proving (a version of) Whitehead's theorem
(http://www.wikiwand.com/en/Whitehead_theorem), *formally in UF*, with
friendly explanation interspersed. I don't know about you, but I
imagine a formal ZFC proof (say in Mizar) of the same would be a lot


On 7 September 2014 12:09, John Baldwin <jbaldwin at uic.edu> wrote:
> Fermat, Leibniz, Euler, and the Gang: The True History of the Concepts of
> Limit and Shadow
> Tiziana Bascelli, Emanuele Bottazzi, Frederik Herzberg, Vladimir Kanovei,
> Karin U. Katz, Mikhail G. Katz, Tahl Nowik, David Sherry and Steven Shnider
> This is a longish article on the development of infinistessimals in
> analysis. It is a blend of history, philosophy and mathematics
> There are also two reviews of 5 books on Turing
> http://www.ams.org/notices/201408/index.html
> John T. Baldwin
> Professor Emeritus
> Department of Mathematics, Statistics,
> and Computer Science M/C 249
> jbaldwin at uic.edu
> 851 S. Morgan
> Chicago IL
> 60607
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

Dr David Roberts
Research Associate
School of Mathematical Sciences
University of Adelaide
SA 5005

More information about the FOM mailing list