Yes, it's already possible[1] with Coq. There are two strategies for that - lowering the CIC (Calculus of Inductive Constructions) to SMT[2] and employ SMT solv

Yes, it's already possible[1] with Coq. There are two strategies for that - lowering the CIC (Calculus of Inductive Constructions) to SMT[2] and employ SMT solvers like Z3, and employing Deep Learning[3][4]. For the Lean part, compared to Coq - there is an interesting discussion[5] why Lean might be not as good as they claim. [1] https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303 https://coq.discourse.group/t/machine-learning-and-hammers-f... [2] https://github.com/lukaszcz/coqhammer https://github.com/lukaszcz/coqhammer [3] https://arxiv.org/abs/1907.07794 https://arxiv.org/abs/1907.07794 [4] https://github.com/UCSD-PL/proverbot9001 https://github.com/UCSD-PL/proverbot9001 [5] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871