Timeline for What mathematical topics should I learn first before I start using proof assistants?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 15, 2022 at 2:35 | vote | accept | Rafael Coelho | ||
| Feb 14, 2022 at 22:27 | vote | accept | Rafael Coelho | ||
| Feb 15, 2022 at 2:34 | |||||
| Feb 14, 2022 at 22:15 | comment | added | Rafael Coelho | @AndrejBauer There's no particular reason. Maybe just because lots of people I know of that use proof assistants are well versed in category theory. | |
| Feb 14, 2022 at 20:57 | comment | added | Andrej Bauer | I see. Monads as a programming technique are indeed based on the category-theoretic monads, but one does not really need the latter to learn the former, as witnessed by scores of competent Haskell programmers who know almost no category theory. | |
| Feb 14, 2022 at 20:53 | comment | added | Bolton Bailey | For example, if you want to program a tactic in Lean, you will need to use the tactic monad. But I would say if you want to do this, just learn about monads - it's not necessary to learn category theory beyond that. | |
| Feb 14, 2022 at 20:50 | comment | added | Bolton Bailey | @AndrejBauer I think one reason people feel these are connected is that proof assistants use monads, a concept from category theory. | |
| Feb 14, 2022 at 20:46 | comment | added | Andrej Bauer | What gave you the impression one needs category theory to use proof assistants, if I may ask? | |
| Feb 14, 2022 at 20:34 | history | answered | Bolton Bailey | CC BY-SA 4.0 |