Stream: Miscellaneous

Topic: Resources to get started with Coq


view this post on Zulip Kristaps Balodis (Apr 02 2022 at 22:36):

Hi! I apologize if this isn't the right place to post this. My name's Kristaps Balodis, I'm a PhD in pure mathematics, and a strong supporter (ideologically) of proof assistants. I have a little experience with Lean, but I'm trying to break into Coq in preparation for the Cortona summer school on univalence this summer.
Any suggestions for newbies in terms of reading/video resources to get started?

Also, I noticed there's a channel for doing constructive real analysis, has anyone started working on p-adic analysis in Coq?

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:37):

A lot of resources listed here: https://github.com/coq-community/awesome-coq#resources

Not aware of any p-adic numbers or similar in Coq.

view this post on Zulip Karl Palmskog (Apr 02 2022 at 22:38):

some videos are under "Shorter tutorials and videos" here: https://coq.inria.fr/documentation

view this post on Zulip Kristaps Balodis (Apr 02 2022 at 22:40):

Thanks!

view this post on Zulip Yosuke Ito (Apr 03 2022 at 05:45):

Welcome to Coq community, Kristaps!
I was also studying pure mathematics (representation theory) and I feel proof assistants prospective for the development of mathematics, too. If you don't mind, could you tell me why you are interested in formalizing mathematics?

view this post on Zulip Johan Commelin (Apr 09 2022 at 11:33):

@Kristaps Balodis There is a formalization of the p-adics in UniMath: https://github.com/UniMath/UniMath/tree/master/UniMath/PAdics So that's some form of Coq, and given that you want to prepare for that Cortona summer school, this might actually be the sort of formalization that you are interested in.


Last updated: Aug 19 2022 at 19:03 UTC