## Stream: general

### Topic: Isabelle Zulip?

#### Scott Morrison (Aug 13 2019 at 00:20):

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 (Aug 13 2019 at 06:40):

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 (Aug 13 2019 at 06:42):

:face_palm: Thanks :-)

#### Jeremy Avigad (Aug 13 2019 at 19:53):

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 (Aug 13 2019 at 23:59):

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.

Last updated: May 13 2021 at 19:20 UTC