If the proven theorem is useful, isn't it better to be able to make use of it earlier, rather than wait for the elegant proof?
An example: If the AdS/CFT conjecture is demonstrably proven, it will elevate it from "useful computational technique" to "law of mathematics, probably how nature does it, too". I'll take any proof, as early as I can get it, in order to guide our experimental work.
In case anyone else had no idea what the parent was talking about.
Wikipedia on Quantum Physics is usually pretty atrocious, and this page is no exception. It reads like... well, nerds showing off knowledge. (There's nothing wrong with that, but unless you're already pretty steeped in things quantum, the page is jargon without meaning)
A more readable summary: http://whystringtheory.com/toolbox/ads-cft/
Indeed. Wikipedia on math in general is useless unless you already understand it.
Gauge/gravity duality under particular circumstances is certainly interesting, but unfortunately our universe is not AdS and in particular does not have a boundary on which the conformal field theory can be constrained. So being able to define string theory nonperturbatively on a Minkowski space defined on the boundary of spacetime is certainly interesting, but as far as we can tell our spacetime does not have that boundary and moreover it would be much nicer if we had a background independent formulation for a nonperturbative string theory, and the gauge/gravity duality does not really offer that. One might draw the analogy to being able to define a patch of Minkowski space around a point on a geodesic through a general curved spacetime: General Relativity explicitly promises only that a smooth coordinatization (e.g. Fermi coordinates) is possible in an infinitesimal neighbourhood around the point although in weak gravity the patch can be much bigger (and the system of coordinates more "Cartesian"). The worry (by this analogy) should be that gauge/gravity correspondence falls apart in strong gravity.
Moreover, it is an enormous stretch to argue that if a large class of bulk theories have the same symmetries as certain boundary theories (or are related in some other way) then therefore there background independent physics are recovered. Rovelli enjoys pointing out that in GR you can always select a preferred frame and map an SR theory over that and do useful computations, but that doing so gives no insights into proper Lorentz-invariant physics, so how does choosing a preferred spacetime and mapping a field theory over that providing insights into quantum gravity?
However, some string theorists (notably Verlinde recently) have been trying to get out of the AdS "box" and think about other chosen spacetimes (e.g. asymptotic de Sitter) to see if some gauge/gravity ideas are even workable for those spacetimes. Maybe they are.
> I'll take any proof, as early as I can get it, in order to guide our experimental work.
If you assume -- because General Relativity survives all observational tests and is expected to be completely correct in weak gravity -- that the string theory has to reduce to (or at least fully reproduce) classical GR in the appropriate limit then you can't expect any experiments which could distinguish between the two in the near future. But if you have a string theory that departs from GR in a testable limit, then sure, compare that with existing and future evidence.
However, string theory might testable outside the gravitational sector if the bulk-boundary correspondence covers more than that sector. Given that string theory tends to come with infinite fields, extra dimensions, supersymmetry and other theoretical objects that are not in the Standard Model, then BTSM experiments may have something to say about such string theory models.
And for your example that touches on applications of math, it approaches scientific research from the wrong perspective. If some math follows reality, (agrees with experiment and even better makes predictions that turn out to be right), there is has to be some backing to it, even if the rigor isn't fully there. Physics often runs with ideas before Math has caught up (see QM in the early days, HEP in general, etc).
So, if we back off from applications who, quite frankly, only care about whether X is true in only a few, really important number of conjectures I can think of--big questions like P=NP for example--then math itself I imagine is, well, a study for its own sake. So, what above exhaustive proofs of your run-of-the-mill conjecture? Who would want to read a paper from a math person that merely iterates through a 200TB cache of data?
People forget that science is a social phenomenon as much as it is systematic process.
I want this all so I can do this myself, so I can prove a run-of-the-mill conjecture and not waste my time with it. I want this because proving is difficult and there is more to SAT than mathematical proofs, it is used in the industry. I want this because I trust a verified proof that the airplane won't crash more than a human proof.
The availability of computer proofs does not devalue the study of mathematics.
Lots of situations where the result obtained is only thing that matters to most users.
A proof that works is the most important part. After that you can make it nice
Not the 200 terabyte one, you can't.
Once I could tell a mathematician the count, in both cases someone they proved the result in an alternative way fairly soon afterwards :)
But oppositely, I don't think anyone's demonstrated "proof mining" to be practical in any general sense. Huge proofs have been produced by brute-force, yes, BUT ONLY after the original theorem claim was altered in a clever and important fashion (for 4-color theorem, for Ramsey's theory and so-forth).
Proof used to be a distillation of a complex phenomenon, or a complex logical tangle, into a smooth thread that one could follow and agree that, yes, this is obvious when you put it this way.
Sure, at some point computers will take over the work of doing proofs, just like in a different trade hammers took over fists, or wheels took over feet, or engines took over muscles, hearts and lungs. But at that point we will have to re-examine this concept of "proof".
To be sure, myself I am very much a classicist of the old school when it comes to such matters. But this is a brave new world we are slowly but surely moving into.
Rene Descartes or Isaac Newton would throw a fit if they could see this.
For example, the graph minor theorem states that a certain order on graphs does not have an infinite antichain. Classically this may have some interesting consequences, but in reality it's not very useful. However, the proof contains some real gems, such as the notion of tree decompositions and the graph structure theorem that lead to mountains of new results all throughout graph theory and related disciplines. Tellingly, the graph minor theorem is a short and simple question while the graph structure theorem is a deeply technical statement that would not have been conjectured on its own but rather was discovered in the process of showing the graph minor theorem.
No. The goal of proving a theorem is proving it any way possible. And "inelegant" proof is just as much a proof as an "elegant" proof.
> and in the best case scenario a proof that actually forms a sensible new theoretical framework in which the theorem becomes almost trivial to prove.
What?
>What?
The idea is that, in creating the proof a mathematician invents a new way of looking at the problem. When viewed in this new way, the problem itself sometimes becomes trivial. When this happens, the the framework that was developed could be used to attack new problems that had previously been unapproachable.
When I was working on my PhD, I probably saved days or weeks of effort by writing a program to brute force an approximate solution to an equation I couldn't work out. After seeing that the solution wasn't what I wanted, I was able to spend the time I would otherwise have spent on figuring out the equation on something more useful.