Lean4 or Agda

Stream: new members

[Kevin Cheung]

I am getting into theorem-proving. My short-term goals is to prove theorems and write verified algorithms in discrete math. I'm looking into Agda (since I know Haskell) and Lean4. Does anyone have experience with both and could point out some major points to look out for in choosing one over the other? Any pointer is greatly appreciated.

[Martin Dvořák]

I have just started studying Agda last week, so I cannot be objective on the comparison. However, I'd say Lean is easier for developing proofs because it has an amazing tactic mode. If you need to write proof terms directly, Agda will assist you more in that regards.

[Martin Dvořák]

I've heard that Lean is more user-friendly but Agda is more computer-friendly. If your goal is to create proofs, I'd choose Lean. If your goal is to develop algorithms for automatic proving, people say Agda is more suitable for that.

[Tomaz Gomes]

If you want to learn about proofs in the most rigorous way, I suggest using Agda or Lean without tactic mode. Tactics are essential in large scale formalizations but they hide a lot of low level details in proofs.

Another point is that, from my experience, Agda's standard library is not great, there is a lot missing there. Lean's on the other hand is awesome. So if you're planning to use builtin formalized structures Lean is probably best.

[Henrik Böving]

What standard library are you talking about here? Lean without mathlib4 or std4 is certainly missing a ton as well

[Tomaz Gomes]

I believe it is still better than Agda's standard library, but yeah, I was talking about mathlib

[Kevin Cheung]

Thanks for the responses. Looks like there are good reasons to learn both. But given that I have to choose one at the moment, I'll probably go with Lean.

[Andrés Goens]

Martin Dvořák said:

I've heard that Lean is more user-friendly but Agda is more computer-friendly. If your goal is to create proofs, I'd choose Lean. If your goal is to develop algorithms for automatic proving, people say Agda is more suitable for that.

Agda or Isabelle? That description sounds more like Isabelle. I'd say if your main focus is on the math, Lean and mathlib are probably the best bet. If it's on the algorithms, probably isabelle is the easiest, if it's on the foundations, probably Agda will be the most enlightening.