# Zulip Chat Archive

## Stream: new members

### Topic: Lean4 or Agda

#### Kevin Cheung (May 09 2023 at 11:44):

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 (May 09 2023 at 12:39):

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 (May 09 2023 at 12:42):

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 (May 09 2023 at 15:14):

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 (May 09 2023 at 15:16):

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

#### Tomaz Gomes (May 09 2023 at 15:17):

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

#### Kevin Cheung (May 10 2023 at 10:38):

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 (May 11 2023 at 09:20):

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.

Last updated: Dec 20 2023 at 11:08 UTC