Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. First, empirically it seems that a number of undergraduate students pick up proof assistants without formal training in those subjects. Second, a good textbook, video series, course, or tutorial for your proof assistant should cover what you need of those topics.

Certainly after you learn a proof assistant you will be better acquainted with logic (especially that used by the proof assistant), with type theory (if it uses HOL of DTT), and with functional programming (again, if it is type theory based or is implemented directly in OCaml via the LCF approach). Also, you will probably develop a natural curiosity about those subjects, as well as category theory, and this is great! (I've suggested actually that one of the best way to learn type theory is to learn a proof assistant.) But they are not a prerequisite IMHO.

In particular I'm worried about sending folks to take full courses in logic (model theory, the completeness theorems), functional programming (building a Scheme interpreter inside Scheme), type theory (strong normalization), and category theory (adjunct functors) before at least trying their hand at a proof assistant.

If you are interested in Lean (and there are lots of great alternatives!), the natural number game is a great place to start. After that, see the recommended next steps here. But notice none of the recommendations on that page say to learn other things first (although one of the possible recommendations is an undergraduate logic course which is taught alongside Lean).

My personal story: I did happen to know logic and some BASIC programming before starting on proof assistants. But I learned functional programming and type theory through the HOL Light proof assistant tutorial, and dependent type theory though the Lean tutorial. I even learned about type classes and monads through Lean.

Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. First, empirically it seems that a number of undergraduate students pick up proof assistants without formal training in those subjects. Second, a good textbook, video series, course, or tutorial for your proof assistant should cover what you need of those topics.

Certainly after you learn a proof assistant you will be better acquainted with logic (especially that used by the proof assistant), with type theory (if it uses HOL of DTT), and with functional programming (again, if it is type theory based or is implemented directly in OCaml via the LCF approach). Also, you will probably develop a natural curiosity about those subjects, as well as category theory, and this is great! (I've suggested actually that one of the best way to learn type theory is to learn a proof assistant.) But they are not a prerequisite IMHO.

In particular I'm worried about sending folks to take full courses in logic (model theory, the completeness theorems), functional programming (building a Scheme interpreter inside Scheme), type theory (strong normalization), and category theory (adjoint functors) before at least trying their hand at a proof assistant.

If you are interested in Lean (and there are lots of great alternatives!), the natural number game is a great place to start. After that, see the recommended next steps here. But notice none of the recommendations on that page say to learn other things first (although one of the possible recommendations is an undergraduate logic course which is taught alongside Lean).

My personal story: I did happen to know logic and some BASIC programming before starting on proof assistants. But I learned functional programming and type theory through the HOL Light proof assistant tutorial, and dependent type theory though the Lean tutorial. I even learned about type classes and monads through Lean.

Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. First, empirically it seems that a number of undergraduate students pick up proof assistants without formal training in those subjects. Second, a good textbook, video series, course, or tutorial should cover what you need of those topics.

Certainly after you learn a proof assistant you will be better acquainted with logic (especially that used by the proof assistant), with type theory (if it uses HOL of DTT), and with functional programming (again, if it is type theory based or is implemented directly in OCaml via the LCF approach). Also, you will probably develop a natural curiosity about those subjects, as well as category theory, and this is great! (I've suggested actually that one of the best way to learn type theory is to learn a proof assistant.) But they are not a prerequisite IMHO.

In particular I'm worried about sending folks to take full courses in logic (model theory, the completeness theorems), functional programming (building a Scheme interpreter inside Scheme), type theory (strong normalization), and category theory (adjunct functors) before at least trying their hand at a proof assistant.

If you are interested in Lean (and there are lots of great alternatives!), the natural number game is a great place to start. After that, see the recommended next steps here. But notice none of the recommendations on that page say to learn other things first (although one of the possible recommendations is an undergraduate logic course which is taught alongside Lean).

My personal story: I did happen to know logic and some BASIC programming before starting on proof assistants. But I learned functional programming and type theory through the HOL Light proof assistant tutorial, and dependent type theory though the Lean tutorial. I even learned about type classes and monads through Lean.

Unlike the other answers, I'm fairly convinced you do not need to learn anything (category theory, type theory, functional programming, or even logic) before hand. I have two basic reasons for this. First, empirically it seems that a number of undergraduate students pick up proof assistants without formal training in those subjects. Second, a good textbook, video series, course, or tutorial for your proof assistant should cover what you need of those topics.

Certainly after you learn a proof assistant you will be better acquainted with logic (especially that used by the proof assistant), with type theory (if it uses HOL of DTT), and with functional programming (again, if it is type theory based or is implemented directly in OCaml via the LCF approach). Also, you will probably develop a natural curiosity about those subjects, as well as category theory, and this is great! (I've suggested actually that one of the best way to learn type theory is to learn a proof assistant.) But they are not a prerequisite IMHO.

In particular I'm worried about sending folks to take full courses in logic (model theory, the completeness theorems), functional programming (building a Scheme interpreter inside Scheme), type theory (strong normalization), and category theory (adjunct functors) before at least trying their hand at a proof assistant.

If you are interested in Lean (and there are lots of great alternatives!), the natural number game is a great place to start. After that, see the recommended next steps here. But notice none of the recommendations on that page say to learn other things first (although one of the possible recommendations is an undergraduate logic course which is taught alongside Lean).

My personal story: I did happen to know logic and some BASIC programming before starting on proof assistants. But I learned functional programming and type theory through the HOL Light proof assistant tutorial, and dependent type theory though the Lean tutorial. I even learned about type classes and monads through Lean.