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?

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.

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

Thanks!

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?

@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: Jan 29 2023 at 08:28 UTC