ComputerAssistedProofFindingMethod

The proof-finding technique described here is suitable for problems which already have an IncompleteProof, in the form of an ideas for:

• dividing the problem whose solution is desired into a large collection of sub-problems
• a formal way of representing proofs to the sub-problems
• a mechanical way of checking proofs to the sub-problems

It is particularly appropriate for situations where the time required seems impractical at first.

The general method is to use the IncompleteProofTechnique in a special kind of CollaborativeMathematics in which one of the participants in the collaboration is a computer. In the collaboration, the computer will play the role of an "idiot savant" -- it can perform routine work extremely quickly, but can't be expected to have any common sense. The challenge in this process is to divide the labor of finding the proof so that the computer performs the routine tasks that would be to tedious for the people, while the humans perform the tasks that are beyond the limited capabilities of the algorithms the people will be programming.

Optimizing the process

• Think of everything you do in the context of the IncompleteProofTechnique
• BeLazy?. Don't do anything now that you could put off until after you're more certain that it's necessary
• AdaptTheProblem. Try to find a way to restate the problem so that it seems easier to solve.
• OptimizeTheAlgorithm?. Try and find a better algorithmic approach to the problem.
• OptimizeBottlenecks?. Find out where your code is actually spending time, and find ways to speed up those parts.
• implement tasks which become routine in code. conversely, don't bother implementing rare cases until you've solved at least a handful of them by hand.
• segregate verification of the proof from finding of the proof. The reason is that you can (and should) take liberties in the proof-finding process, while you will need to be extremely careful with the proof-checking process.
• if the ComputerAssistedProof process is running smoothly without your intervention, consider working on something else while it runs, only occasionally checking back. Your time isn't needed right now, so don't waste it.

When things seem difficult or impossible

• use MentalTechniques when things are difficult.
• DiagramImpasses?
• tackle intermediate problems (e.g., getting to the first quasi-relator in the MOM search)
• consider alternate approaches for part of the work (e.g., the corona method, or the current MOM attempt to use the quasi-relator outside the algorithm)

Designing a proof-finding algorithm

• make it parallel:
  • in the traditional sense of being able to run on different computers
  • so that it doesn't stall if it runs into an unsurmountable obstacle.
• Consider using the techniques described in ComputerAssistedProofFindingAlgorithm.
• LessIsBetter?. Don't seek a perfect algorithm; settle for one that you can't mentally prove to be inadequate for the task at hand.
• StriveForSimplicity?. Your mind has a limited capacity for intuitively understanding complexity. Keep your algorithm within this limit, refactoring and rewriting from scratch as needed.
• FailGracefully?. Your algorithm will likely fail. Design it to fail in a graceful way, and to alert you to the failure.
• ExposeParameters?. If there's a parameter to the algorithm that might change, expose it so that you can easily change by invoking the algorithm in a different way.

Writing Code

• WriteToolsNotMonoliths?.
• ChooseLanguagesCarefully?.
• AgileProgramming?.
• note defects now, fix them when opportunity strikes later.
• DiscardStaleCode?.
• UseMeaningfulNames?. Good names give your mind handles to grasp.
• WriteCodeInYourMind?. Design and implement your algorithms in your head first. Don't start writing code for a task until you think you see how to finish it.
• DontDoUnitTests?. Your success depends on your ability to debug emerging patterns about the behavior of your algorithm; conventional debugging is a warm-up exercise.
• CommentInfrequently?. Comments get in the way of your intuitive grasp of the code itself. Exceptions:
  • names (such as members of structures), for which the comment is an extension of the good name you've chosen.
  • hacks, or places where the least-expensive decision is to code for convenience, not for elegance.
• If everything is working correctly, you will find yourself DebuggingAsYouWrite?, finding and fixing errors in the mental version of your algorithm as you give them concrete form.

Observing the progress of a partially-found proof

• UseAProfilingTool? to figure out what parts are slow in practice.
• InventInterestingSummaryStatistics?
• ExamineRepresentativeExamples?. Manually go through what's happening as the code tries to solve a few representative cases, and see if you can come up with a better solution for some of them.
• VisualizeTheAlgorithm?. Find ways to visualize what's happening, either for individual cases or in summary.
• InvestigateSurprisingBehaviour?. If you observe something you don't understand, try to find out why it happened.

Examples

FindingKillerWords outlines the story of how ComputerAssistedProofFindingMethod was used to find ProofOfTheInsulatorLemmas. http://thething.is/wiki/MOM.pl?NewSearchLog is a progress log of the use of a related algorithm which is in searching for a related proof.