[cap-talk] (Was: Web calculus) theory and practice (flame?)

David Hopwood david.nospam.hopwood at blueyonder.co.uk
Mon Feb 27 20:12:30 EST 2006

Jed at Webstart wrote:
> David,
> Whew!  I can see I touched a sensitive point on this contrast between
> theory and practice.  While I see you disagreeing with many of my
> words, I don't pick up any essential disagreement about our understandings
> of theory and practice.

Perhaps I am a bit touchy on this subject, yes :-) We don't seem to disagree
on anything fundamental.

>> > For example in
>> > theory one can use Quantum Mechanics to calculate the orbit[al]s
>> > of electrons for any atoms.  In practice it's only possible to
>> calculate
>> > the orbits for the hydrogen atom and to make approximations for the
>> > helium atom (at least last I checked).
>> Let's assume this is correct (my knowledge of quantum mechanics is
>> minimal)
>> and say that you're designing some exotic power reactor in which it is
>> necessary to have a comprehensive understanding of the orbitals of
>> electrons
>> in the elements used as fuel. The three kinds of response described above
>> apply here; you can
>>  - restrict the design of the reactor (e.g. by using only hydrogen) so
>>    that your existing theory of electron orbitals is sufficient,
>>  - extend the theory so that it can calculate the orbitals for the
>>    elements your reactor will use, or
>>  - muddle along regardless.
> If by "muddle along regardless" you mean to include using approximations
> for the orbitals of other atoms, then I think you disparage that approach
> too strongly.

I didn't mean that approximations are always insufficient. They may or may
not be depending on the context (and degree of risk).

>> I do not believe that there is any real phenomenon that cannot in
>> principle be explained by an appropriate theory. That's a stronger
>> position than needed to support my general argument in this post, but
>> it may help to see where I'm coming from.
> That is a pretty strong position.  For me it has no significance.  Whether
> or not all "real phenomenon" (I would focus on observations) can be
> explained
> by an appropriate theory doesn't really matter to me.  I expect that at
> least during
> my lifetime there will continue to be observations that are not
> successfully
> explained by the best theories.  We just have to keep working on better
> theories
> and refining our applications of them.  Even if at some time everything is
> explained and the world becomes a boring place for scientists I don't see
> how a belief like you state above will have helped with the explanations.
> In the above when you say "in principle" you again seem to be using
> a phrase that distinguishes between the theoretical and the practical
> or the academic and the applied.

No, simply that, as you say, "at least during my lifetime there will continue
to be observations that are not successfully explained by the best theories."
And in anyone's lifetime, in fact.

>> I hope and expect that at some point in the near future (< 10 years),
>> progress in computer-assisted reasoning will make it feasible to produce
>> strictly formal proofs (that can be checked by very simple theorem
>> checkers) with a similar investment of effort as is currently the case
>> for semi-formal reasoning.
> I find the above delightful.  I've long argued that it's important to place
> mathematics on a more formal footing by using computers to check proofs.
> Many people don't seem to appreciate that while it's indeed impossible to
> develop an algorithm that will prove all possible "true" statements in
> adequately rich theories (Gödel, etc.), it's still straight forward (if not
> necessarily simple) to
> have computer algorithms check the correctness of any proof.  By having
> computers do such checking it seems to me that we could avoid some
> problems like the questions about whether quite complex proofs (e.g.
> for the Four Color Problem, or Fermat's so-called 'last theorem' or others)
> are correct.

Actually, precisely this process has recently (2005) been applied by Georges
Gonthier and Benjamin Werner to one of the proofs of the four colour theorem,
using the Coq theorem prover:


  Devlin, K. "Devlin's Angle: Last Doubts Removed About the Proof of the Four
  Color Theorem." January 2005. <http://www.maa.org/devlin/devlin_01_05.html>

  Knight, W. "Computer Generates Verifiable Mathematics Proof."
  New Scientist Breaking News. April 19, 2005.

  Georges Gonthier's home page at Microsoft Research, from which the Coq proof
  can be downloaded: <http://research.microsoft.com/~gonthier/>

This still doesn't mean that the proof is at all easy to understand -- it's
2.6 Mbytes (!) of rather dense code. The important points are:

 - the process is already feasible, even for extremely complicated proofs.
   That's why I'm estimating less than 10 years for it to become more accessible
   to mathematicians who are not experts in computer-based theorem proving.

 - unlike the 1976 Appel and Haken computer-verified proof of the 4-colour
   theorem, which relied on software specific to that proof, to accept this
   version you only need to trust Coq and its libraries (which you can run
   using diverse compilers and hardware).

This is the same Georges Gonthier who co-developed the join calculus, incidentally.

> The above is quite different from the effort of, say, the Principia
> Mathematica (which seems to have had relatively little - dare I say it -
> 'practical' value) where the emphasis was on completing mathematics.

Principia Mathematica had some significant, if indirect, influence on later
developments -- for example, the Ramified Theory of Types that it introduced
was one of the first type theories.

David Hopwood <david.nospam.hopwood at blueyonder.co.uk>

More information about the cap-talk mailing list