Galois theory in Coq?

Stream: general

[Yury G. Kudryashov]

Hi, I remember that Galois Theory was formalized in Coq around the same time it was formalized in Lean but I fail to find a reference.

[Yury G. Kudryashov]

If you have a reference (or names), could you please share it with me?

[Johan Commelin]

https://drops.dagstuhl.de/opus/volltexte/2021/13903/ seems relevant

[Yury G. Kudryashov]

Thank you! One more question: AFAIR, there were at least 2 formalizations of the Jordan Curve Theorem. One of them is Thomas Hales, 2007 (Isabelle/HOL). What's the other one?

[Alex J. Best]

I found http://sakura.cs.shinshu-u.ac.jp/mizar/mma.dir/2007/MMA_2007_paper_4_for_web.pdf on google scholar is that what you were thinking of?

[Yury G. Kudryashov]

Thank you! I think, there was a Coq version too.

[Kevin Buzzard]

I would imagine that Gonthier would have needed something along these lines in his proof of 4 colour theorem but this is only speculation.

[Yury G. Kudryashov]

He proved a specific (polygonal?) version of the Jordan Curve Theorem.

[Yury G. Kudryashov]

From https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/gonthier-4colproof.pdf:

The machine formalisation of the Jordan Curve Theorem was the subject of several projects; T. Hales
has just announced that he had completed the proof using HOL Light. There seemed to be little point in
trying to replicate these works.

[Floris van Doorn]

Tom's 2007 paper has a good overview of the state at that time:

• There was at that time an ongoing formalization in Mizar, I don't know if that ever finished
• Tom formalized it in HOL Light
• The Isabelle formalization is by Larry Paulson, based on Tom's version

[Yury G. Kudryashov]

Which year is Larry Paulson's formalization?

[Yury G. Kudryashov]

I don't know how to tell it by that link.

[Floris van Doorn]

The history of https://github.com/seL4/isabelle/blob/master/src/HOL/Analysis/Jordan_Curve.thy suggests 2017

[Karl Palmskog]

https://github.com/coq-contribs/jordan-curve-theorem (history goes back to 2009) https://arxiv.org/abs/0802.2853

[Mario Carneiro]

the jordan curve theorem is also proved in Mizar - https://mizar.uwb.edu.pl/jordan/

[Yury G. Kudryashov]

This was already reported by @Alex J. Best above. I added it to the slides.

[Yury G. Kudryashov]

Thank you! I updated slides.

[Yury G. Kudryashov]

I wonder why the webpage you linked doesn't have authors' names. Is it their policy?

[Mario Carneiro]

No, the MML itself contains authors in the style of journal article submissions. I'm not sure what that page is, it seems to be some special page describing some aspect of jordan curve theorem and/or the Go game specification