3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

Sean Lamont, Christian Walder, Amir Dezfouli +2

A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number o…