Which is the most powerful automation tactic available in Lean, LeanDojo or ReProver

[brando90]

I want to try to

Reproduce Draft Sketch Prove (DSP) in Lean

The main thing I want to know is which is the strongest automation/prover to close a proof obligation in Lean or Lean Dojo. Any suggestions?

My Ideas:

1. use ReProver
2. use LeanHammer (https://github.com/phlippe/Lean_hammer)
3. use the most powerful tactic available in lean e.g., ring?; linarith?; tauto?; library_search?; finish?; simp?; omega?, smt_tactic.interactive.smt?,

Any other suggestions?

---

Reference:

DSP attempts to produces proves via this flow:

informal statement (usually human given) -> informal proof (human/given or produced by AF from informal statement) -> produce formal proof sketch from informal proof (also produce autoformalization of target statement) -> close remaining holes in proof via automation (e.g., seldgehammer)

other refs: https://chat.openai.com/c/b988a232-0e5d-4ecd-89a5-08ee958fb60f https://claude.ai/chat/c9d65127-7798-4123-bf5a-06faf5743052

other ref: phlippe/Lean_hammer#2

[yangky11]

Hi Brando,

I don't have a good answer since we didn't evaluate LeanHammer and ring?; linarith?; tauto?; library_search?; finish?; simp?; omega?, smt_tactic.interactive.smt?. From results in our paper, we only know ReProver is better than tidy (under our specific experimental setup).

[brando90]

So the main questions is conceptual.

1. Do you recommend to run a prover using python on the fly like in LeanDojo(formal_stmt, Prover) or LeanDojo(formal_stmt) to verify that that theorem is provable

or

2. To generate the strings beforehand offline and then use some other way to check the statements generated by the LLM?

or

3. Run things directly in Lean

Last comment, I am more than happy ot use tidy and ReProver. :)

[yangky11]

All 3 options are possible, and it ultimately comes down to which one is easier to implement. My guess is that 2 would make more sense.