The current computer-assisted proof I'm working on, trying to enumerate classes of cusped hyperbolic 3-manifolds up to a fixed maximal cusp area, makes a good ExampleAlgorithm.
ComputerAssistedProofFindingAlgorithm was used to generate ProofOfTheInsulatorLemmas, and was in turn constructed and operated using ComputerAssistedProofFindingMethod.