Replies: 1 comment 2 replies
-
Hi Brando, I don't have a good answer since we didn't evaluate LeanHammer and |
Beta Was this translation helpful? Give feedback.
2 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
I want to try to
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:
ring?; linarith?; tauto?; library_search?; finish?; simp?; omega?, smt_tactic.interactive.smt?,
Any other suggestions?
Reference:
DSP attempts to produces proves via this flow:
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
Beta Was this translation helpful? Give feedback.
All reactions