6 ms·

There’s more to mathematics than rigour and proofs

119 points by 001sky 14y ago

dsirijus 14y ago
Well, suggested solution of this problem seems kinda backwards to me. I'd much prefer something along the lines of what Stephen Wolfram suggests - offload computation to computers in the first pre-rigorous stage, which may enable building of the foundation in a more rigorous manner right from the start. Even at rigorous stage, offloading computation increases dramatically exposure to solutions and builds intuition faster by orders of magnitude.
- josephagoss 14y ago
  What does this mean? For example I self-teach myself math at the moment, easy stuff like calculus. I'm still trying to get my head around it all. How can I offload computation to build up intuition faster? Any tips? (I love programming if that helps)
  - dsirijus 14y ago
    Particulary in starting calculus, after laying out the foundation of real numbers, exercises pretty soon start with determing limits, inflexion points, trends, and all. Sure, play with those at first by hand, but try to plot and play with those functions in, say, Mathematica. Pretty soon you'll be able to intuitively "know" how any of the functions you could be thrown at exams should look like, which in itself is pretty usable skill. Unrelated, I'd find it even more usable in physics, where solution guesstimate developed by exposure to numerous examples computationally solved can reliably indicate the correct solution as soon as you read the exercise or a problem.
    - josephagoss 14y ago
      Thanks for replying, I got to get back into Mathematica, its so different from "normal" languages. we use Matlab at uni a lot, but its not really the same at all.
- ionfish 14y ago
  Having written the following, I now wonder whether you meant something more specific by computation than I did, so I'm not certain whether my point is really a response. Could you spell out the details of your comment a bit more, and perhaps touch on the approach which Wolfram argues for? * * * Offloading computation only works when you understand what the computations are and why we do them. That's something that must be learned, it's not knowledge that springs fully formed into our minds as soon as we step into a classroom. Carrying out computations thus gives us explicit and implicit knowledge of how the things we may eventually automate actually work. But it's also valuable because it trains us to compute in a precise and effective manner—a capability that remains useful later on. For instance, in logic it's often important to be able to carry out syntactic manipulations (e.g. into normal forms) in one's head, or even tacitly. I'm sure there are plenty of examples from other areas of mathematics where computation is important, it's just that we do it so automatically that we don't think about it. Often I've found that students have trouble following proofs that take logically and computationally innocent steps without saying what's going on. Here I don't mean things like applying AC in the background, but just simple tricks like de Morgan's laws or taking the contrapositive. They have difficulty because they haven't taken those steps often enough themselves to have internalised them.
  - Avshalom 14y ago
    I just recall the Wolfram article and I seem to think it was pretty handwavey as to what/how things get offloaded (to Mathematica specifically of course). But I will say that at least half the homework of my Calc 1-3 courses was spent well past the "understanding" stage and more into "getting fast enough to do it on an artificial, time limited test situation" and basically memorizing pages of identities that I quickly forgot because they so rarely came up in my physics courses. This was pretty much the case with almost every math class since about algebra 1 in middle school. And in particular I would like to hold up Electricity and Magnetism 2. Calculating the momentum of a magnetic field, in all but the most trivial case, takes a full sheet of paper: being rows and rows of 8 inch long equations as you carry out the tedious work of canceling terms; moving things in and out of square roots; and multiplying large polynomials together. It's all basic algebra stuff you learn in high school but it's a slog to work through and so time consuming that you actually lose track of the big picture and end up with very little better understanding at the end. As far as I know that's why things like tensor and bra-ket notation had to be invented in the first place. Without a compressed notation the ability to get a correct answer to any interesting problem became less a question of knowledge and more a question of probability of transcription/sign flip errors. not that anybody teaches sophmores tensor notation.
stiff 14y ago
I guess this is the order mathematics was taught in the authors university, in my experience with taking mathematics courses as part of a engineering degree, way too often there is no attempt at a "pre-rigorous" stage at all, as applications and intuitions are seen with contempt by the more formally-minded teachers. Vladimir Arnold's essay on this topic is a classic that I reread every few months for inspiration: http://pauli.uni-muenster.de/~munsteg/arnold.html http://pauli.uni-muenster.de/~munsteg/arnold.html Richard Courant, the classic book of which is referenced in the article, remarks in the preface of one of his other books how the logical order of presentation of mathematical theories is much different from the order that works best pedagogically. I wish more educators would understand this seemingly simple observation.
- dsirijus 14y ago
  Thanks for a great read in link.
- flebron 14y ago
  As a teacher, the reason I teach with formality before allowing students to be informal, is that formality is training wheels. Initially, the students do not know how to write a coherent proof. That is why we give them formal tools such as induction, and require them to write clearly, detailing their steps. When we do not do this, we see catastrophic lack of logical and coherent thought. Sometimes, this is the result of them not being able to _write_ their thoughts coherently, but more often, it is a results of their thoughts not _being_ coherent in the first place. Formality is used, partly, as forced coherency in writing, in an attempt to induce coherency in thought. Once the students are able to write coherent proofs, sure, let them ride fast, let them "freestyle" proofs, with the confidence that what they're writing is what they intend to write, and with the skill to communicate concisely, clearly and unambiguously with informal language. If they can do it, more power to them. Often times, however, they need a lot of time with the training wheels, before they can ride fast and not fall disastrously.
  - stiff 14y ago
    I think you are talking about a different thing than I do. I have nothing against demanding some rigour in reasoning very early on in mathematics courses, what I am concerned about is the purely formal presentation of mathematical concepts, especially those that were first discovered by studying physical or geometrical situation and which naturally arise in such contexts. For example, is the formal epsilon-delta definition of a limit the best way to begin a calculus course? Yes, this is logically one of the basic building blocks of the theory, but what value does it have pedagogically for a beginning student? It is known that learning happens to a large degree via associating new concepts with ones already known, what can such a definition be associated with? This is carried out to extremes some times, I've seen introductory calculus books replacing sentences in natural language with formal-logic apparatus like quantifiers etc. and advertising it as some great pedagogical improvement. Those are in my opinion excellent examples of courses developing intuition without sacrificing rigour: http://ocw.mit.edu/resources/res-18-006-calculus-revisited-single-variable-calculus-fall-2010/ http://ocw.mit.edu/resources/res-18-006-calculus-revisited-s... http://ocw.mit.edu/courses/mathematics/18-06-linear-algebra-spring-2010/video-lectures/ http://ocw.mit.edu/courses/mathematics/18-06-linear-algebra-... I also love the books by Richard Courant for how they manage to explain the concepts in crystal-clear English writing, present both the applications and the theory, building up the rigour gradually.
plinkplonk 14y ago
It is important to note that (in the Terry Tao's opinion) the 'more' comes only after being very thorough on the rigor and proofs, He identifies three sequential stages in learning mathematics - the pre-rigor/intuitive handwavey stage, the rigorous 'axioms and proofs' stage and the final post rigorous stage (quoting from the article) . 'in which one has grown comfortable with all the rigorous foundations of one’s chosen field, and is now ready to revisit and refine one’s pre-rigorous intuition on the subject, but this time with the intuition solidly buttressed by rigorous theory. " Many interesting thoughts on the transitions from one stage to the next. Great post.
codewright 14y ago
The same tick-tock-tick pattern occurs in programming. There was a hacker koan about this I believe. The apprentice is lax, undisciplined, and writes buggy code. The journeyman sees all that he has wrought upon the poor world with his awful code, and immediately takes to applying every precept he can to produce rigorously engineered and stable code. I leave it to the imaginations of others to perceive what might lay in the third step.
- mikevm 14y ago
  burnout?
CurtMonash 14y ago
The article & the associated comment thread have much to recommend them. But let's not glibly assume that "post-rigorous" ==> correct; much of economics can serve as a counterexample to that hypothesis. I got out of mathematics (despite getting a PhD from a top department) because I felt that if all but a few dozen mathematicians in the world were shot, the progress of mathematics would not be much impeded, and I wasn't sure I would be in that several dozen. I did think I was that good in economics and related disciplines, but in that case there was a question as to what would get listened to. And so I wound up in a non-academic career ... And before any of that, I got out of physics because it seemed boring. In the mid-1970s, that was a very fortunate decision. Going to grad school in math was somewhat about "Oops, I'm leaving my major, now what? Oh yes, I also finished a math major, and I can probably get into an excellent school and buy some time to decide what to do next ...."
CurtMonash 14y ago
Three students were asked to evaluation the hypothesis "All odd numbers > 1 are prime." The math major replied "3 is prime. 5 is prime. 7 is prime. 9 is ... NOT prime. The hypothesis is false." The chemistry major replied "3 is prime. 5 is prime. 7 is prime. 9 is ... NOT prime. 11 is prime. 13 is prime ... The hypothesis is looking good, within experimental error." The engineering major replied "3 is prime. 5 is prime. 7 is prime. 9 is prime. 11 is prime ..." That's one way to cope when you're overmatched by rigor. ;)
- tosseraccount 14y ago
  You just described Bioinformatics! sigh We got all 3.
- webwarrior 14y ago
  Didn't get the "engineering major" part. Why he thought that 9 is prime?
  - Xurinos 14y ago
    I didn't get it either, but my guess: The engineering student took a literal view. You told him to evaluate the statement; you gave him a rule. If you say all odd numbers greater than 1 are prime, then so be it.
    - dbaupp 14y ago
      I think it might just be implying that engineering students aren't very good at mathematics.
  - tel 14y ago
    Because he doesn't understand what "evaluate the hypothesis" means.
- ufo 14y ago
  The version I saw of this joke also had a version for the biology major: 3 is prime, 4 is prime, 5 is prime... :)
ths 14y ago
Good post! Generalizing the point, maybe a good description of sophistication is: using one's intuition in a natural way to explore the boundaries of one's knowledge, having previously refined that intuition by rigorous study and experiential learning. It's through an increasingly refined intuition about things within our horizon of knowledge that we're able to focus our conscious thought on the border of that horizon and expand it.
nano_o 14y ago
Interactive theorem provers can quickly get you from stage 1 to 2. If you are interested, [1] describes the experience of a professor teaching how to write correct and readable proofs about program semantics using the interactive theorem prover Isabelle/HOL. Isabelle/HOL can make you learn fast because it allows one to get instant feedback on a proof. Proving things may then become surprisingly addictive. [1] http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf
tmoertel 14y ago
If we attempt to apply Tao’s three stages -- pre-rigorous, rigorous, and post-rigorous -- to programming, something interesting happens: we find that the programming world is mostly stuck at the pre-rigorous stage because there is no widely accepted theory to guide practitioners to later stages. Yes, computer science has an accepted theoretical foundation, but computer science is not programming. In programming, the closest I’ve seen to a widely practiced theory has come out of the Haskell community. There, you can see the beginnings of a theory in which programs are constructed out of formal building blocks like monoids and functors and where appeals to category theory and monad laws guide design decisions. It’s a start.
- tel 14y ago
  This is the most clear explanation for what I enjoy about the Haskell community I've ever read. I am utterly addicted to Conor McBride's [1] work as well since he's doing the incredible thing of answering semi-practical questions with deep dependent typing theory. I also think Gabriel Gonzalez's [2] writing has the right ideas as he tries to explain the feeling and heuristic of using categorical and functorial design while also writing a very beautiful library [3]. I also really can't get away without mentioning Edward Kmett[4], Conal Elliott[5], and Edward Z. Yang[6] for writing both blog posts and code expanding on the practical advantages of theoretical methods. [1] https://personal.cis.strath.ac.uk/conor.mcbride/ https://personal.cis.strath.ac.uk/conor.mcbride/ further work available extensively at StackOverflow, user Pigworker (http://stackoverflow.com/users/828361/pigworker http://stackoverflow.com/users/828361/pigworker) and you should definitely attempt to read Kleisli Arrows of Outrageous Fortune if you're interested in some dependently typed madness. [2] http://www.haskellforall.com/ http://www.haskellforall.com/ and especially http://www.haskellforall.com/2012/09/the-functor-design-pattern.html http://www.haskellforall.com/2012/09/the-functor-design-patt... [3] http://hackage.haskell.org/package/pipes-2.5.0 http://hackage.haskell.org/package/pipes-2.5.0 [4] http://comonad.com/reader/ http://comonad.com/reader/ [5] http://conal.net/ http://conal.net/ [6] http://ezyang.com/ http://ezyang.com/
  - ky3 14y ago
    Dan Doel [1], who works with Edward Kmett, gets it too. And there's the inimitable Luke Palmer [2], whose blog contains nuggets of gold for those who care to dig through the archives. [1] http://www.reddit.com/user/doliorules http://www.reddit.com/user/doliorules [2] http://lukepalmer.wordpress.com/tag/haskell/ http://lukepalmer.wordpress.com/tag/haskell/
drallison 14y ago
Mathematics and proofs are a social process. Take a look at the classic paper by DeMillo, Lipton, and Perlis, Social Processes and Proofs of Programs and Theorems, available from several sources on the web.
Evbn 14y ago
Tao seems to be ignoring the common possibility that post-rgorous mathematical analysis makes mistakes, including proofs of (later realized to be) false statements. The tick-tock analogy of a poster here makes more sense: rigor informs intuition, decreasing likelihood of error, and intuition generates hypotheses to be verified with rigor. But mathematicians I know don't think in intuition that can be perfectly converted into rigor.
nickray 14y ago
I think Johnny Neumann said it best: "There's no sense in being precise when you don't even know what you're talking about."

119 points by 001sky 14y ago

Well, suggested solution of this problem seems kinda backwards to me. I'd much prefer something along the lines of what Stephen Wolfram suggests - offload computation to computers in the first pre-rigorous stage, which may enable building of the foundation in a more rigorous manner right from the start. Even at rigorous stage, offloading computation increases dramatically exposure to solutions and builds intuition faster by orders of magnitude.

josephagoss 14y ago
What does this mean? For example I self-teach myself math at the moment, easy stuff like calculus. I'm still trying to get my head around it all. How can I offload computation to build up intuition faster? Any tips? (I love programming if that helps)
- dsirijus 14y ago
  Particulary in starting calculus, after laying out the foundation of real numbers, exercises pretty soon start with determing limits, inflexion points, trends, and all. Sure, play with those at first by hand, but try to plot and play with those functions in, say, Mathematica. Pretty soon you'll be able to intuitively "know" how any of the functions you could be thrown at exams should look like, which in itself is pretty usable skill. Unrelated, I'd find it even more usable in physics, where solution guesstimate developed by exposure to numerous examples computationally solved can reliably indicate the correct solution as soon as you read the exercise or a problem.
  - josephagoss 14y ago
    Thanks for replying, I got to get back into Mathematica, its so different from "normal" languages. we use Matlab at uni a lot, but its not really the same at all.
ionfish 14y ago
Having written the following, I now wonder whether you meant something more specific by computation than I did, so I'm not certain whether my point is really a response. Could you spell out the details of your comment a bit more, and perhaps touch on the approach which Wolfram argues for? * * * Offloading computation only works when you understand what the computations are and why we do them. That's something that must be learned, it's not knowledge that springs fully formed into our minds as soon as we step into a classroom. Carrying out computations thus gives us explicit and implicit knowledge of how the things we may eventually automate actually work. But it's also valuable because it trains us to compute in a precise and effective manner—a capability that remains useful later on. For instance, in logic it's often important to be able to carry out syntactic manipulations (e.g. into normal forms) in one's head, or even tacitly. I'm sure there are plenty of examples from other areas of mathematics where computation is important, it's just that we do it so automatically that we don't think about it. Often I've found that students have trouble following proofs that take logically and computationally innocent steps without saying what's going on. Here I don't mean things like applying AC in the background, but just simple tricks like de Morgan's laws or taking the contrapositive. They have difficulty because they haven't taken those steps often enough themselves to have internalised them.
- Avshalom 14y ago
  I just recall the Wolfram article and I seem to think it was pretty handwavey as to what/how things get offloaded (to Mathematica specifically of course). But I will say that at least half the homework of my Calc 1-3 courses was spent well past the "understanding" stage and more into "getting fast enough to do it on an artificial, time limited test situation" and basically memorizing pages of identities that I quickly forgot because they so rarely came up in my physics courses. This was pretty much the case with almost every math class since about algebra 1 in middle school. And in particular I would like to hold up Electricity and Magnetism 2. Calculating the momentum of a magnetic field, in all but the most trivial case, takes a full sheet of paper: being rows and rows of 8 inch long equations as you carry out the tedious work of canceling terms; moving things in and out of square roots; and multiplying large polynomials together. It's all basic algebra stuff you learn in high school but it's a slog to work through and so time consuming that you actually lose track of the big picture and end up with very little better understanding at the end. As far as I know that's why things like tensor and bra-ket notation had to be invented in the first place. Without a compressed notation the ability to get a correct answer to any interesting problem became less a question of knowledge and more a question of probability of transcription/sign flip errors. not that anybody teaches sophmores tensor notation.

stiff 14y ago

I guess this is the order mathematics was taught in the authors university, in my experience with taking mathematics courses as part of a engineering degree, way too often there is no attempt at a "pre-rigorous" stage at all, as applications and intuitions are seen with contempt by the more formally-minded teachers. Vladimir Arnold's essay on this topic is a classic that I reread every few months for inspiration: http://pauli.uni-muenster.de/~munsteg/arnold.html http://pauli.uni-muenster.de/~munsteg/arnold.html Richard Courant, the classic book of which is referenced in the article, remarks in the preface of one of his other books how the logical order of presentation of mathematical theories is much different from the order that works best pedagogically. I wish more educators would understand this seemingly simple observation.

dsirijus 14y ago
Thanks for a great read in link.
flebron 14y ago
As a teacher, the reason I teach with formality before allowing students to be informal, is that formality is training wheels. Initially, the students do not know how to write a coherent proof. That is why we give them formal tools such as induction, and require them to write clearly, detailing their steps. When we do not do this, we see catastrophic lack of logical and coherent thought. Sometimes, this is the result of them not being able to _write_ their thoughts coherently, but more often, it is a results of their thoughts not _being_ coherent in the first place. Formality is used, partly, as forced coherency in writing, in an attempt to induce coherency in thought. Once the students are able to write coherent proofs, sure, let them ride fast, let them "freestyle" proofs, with the confidence that what they're writing is what they intend to write, and with the skill to communicate concisely, clearly and unambiguously with informal language. If they can do it, more power to them. Often times, however, they need a lot of time with the training wheels, before they can ride fast and not fall disastrously.
- stiff 14y ago
  I think you are talking about a different thing than I do. I have nothing against demanding some rigour in reasoning very early on in mathematics courses, what I am concerned about is the purely formal presentation of mathematical concepts, especially those that were first discovered by studying physical or geometrical situation and which naturally arise in such contexts. For example, is the formal epsilon-delta definition of a limit the best way to begin a calculus course? Yes, this is logically one of the basic building blocks of the theory, but what value does it have pedagogically for a beginning student? It is known that learning happens to a large degree via associating new concepts with ones already known, what can such a definition be associated with? This is carried out to extremes some times, I've seen introductory calculus books replacing sentences in natural language with formal-logic apparatus like quantifiers etc. and advertising it as some great pedagogical improvement. Those are in my opinion excellent examples of courses developing intuition without sacrificing rigour: http://ocw.mit.edu/resources/res-18-006-calculus-revisited-single-variable-calculus-fall-2010/ http://ocw.mit.edu/resources/res-18-006-calculus-revisited-s... http://ocw.mit.edu/courses/mathematics/18-06-linear-algebra-spring-2010/video-lectures/ http://ocw.mit.edu/courses/mathematics/18-06-linear-algebra-... I also love the books by Richard Courant for how they manage to explain the concepts in crystal-clear English writing, present both the applications and the theory, building up the rigour gradually.

plinkplonk 14y ago

It is important to note that (in the Terry Tao's opinion) the 'more' comes only after being very thorough on the rigor and proofs, He identifies three sequential stages in learning mathematics - the pre-rigor/intuitive handwavey stage, the rigorous 'axioms and proofs' stage and the final post rigorous stage (quoting from the article) . 'in which one has grown comfortable with all the rigorous foundations of one’s chosen field, and is now ready to revisit and refine one’s pre-rigorous intuition on the subject, but this time with the intuition solidly buttressed by rigorous theory. " Many interesting thoughts on the transitions from one stage to the next. Great post.

codewright 14y ago

The same tick-tock-tick pattern occurs in programming. There was a hacker koan about this I believe. The apprentice is lax, undisciplined, and writes buggy code. The journeyman sees all that he has wrought upon the poor world with his awful code, and immediately takes to applying every precept he can to produce rigorously engineered and stable code. I leave it to the imaginations of others to perceive what might lay in the third step.

mikevm 14y ago
burnout?

CurtMonash 14y ago

The article & the associated comment thread have much to recommend them. But let's not glibly assume that "post-rigorous" ==> correct; much of economics can serve as a counterexample to that hypothesis. I got out of mathematics (despite getting a PhD from a top department) because I felt that if all but a few dozen mathematicians in the world were shot, the progress of mathematics would not be much impeded, and I wasn't sure I would be in that several dozen. I did think I was that good in economics and related disciplines, but in that case there was a question as to what would get listened to. And so I wound up in a non-academic career ... And before any of that, I got out of physics because it seemed boring. In the mid-1970s, that was a very fortunate decision. Going to grad school in math was somewhat about "Oops, I'm leaving my major, now what? Oh yes, I also finished a math major, and I can probably get into an excellent school and buy some time to decide what to do next ...."

CurtMonash 14y ago

Three students were asked to evaluation the hypothesis "All odd numbers > 1 are prime." The math major replied "3 is prime. 5 is prime. 7 is prime. 9 is ... NOT prime. The hypothesis is false." The chemistry major replied "3 is prime. 5 is prime. 7 is prime. 9 is ... NOT prime. 11 is prime. 13 is prime ... The hypothesis is looking good, within experimental error." The engineering major replied "3 is prime. 5 is prime. 7 is prime. 9 is prime. 11 is prime ..." That's one way to cope when you're overmatched by rigor. ;)

tosseraccount 14y ago
You just described Bioinformatics! sigh We got all 3.
webwarrior 14y ago
Didn't get the "engineering major" part. Why he thought that 9 is prime?
- Xurinos 14y ago
  I didn't get it either, but my guess: The engineering student took a literal view. You told him to evaluate the statement; you gave him a rule. If you say all odd numbers greater than 1 are prime, then so be it.
  - dbaupp 14y ago
    I think it might just be implying that engineering students aren't very good at mathematics.
- tel 14y ago
  Because he doesn't understand what "evaluate the hypothesis" means.
ufo 14y ago
The version I saw of this joke also had a version for the biology major: 3 is prime, 4 is prime, 5 is prime... :)

ths 14y ago

Good post! Generalizing the point, maybe a good description of sophistication is: using one's intuition in a natural way to explore the boundaries of one's knowledge, having previously refined that intuition by rigorous study and experiential learning. It's through an increasingly refined intuition about things within our horizon of knowledge that we're able to focus our conscious thought on the border of that horizon and expand it.

nano_o 14y ago

Interactive theorem provers can quickly get you from stage 1 to 2. If you are interested, [1] describes the experience of a professor teaching how to write correct and readable proofs about program semantics using the interactive theorem prover Isabelle/HOL. Isabelle/HOL can make you learn fast because it allows one to get instant feedback on a proof. Proving things may then become surprisingly addictive. [1] http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf

tmoertel 14y ago

If we attempt to apply Tao’s three stages -- pre-rigorous, rigorous, and post-rigorous -- to programming, something interesting happens: we find that the programming world is mostly stuck at the pre-rigorous stage because there is no widely accepted theory to guide practitioners to later stages. Yes, computer science has an accepted theoretical foundation, but computer science is not programming. In programming, the closest I’ve seen to a widely practiced theory has come out of the Haskell community. There, you can see the beginnings of a theory in which programs are constructed out of formal building blocks like monoids and functors and where appeals to category theory and monad laws guide design decisions. It’s a start.

tel 14y ago
This is the most clear explanation for what I enjoy about the Haskell community I've ever read. I am utterly addicted to Conor McBride's [1] work as well since he's doing the incredible thing of answering semi-practical questions with deep dependent typing theory. I also think Gabriel Gonzalez's [2] writing has the right ideas as he tries to explain the feeling and heuristic of using categorical and functorial design while also writing a very beautiful library [3]. I also really can't get away without mentioning Edward Kmett[4], Conal Elliott[5], and Edward Z. Yang[6] for writing both blog posts and code expanding on the practical advantages of theoretical methods. [1] https://personal.cis.strath.ac.uk/conor.mcbride/ https://personal.cis.strath.ac.uk/conor.mcbride/ further work available extensively at StackOverflow, user Pigworker (http://stackoverflow.com/users/828361/pigworker http://stackoverflow.com/users/828361/pigworker) and you should definitely attempt to read Kleisli Arrows of Outrageous Fortune if you're interested in some dependently typed madness. [2] http://www.haskellforall.com/ http://www.haskellforall.com/ and especially http://www.haskellforall.com/2012/09/the-functor-design-pattern.html http://www.haskellforall.com/2012/09/the-functor-design-patt... [3] http://hackage.haskell.org/package/pipes-2.5.0 http://hackage.haskell.org/package/pipes-2.5.0 [4] http://comonad.com/reader/ http://comonad.com/reader/ [5] http://conal.net/ http://conal.net/ [6] http://ezyang.com/ http://ezyang.com/
- ky3 14y ago
  Dan Doel [1], who works with Edward Kmett, gets it too. And there's the inimitable Luke Palmer [2], whose blog contains nuggets of gold for those who care to dig through the archives. [1] http://www.reddit.com/user/doliorules http://www.reddit.com/user/doliorules [2] http://lukepalmer.wordpress.com/tag/haskell/ http://lukepalmer.wordpress.com/tag/haskell/

drallison 14y ago

Mathematics and proofs are a social process. Take a look at the classic paper by DeMillo, Lipton, and Perlis, Social Processes and Proofs of Programs and Theorems, available from several sources on the web.

Evbn 14y ago

Tao seems to be ignoring the common possibility that post-rgorous mathematical analysis makes mistakes, including proofs of (later realized to be) false statements. The tick-tock analogy of a poster here makes more sense: rigor informs intuition, decreasing likelihood of error, and intuition generates hypotheses to be verified with rigor. But mathematicians I know don't think in intuition that can be perfectly converted into rigor.

nickray 14y ago

I think Johnny Neumann said it best: "There's no sense in being precise when you don't even know what you're talking about."