Installing automated proof tools?

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

There are now a number of experimental add-ons to Lean (e.g.,Duper, Lean Copilot, Sagredo... any others?), that could in principle be used to close simple goals that show up in the PFR project. Would there be interest (particularly among potential code contributors) for installing one or more of these add-ons to PFR as an experiment? Given that the primary aims of this project have already been successfully completed, and the current pace of contributions has moderated from its peak, I think we can afford the risk that one of these tools may cause some temporary build issues (I assume that in the very worst case we can roll back to a version of the repository without the tool).

[Paul Lezeau]

I'd be open to trying out new tools!

[Rémy Degenne]

There is also llmstep, which is similar to Lean Copilot.

[Terence Tao]

Ideally I would want to experiment with a tool where a participant who doesn't want to use the tool sees no change in his or her workflow (and no big CPU spikes when trying to compile the code), but that participants who do want to try out the tool can do so.

[Jason Rute]

As someone who works on similar (but different) tools, I'd love all your thoughts on the current tools both in terms of usability and power.

[Jason Rute]

I think except for duper, the others are just suggest and proof search tools that (as long as you don't leave them in your code) won't effect other users. After running them, you replace the call with the suggested tactic or proof. @Josh Clune @Kaiyu Yang @Sean Welleck @Scott Morrison could say more for sure.

[Terence Tao]

Duper also has a similar suggestion mode duper? as well, right?

[Terence Tao]

If the tool is invisible to all other users then I don't really see any downside to adding such a tool (other than the one-time cost of actually installing the tool and propagating it to all the local copies of the repo - I assume it isn't an absolutely massive set of files).

[Terence Tao]

I also assume that these tools can be maintained independently of mathlib, so that updating one won't break the other.

[Adam Topaz]

The only potential issue I see is that duper depends on lean_auto which depends on std, which is also a dependency of mathlib. So there may be a clash if two different versions of std are used.

[Mario Carneiro]

I believe lake is not clever enough to do version resolution, so it won't actually cause a failure necessarily. As long as lean_auto and duper are not using unstable APIs I would not expect them to break very often due to std changes.

[Mario Carneiro]

And if they do, the fix would be to either PR / merge updates to lean_auto / duper or have a branch in a fork and depend on that instead

[Mario Carneiro]

If/when duper becomes a dependency of mathlib, managing this will become the responsibility of the maintainer team, we will make sure that they are always on compatible versions