Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] From the BOOK to the AFP: Two Squares via Invo...

view this post on Zulip Email Gateway (Aug 15 2022 at 15:39):

From: Lawrence Paulson <lp15@cam.ac.uk>
Maksym Bortin has contributed a new entry, containing "the involution-based proof of the two squares theorem from THE BOOK.”

It’s online at https://www.isa-afp.org/entries/Involutions2Squares.html

Due to a bug, the wrong email address is shown. Maksym’s address is maksym.bortin@taltech.ee>

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC