Carnegie Mellon University has been awarded a whopping $7.5 million Dept. of Defense grant "to reshape the foundations of mathematics by developing a new approach that allows for large-scale formalization and computer verification," arriving at a "new, computational foundation for mathematics," based on "homotopy type theory"... a combination of 'homotopy theory' and 'type theory':
https://www.cmu.edu/news/stories/archives/2014/april/april28_awodeygrant.html#.U2An4hZDTn4
The press release ends thusly:
"CMU's Steven Awodey and his research team will use a $7.5 million grant from the Department of Defense to reshape the foundation of mathematics, building on his groundbreaking discovery in 2005 of a connection between abstract, mathematical geometry and computational logic."I had trouble finding any references or descriptions of 'homotopy type theory' that I felt the average reader (including MYSELF!) could follow well. But this year-old post from Christian Perfect helps some:
http://aperiodical.com/2013/06/homotopy-type-theory-a-new-foundation-for-21st-century-mathematics/
and Christian's piece has other links including this introduction to the subject:
http://www.carloangiuli.com/blog/homotopy-type-theory-univalent-foundations-of-mathematics/
Homotopy type theory tries to unify the foundations of mathematics that were originally shattered when set theory fell victim to Russell's Paradox. Needless to say, it's a fairly cutting-edge area of mathematical thought that apparently shows a lot of promise. Indeed, I find it fascinating that the Defense Dept. is pouring money into it... but that's partly my naivete in associating the DOD with more practical 'hardware' sorts of expenditures... they of course back LOTS of more abstract study; it's just not what most people think of front-and-center when you say "Department of Defense!" Anyway, not bad funding if you can get it! ;-)
No comments:
Post a Comment