This syntax looks much more friendly than Lean! Could be really great. Complaint about their Live Code environment. I tried running the code on their front-page in the live environment and it gave me `input.pf:2.9-2.12: undefined variable: Nat` which immediately makes me bounce off.

Which kind of software license uses Deduce? The web says it's open source, but I couldn't find the license in the github repository.

I've really liked educational proof checkers going back to the tutch proof checker.

One thing I didn't see here is the ability to header-like file which declares the type of proofs... the syntax of deduce looks very nice though.

Because of the Curry Howard Correspondence, do they have a compiler to compile proofs written in this language to machine code, with optional inline assembly support?

undefined

> for education

Is there any standard curriculum course for... this? (Actually, I don't know if it's a good idea to use this for learning, instead of learning Lean, because I imagine that 95% of learning Lean would be Learning its library anyway. But I never actually tried to use these kind of tools for anything.)

> A proof checker meant for education

What makes it for education? Why can't it be used as a general purpose proof checker?

I’m excited to take a look. I like and usually recommend Daniel Velleman’s “Proof Designer” but I’ve heard from some it’s too obtuse for beginners.