4 ms·
Toward an exploratory medium for mathematics
- munin 11y agothis looks really cool! I think it's weird that the author dings matlab and mathematica for being unable to do counterfactual reasoning. matlab and mathematica are computational tools, they don't do "reasoning" the way that say coq or other proof assistants do. and proof assistants can do counterfactual reasoning, so what's the deal? beyond that it would take a lot of work to encode these graphical diagrams into coq I guess...
- conceit 11y agoMatlab has a package for symbolic computation. It sounds to me like the author would want some of that, although I didn't quite follow through the whole argument.
- seanmcdirmid 11y agoI think he is arguing that they don't aid in counterfactual reasoning. They provide no facilities to help you yourself discover contradictions. This isn't about automating proofs, just helping you think through the problem.
- seanmcdirmid 11y agoBah, I totally wrote this wrong. What I really meant to say was that it is not an automated system for doing a proof. It is a tool that helps you do reasoning and thinking. Augmenting human intelligence rather than replacing it.
- munin 11y agoI think the proponents of proof assistants would say that the proof assistant is also there to help you do reasoning and thinking.
- seanmcdirmid 11y agoI think they would! But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself. This kind of tool aides in reasoning via a concrete example that can be tweaked in real time to see different sides of the problem.
- catnaroek 11y ago> But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself. This isn't really true. Nowadays, Coq can automate much of the process of coming up with a full proof - which is exactly what requires “abstract thinking”. (Of course, you still need to identify “strategic lemmas”, but even these lemmas can often be proven mostly automatically.) The downside is that machine-generated proofs are often gibberish from the point of view of human intelligibility, but that's okay if you're only interested in the truth of what is being proven. > This kind of tool aides in reasoning via a concrete example Actually, going from a concrete example to a more general abstract concept requires you to do the thinking yourself. At least if you want the result of the generalization process to be valid.
- seanmcdirmid 11y agoSurely Coq can fill in the wholes, but it is completely abstract; it doesn't use concrete examples to do this, and anyways, you really have to understand what it is doing. The point of this kind of work is that it augments your thinking by allowing you to visualize and manipulate your concrete example. Before, you'd just have pen and paper for that, with no assistance from the computer at all. The whole formal kick really comes after you have enough intuition about the problem, this comes before that and aides in the intuition accumulation process.
- catnaroek 11y agoWhy do I need an intuition when I can just manipulate formulas?
- mockery 11y agoAre these videos of an functioning piece of software, or mockups? There are a lot of interactions that are glossed over, and it's not obvious to me how this software would function. I'm also skeptical about the characterization of an exploration of the properties of a single 2D matrix as "real mathematical work."
- transfire 11y agoCan anyone summarize?
- fnovd 11y agoMany useful mathematical proofs can be derived based on proving the impossibility of a contradictory assumption. I can try to disprove the triangle angle sum theorem (that the sum of the three angles in any triangle is 180) by attempting to draw a triangle that contradicts that assumption. I may begin by drawing two 90 degree angles. In doing so, I instead demonstrate that the 2 unconnected lines will never intersect in 2D space, and thus the figure cannot be triangle. This is a useful step along the way of formally proving that the sum of angles in any triangle is 180. My attempt at drawing an impossible figure can help visualize exactly why such a figure is impossible. This suspension of constraint enforcement is easy on pen and paper. I can attempt to draw whatever I wish. However, there is no easy way to experiment in this way with modern mathematical software. How do you formalize a proof by contradiction in software that has these constraints pre-programmed?
- catnaroek 11y agoThat the internal angles of a triangle on the Euclidean plane add up to pi, can be derived directly, without resorting to proof by contradiction. (Hint: Draw a parallel line to one of the edges, which passes through the vertex not contained in that edge.) Also, a proof by contradiction of an equality is unsatisfactory in constructive mathematics, because, in general, you can't go from “that A and B are not equal implies a contradiction” to “A and B are equal”. (This would require equality to be decidable.)
- deleted 11y ago[deleted]
- conceit 11y agoThe way the term medium is used here really bothers me. For one, because I was taught that a medium is a oneway communication channel. Further more, because the plural media has an idiomatic meaning in English, that is the publishing industry. I find it Ironic that it's in the name of the site, even, although I should judge the content by its merit. I don't because it's tl;dr and I got lost around the explanation of SVD (a link to wikipedia would be enough).
- theoh 11y agoI don't know who erroneously taught you that a medium is always a one-way channel. In the creative sense, it's a cliche to talk about exploring something "through the medium of dance" or to refer to painting or drawing as a medium. The blackboard is a traditional mathematical medium.
- endergen 11y agoIt's common to call video games a medium. So that's a good example if it helps.