automatic proving in lean

Stream: new members

[stark]

I wonder whether there is automatic theory proving implementation in lean, like analytica in mathematica or vampire prover

[Alex J. Best]

There are several projects in this direction, with slightly different but related goals, like https://github.com/leanprover-community/lean-auto and https://github.com/leanprover-community/duper