[agentultra]

I think I mistyped. Pardon the pun!

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

Do you also work with Lean?

[Cladode]

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.

[agentultra]

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