Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: the Three Squares Theorem

Email Gateway (May 16 2023 at 14:47):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new AFP entry, by Anton Danilkin and Loïc Chevalier: the Three Squares Theorem of Legendre. This result gives necessary and sufficient conditions for a natural number to be represented as the sum of three squares of integers. it’s a simple sounding result with a long and tricky proof.

https://www.isa-afp.org/entries/Three_Squares.html

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC