2025
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
NeurIPS 2025poster
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 of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically simi…