Introduction

I'm working on a new introduction, written along more conventional mathematical lines. First draft in NewIntroduction. -- NathanielThurston

The purpose of this publication is to prove:

PropositionIntroduction: others will be able to extend or expand on NathanielThurston's work in [Homotopy Hyperbolic 3-Manifolds are Hyperbolic].

Discussion:

This work used ComputerAssistedProof techniques to arrive at a ProofOfTheInsulatorLemmas. The traditional route to enabling extensions or expansions was followed -- in 1994, RobertMeyerhoff?, DavidGabai?, and NathanielThurston circulated a preprint of a paper which included these proofs, and after an extensive peer review process it was eventually published in the Annals of Mathematics in 2003. Along with the publication of the preprint, the source code used to find the proof was made available to interested parties. In the intervening years, others have used the result. However, despite several attempts to extend or apply those ComputerAssistedProof techniques to other problems, to our knowledge no such attempts have been successful.

The published paper included a reference to "Finding killerwords" (in preparation) -- a paper that was to explain the process by which the computer algorithm found "words" in a finitely-presented group which could be used to "kill" (eliminate from consideration by a simple proof process) one of the cases of which the overall proof was comprised. Nathaniel has until now resisted writing this paper, out of a sense that he wouldn't have been able to explain the process well enough for it to be reproduced. In particular, for many years it seemed that the ComputerAssistedProofFindingAlgorithms he used were trivial adaptations of well-known algorithms in computer science; that the processes he used was "to have no process"; and most critically that the success of the algorithm depended on his active participation, without which the algorithm would have only be able to solve far easier problems than finding ProofOfTheInsulatorLemmas.

This last criteria, that of requiring human guidance deserves further explanation. During the course of finding the ProofOfTheInsulatorLemmas, there were perhaps a dozen occasions in which the algorithm reached an obstacle that would have effectively prevented it from finishing its task. Each time such an obstacle was approached, NathanielThurston found evidence of the obstacle; made an inspired guess as to the cause of the obstacle and how it might be bypassed; and controlled or modified the algorithm to "drive" the algorithm around the obstacle. The key in these cases was his ability to make "inspired guesses", for this required:

• Proficiency with the art of AbductiveReasoning, which could be stated as the general art of making inspired guesses.
• Proficiency with the art of debugging (without which deducing cause from effect in the context of programs would be impossible).
• Proficiency with the art of finding proofs (without which the overall structure of the algorithm would be difficult to understand).
• A background in algorithms (without which a detailed understanding of ComputerAssistedProofFindingAlgorithm - and in particular, with its potential variants - would have been difficult).
• A basic background in GeometricTopology, and collaboration with others who had mastered that subject.

The conclusion was that there were few people who had all of the required proficiencies, and that anyone who had them all would have little use for the paper NathanielThurston felt capable of writing until recently.

It's useful to view the "flash of insight leading to an inspired guess" as another kind of proof-finding. In this case, the proposition which is "proven" is "there is a comprehensible reason why the currently-formulated process of proof-finding isn't working sufficiently well", and the proof is found by example, through the discovery and testing of that reason. In other words, in order to adequately present the process of proof-finding in its original narrow meaning of finding a WordOfSymbols in an artificial formal language, it seems necessary to also address the question of proof-finding in general: finding a WordOfSymbols in the natural English language of words that convinces people.

Insights contributing to the proposed solution to the problem of finding and explaining a sufficiently-powerful replacement for the "flash of insight" came in 2009 in the following order:

• CollaborativeMathematics suggested that a group of people can combine to form a "super-mathematician" which can make effective use of the union of the participants' knowledge and abilities.
• AbductiveReasoning provided a name for the art of accurately leaping to conclusions.
• InverseLogic provided the ability to argue with confidence from the direction of what is required when appropriate.
• IncompleteProof provided a way to explain the theory of finding proofs.
• PatternLanguage provided a way to explain the overall structure of this publication.
• MentalTechniques provide hope that the art of AbductiveReasoning can be explained and possibly taught.
• MissionCreep provides a way to divide what belongs in this document from what doesn't.

IncompleteProof:

It seems likely that a person, or a group of people, could use some or all of the techniques described in the PatternLanguage contained in this publication in a way that could be fairly said to extend or expand on NathanielThurston's work. In particular, it seems likely that they could use ComputerAssistedProofFindingMethod to find other ComputerAssistedProofs.

---

Eventually, a table of contents and an index of terms are planned. The reader may also find it useful to:

• http://thething.is/FindingKillerWords.pl?action=index will provide a list of all terms in the PatternLanguage
• click on a page title, which will provide a list of all pages in which the page is referenced.
• visit TheNextSteps for an outline of what needs to be done next in order to transform this draft into a completed thesis.
• examine BrainStorming to see ideas which seem related but which haven't yet been connected with the rest.

References

• The Tricki:/ is another library of techniques found to be useful in mathematical problem-solving.
• George Pólya, [How to Solve It], 1945.
• [Jacques Hadamard], The Mathematician's Mind, 1963.
• Philip J. Davis and Reuben Hersh, [The Mathematical Experience], 1981.
• William P. Thurston, [On Proof proof and progress in mathematics], 1994.