Isabelle Zulip?

Stream: general

[Scott Morrison]

I saw in Angeliki Koutsoukou-Argyraki‘s very nice note on her experience learning Isabelle/HOL https://www.researchgate.net/publication/334549483_FORMALISING_MATHEMATICS_-IN_PRAXIS_A_MATHEMATICIAN%27S_VERY_FIRST_EXPERIENCES_WITH_ISABELLEHOL a mention of a new Zulip for Isabelle. Does anyone know where it is? Googling only seems to find us.

[Kevin Kappelmann]

I saw in Angeliki Koutsoukou-Argyraki‘s very nice note on her experience learning Isabelle/HOL https://www.researchgate.net/publication/334549483_FORMALISING_MATHEMATICS_-IN_PRAXIS_A_MATHEMATICIAN%27S_VERY_FIRST_EXPERIENCES_WITH_ISABELLEHOL a mention of a new Zulip for Isabelle. Does anyone know where it is? Googling only seems to find us.

It's here: https://isabelle.zulipchat.com/

[Scott Morrison]

:face_palm: Thanks :-)

[Jeremy Avigad]

On a related note, I tried another experiment using Isabelle's Sledgehammer to prove that there are infinitely many primes congruent to 3 mod 4. In this case, Sledgehammer wrote most of the proof for me, and it felt pretty good. https://github.com/avigad/arwm/tree/master/isabelle_experiments.

[Kevin Buzzard]

How much easier is it in Isabelle than formalising the corresponding proof in Lean? Can you do 5 mod 6 using essentially the same argument? The low level argument you use will show that for any proper subgroup of $(\mathbb{Z}/N\mathbb{Z})^\times$, there are infinitely many primes not in that subgroup modulo $N$ but it doesn't go much further than that.