Hacker News Reader

I think I mistyped. Pardon the pun!

I meant that Lean, I think, could be implemented in Lean.

Do you also work with Lean?

That's an interesting question: can Lean be implemented in Lean's dependent type theory.

I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.

That sounds like it could be a lot of fun! Good luck. :)

Reply on news.ycombinator.com