Hacker News Reader

I'm planning to learn Agda for this very reason. Have you looked at Agda or other proof checkers?

What about Lean made you decide to use it for this project? The Tactics system?

Yes I've played with Agda before Lean. I found documentation for Agda to be sparse, maybe it's improved since then. Also, it was kind of a pain to get it setup. Lean was extremely easy to get running, works beautifully with VSCode, has great documentation and a helpful community. It's a "sexy" language and set of tooling compared to Agda and Coq (and I'm of the opinion aesthetics matter). It also feels more well-supported with the backing of Microsoft Research behind it.

Reply on news.ycombinator.com