Timeline for Mathematicians whose works were criticized by contemporaries but became widely accepted later
Current License: CC BY-SA 3.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 14, 2013 at 5:52 | comment | added | Andrej Bauer | @Asaf: I am not going to discuss with you in such an argumentative manner. Tone it down, please. | |
| Feb 13, 2013 at 20:20 | comment | added | Asaf Karagila♦ | @Andrej: Really? Never? Do I need to supply any of the copious amounts of things that throughout the history were thought to "never happen"? Are you claiming that those people who work on proof assistants are flawless? If so I really need to ask them a few questions. | |
| Feb 13, 2013 at 19:48 | comment | added | Andrej Bauer | @arsmath: mathematicians will not become obsolete because some new tool has been invented, but the nature of their work might change. Also, formalizing constructive math is no easier or harder than formalizing classical math. When we know how to automate one, we'll know how to automate the other one. | |
| Feb 13, 2013 at 19:48 | comment | added | Andrej Bauer | @Asaf: you should read mathoverflow.net/questions/18421/… Of course your scenario can never happen, because people who write proof assistants worry a lot about your scenario and have devised methods for making sure that the risks are minimized. In any case, even with existing technology you can trust formalized proofs a lot more than published proofs. | |
| Feb 13, 2013 at 19:22 | comment | added | Asaf Karagila♦ | @arsmath: If we are considering apocalyptic extensions to Andrej's proof assistant scenario, consider the case where a bright mathematician which is also a hacker stumbles upon a bug which allows him (or her) to prove anything, and this bug is so deep within the software that no one would find it otherwise; this genius publishes tons of groundbreaking theorems (with the hidden contradiction), after three decades of work built upon those theorems the contradiction is found, everything is collapsed... all constructivists get ridiculed for having mathematicians waste half a century. | |
| Feb 13, 2013 at 17:25 | comment | added | Asaf Karagila♦ | The late 21st century? Are you predicting the future? Please let me know what are the lottery numbers for the next weeks. | |
| Feb 13, 2013 at 9:28 | comment | added | arsmath | And then two years later, computer scientists figure out how to promote the assistant to the boss, and now that mathematics has been automated, all human mathematicians become instantly obsolete. Alternate scenario: thanks to the proof assistants, the world's supply of constructive theorems can be supplied by one guy in his basement and constructivism dies as an active research project. Since constructive proof assistants are a solved problem, all of the grant money in computer science goes to the unsolved problem of proof assistants for ZFC. | |
| Feb 13, 2013 at 6:12 | comment | added | Andrej Bauer | @Lasse: you give mathematicians too much credit. What they like and how they work (or say they work) depends on socioeconomic factors. Here's a scenario: computer scientists create veru useful proof assistants, based on type theory; computer science gets loads more money than mathematics; mathematicians jump onto the type theory bandwagon because they get paid, and computer helps them do math. Mathematicians don't care whether they use ZFC, or whether they need choice, or excluded middle. They just do math, and if they could do it in some other setting, they might. | |
| Feb 12, 2013 at 20:17 | comment | added | arsmath | Intuitionistic logic is of mathematical interest. Some things are intuitionistic, the way some things are nonabelian groups. | |
| Feb 12, 2013 at 16:01 | comment | added | Lasse Rempe | The majority of mathematicians will never switch to constructive mathematics, at least not until a contradiction is discovered in ZFC. :) Even in the (rather unlikely) event that this happens, it is far more likely that some weaker, still non-constructive, set of axioms is going to be used. The mathematical world we work in is too powerful and convenient to give up without good reason. Of course this doesn't mean that the study of intuitionistic logic isn't interesting from a foundational point of view. | |
| Feb 12, 2013 at 13:46 | comment | added | Andrej Bauer | Let's hope you are correct about the 22nd century. (Maybe you are because computers won't be programmed to crack jokes while proving theorems.) P.S.: to formalize classical mathematics in Martin-Löf type theory, use the 0-truncated types with a couple of extra axioms. | |
| Feb 12, 2013 at 13:38 | comment | added | arsmath | Yes, yes, yes, and 1/2 yes. (How do you formalize classical mathematics in Martin-Lof type theory? Doesn't strong normalization prevent it?) My point is that unless you are a constructivist, Martin Lof type is just another thing you can study, like complex analysis, or homological algebra, or whatever. People who study the fundamental groups of hyperbolic 3-manifolds don't make fun of 19th century complex analysts. There's no reason why type theorists of the 22nd century need to make fun of today's set theorists. | |
| Feb 12, 2013 at 13:23 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 182 characters in body; added 16 characters in body; deleted 13 characters in body; added 1 characters in body
|
| Feb 12, 2013 at 12:36 | comment | added | Andrej Bauer | But it did happen in the late 21st century ;-). Anyhow, are you aware of the uses of Martin-Löf type theory outside constructivism? Say in homotopy theory, or in programming languages, or in formalization of mathematics (constructive and classical)? | |
| Feb 12, 2013 at 12:06 | comment | added | arsmath | This will never happen. There's no trade-off between ZF and Martin-Lof type theory, unless you are explicitly philosophically committed to constructivism. As a proportion of mathematicians, classical complex function theory is a much smaller proportion of mathematics than it was in the late 19th century, but nobody makes fun of complex analysts. | |
| Feb 12, 2013 at 11:13 | comment | added | boumol | My mistake, I was reading late 20th century. @Bauer:I haven't downvote yet, I will wait for the late 21st century. | |
| Feb 12, 2013 at 11:07 | comment | added | Zhen Lin | @boumol: The late 21st century is still some way off, but we can hope... | |
| Feb 12, 2013 at 11:01 | comment | added | boumol | @Bauer: Do you really think that at some moment "most mathematicians were educated in the tradition of constructive Martin-Löf type theory"? | |
| Feb 12, 2013 at 10:52 | history | answered | Andrej Bauer | CC BY-SA 3.0 |