proof search tactics

Stream: new members

[Andrea Vezzosi]

Hi, what are examples of proof search tactics beyond tidy ?

Something that can handle a variety of goals, at least for a specific domain/project.

[Johan Commelin]

In Lean 4, there is aesop.

[Johan Commelin]

For specific domains, things like ring and linarith exist.

[Andrea Vezzosi]

Thanks! I think I'll need some combination of linarith with first order logic. Aesop looks interesting but I might be stuck with Lean 3.