Welcome to DU!
The truly grassroots left-of-center political community where regular people, not algorithms, drive the discussions and set the standards.
Join the community:
Create a free account
Support DU (and get rid of ads!):
Become a Star Member
Latest Breaking News
General Discussion
The DU Lounge
All Forums
Issue Forums
Culture Forums
Alliance Forums
Region Forums
Support Forums
Help & Search
The Revolution Will Not Be Formalized
https://golem.ph.utexas.edu/category/2015/05/the_revolution_will_not_be_for.html
May 18, 2015
The Revolution Will Not Be Formalized
Posted by Mike Shulman
After a discussion with Michael Harris over at the blog about his book Mathematics without apologies, I realized that there is a lot of confusion surrounding the relationship between homotopy type theory and computer formalization — and that moreover, this confusion may be causing people to react negatively to one or the other due to incorrect associations. There are good reasons to be confused, because the relationship is complicated, and various statements by prominent members of both communities about a “revolution” haven’t helped matters. This post and its sequel(s) are my attempt to clear things up.
<snip>
What is the future of computer-verified proof? Is it the future of mathematics? Should we be happy or worried about that prospect? Does it mean that computers will take over mathematics and leave no room for the humans? My personal opinion is that (1) computer-verified proof is only going to get more common and important, but (2) it will be a long time before all mathematics is computer-verified, if indeed that ever happens, and (3) if and when it does happen, it won’t be anything to worry about.
The reason I believe (2) is that my personal experience with computer proof assistants leads me to the conclusion that they are still very far from usable by the average mathematician on a daily basis. Despite all the fancy tools that exist now, verifying a proof with a computer is usually still a lot more work than writing that proof on paper. And that’s after you spend the necessary time and effort learning to use the proof assistant tool, which generally comes with quite a passel of idiosyncracies.
Moreover, in most cases the benefits to verifying a proof with a computer are doubtful. For big theorems that are very long or complicated or automated, so that their authors have a hard time convincing other mathematicians of their correctness by hand, there’s a clear win. (That’s one of the reasons I believe (1), because I believe that proofs of this sort are also going to get more common.) Moreover, a certain kind of mathematician finds proof verification fun and rewarding for its own sake. But for the everyday proof by your average mathematician, which can be read and understood by any other average mathematician, the benefit from sweating long hours to convince a computer of its truth is just not there (yet). That’s why, despite periodic messianic claims from various quarters, you don’t see mathematicians jumping on any bandwagon of proof verification.
<snip>
May 18, 2015
The Revolution Will Not Be Formalized
Posted by Mike Shulman
After a discussion with Michael Harris over at the blog about his book Mathematics without apologies, I realized that there is a lot of confusion surrounding the relationship between homotopy type theory and computer formalization — and that moreover, this confusion may be causing people to react negatively to one or the other due to incorrect associations. There are good reasons to be confused, because the relationship is complicated, and various statements by prominent members of both communities about a “revolution” haven’t helped matters. This post and its sequel(s) are my attempt to clear things up.
<snip>
What is the future of computer-verified proof? Is it the future of mathematics? Should we be happy or worried about that prospect? Does it mean that computers will take over mathematics and leave no room for the humans? My personal opinion is that (1) computer-verified proof is only going to get more common and important, but (2) it will be a long time before all mathematics is computer-verified, if indeed that ever happens, and (3) if and when it does happen, it won’t be anything to worry about.
The reason I believe (2) is that my personal experience with computer proof assistants leads me to the conclusion that they are still very far from usable by the average mathematician on a daily basis. Despite all the fancy tools that exist now, verifying a proof with a computer is usually still a lot more work than writing that proof on paper. And that’s after you spend the necessary time and effort learning to use the proof assistant tool, which generally comes with quite a passel of idiosyncracies.
Moreover, in most cases the benefits to verifying a proof with a computer are doubtful. For big theorems that are very long or complicated or automated, so that their authors have a hard time convincing other mathematicians of their correctness by hand, there’s a clear win. (That’s one of the reasons I believe (1), because I believe that proofs of this sort are also going to get more common.) Moreover, a certain kind of mathematician finds proof verification fun and rewarding for its own sake. But for the everyday proof by your average mathematician, which can be read and understood by any other average mathematician, the benefit from sweating long hours to convince a computer of its truth is just not there (yet). That’s why, despite periodic messianic claims from various quarters, you don’t see mathematicians jumping on any bandwagon of proof verification.
<snip>
6 replies
= new reply since forum marked as read
= new reply since forum marked as read
The article was written by Mike Shulman on one of John Baez' blogs.
http://en.wikipedia.org/wiki/Michael_Shulman_%28mathematician%29
Michael Shulman (1980) is an American mathematician at the University of San Diego who works in category theory and higher category theory, homotopy theory, logic as applied to set theory, and computer science. He did his undergraduate work at the California Institute of Technology and his postgraduate work at the University of Cambridge and the University of Chicago, where he received his Ph.D. in 2009.
<snip>
Michael Shulman (1980) is an American mathematician at the University of San Diego who works in category theory and higher category theory, homotopy theory, logic as applied to set theory, and computer science. He did his undergraduate work at the California Institute of Technology and his postgraduate work at the University of Cambridge and the University of Chicago, where he received his Ph.D. in 2009.
<snip>
http://en.wikipedia.org/wiki/John_C._Baez
John Carlos Baez (/ˈbaɪ.ɛz/; born June 12, 1961) is an American mathematical physicist and a professor of mathematics at the University of California, Riverside (UCR)[1] in Riverside, California. He is known for his work on spin foams in loop quantum gravity.[2][3] For some time, his research had focused on applications of higher categories to physics and other things.[4]
Baez is also known to science fans as the author of This Week's Finds in Mathematical Physics,[5] an irregular column on the internet featuring mathematical exposition and criticism. He started This Week's Finds in 1993 for the Usenet community, and it now has a worldwide following in its new form, the blog "Azimuth". This Week's Finds anticipated the concept of a personal weblog.[6] Additionally, Baez is known on the World Wide Web as the author of the crackpot index.
<snip>
Blogs
Baez runs the blog "Azimuth," where he writes about a variety of topics ranging from This Week's Finds in Mathematical Physics to the current focus, combating climate change and various other environmental issues.
Baez is also co-founder of the n-Category Café (or n-Café), a group blog concerning higher category theory and its applications, as well as its philosophical repercussions. The founders of the blog are Baez, David Corfield and Urs Schreiber, and the list of blog authors has extended since. The n-Café community is associated with the nLab wiki and nForum forum, which now run independently of n-Café. It is hosted on The University of Texas at Austin's official website.
Family
Singer and progressive activist Joan Baez is his cousin and her father, physicist Albert Baez, was his uncle.[7]
John Baez is married to Lisa Raphals who is a professor of Chinese and comparative literature at UCR.[8][9]
<snip>
Fields: Mathematics, Physics
Institutions: University of California, Riverside
Alma mater: Princeton University (undergraduate)
Massachusetts Institute of Technology(Ph.D)
Yale University (Postgraduate)
John Carlos Baez (/ˈbaɪ.ɛz/; born June 12, 1961) is an American mathematical physicist and a professor of mathematics at the University of California, Riverside (UCR)[1] in Riverside, California. He is known for his work on spin foams in loop quantum gravity.[2][3] For some time, his research had focused on applications of higher categories to physics and other things.[4]
Baez is also known to science fans as the author of This Week's Finds in Mathematical Physics,[5] an irregular column on the internet featuring mathematical exposition and criticism. He started This Week's Finds in 1993 for the Usenet community, and it now has a worldwide following in its new form, the blog "Azimuth". This Week's Finds anticipated the concept of a personal weblog.[6] Additionally, Baez is known on the World Wide Web as the author of the crackpot index.
<snip>
Blogs
Baez runs the blog "Azimuth," where he writes about a variety of topics ranging from This Week's Finds in Mathematical Physics to the current focus, combating climate change and various other environmental issues.
Baez is also co-founder of the n-Category Café (or n-Café), a group blog concerning higher category theory and its applications, as well as its philosophical repercussions. The founders of the blog are Baez, David Corfield and Urs Schreiber, and the list of blog authors has extended since. The n-Café community is associated with the nLab wiki and nForum forum, which now run independently of n-Café. It is hosted on The University of Texas at Austin's official website.
Family
Singer and progressive activist Joan Baez is his cousin and her father, physicist Albert Baez, was his uncle.[7]
John Baez is married to Lisa Raphals who is a professor of Chinese and comparative literature at UCR.[8][9]
<snip>
