ComputerAssistedProof is a procedure by which one or more people work with one or more computers to arrive at a proof.
It is useful to think of ComputerAssistedProof as a form of CollaborativeMathematics in which some of the participants are computers. In this context, the relevant properties of the computers are:
- Computers are great at exactly following precise rules.
- Computers are good at performing repetitive tasks.
- Computers have no common sense.
The trick in collaborating with a computer is to find ways to assign it well-understood, repetitive, easy-to-specify tasks, while leaving the parts that require common sense to the humans. In particular, until people understand how to do something well enough that it's routine, it's often futile to try to program a computer to do it.
Examples
ComputerAssistedProofFindingMethod describes the process by which
NathanielThurston collaborated with
ComputerAssistedProofFindingAlgorithm, RobertMeyerhoff
?, and DavidGabai
? to find a
ProofOfTheInsulatorLemmas.