Kristaps Balodis (Apr 02 2022 at 22:36): 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?
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.
Karl Palmskog (Apr 02 2022 at 22:38):some videos are under "Shorter tutorials and videos" here: https://coq.inria.fr/documentation
Kristaps Balodis (Apr 02 2022 at 22:40):Thanks!
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?
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: Apr 19 2024 at 12:02 UTC