lean-smt
is a plugin for the Lean theorem prover that integrates it with the cvc5 SMT solver.
With it, the user can discharge proof obligations to be solved by the ATP. In my
master thesis I studied
different approaches for reconstructing proofs coming from cvc5 into Lean and integrated the most promising
one to lean-smt. I still contribute to the project regularly. Here are some representative PRs: