Zulip Chat Archive

Stream: general

Topic: Isabelle Zulip?


view this post on 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.

view this post on Zulip 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/

view this post on Zulip Scott Morrison (Aug 13 2019 at 06:42):

:face_palm: Thanks :-)

view this post on Zulip 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.

view this post on Zulip 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 (Z/NZ)×(\mathbb{Z}/N\mathbb{Z})^\times, there are infinitely many primes not in that subgroup modulo NN but it doesn't go much further than that.


Last updated: May 13 2021 at 19:20 UTC