the ultimate question

Stream: general

[Huỳnh Trần Khanh]

I want to make a toy theorem prover based on the Calculus of Inductive Constructions, how can I get started?

[Huỳnh Trần Khanh]

As a programmer, I don't want to treat anything as a black box. It feels rather unsatisfying.

[Mario Carneiro]

You might find the discussion at https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/stlc.20terms helpful for getting started writing a typechecker for lambda calculus. Patrick Thomas is working in haskell but you can just as well do that in lean 3 or lean 4, or any other language for that matter.