[FOM] fom topics in Notices of AMS

[David Roberts]

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
http://www.ams.org/journals/bull/2014-51-04/S0273-0979-2014-01456-9/

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

Regards,
David





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
AUSTRALIA