Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Archive of Formal Proofs

Email Gateway (Aug 18 2022 at 10:47):

From: Tobias Nipkow <nipkow@in.tum.de>
Today I have added two articles by Roelof Oosterhuis into the
development branch of the AFP:

1. Fermat's Last Theorem for exponents 3 and 4
2. Sums of 2 and 4 squares

Note that they are not visible in the 2005 version of the AFP. They will
appear in the development snapshot of the AFP in a few days.

Enjoy,
Tobias

Email Gateway (Aug 18 2022 at 11:43):

From: Lawrence Paulson <lp15@cam.ac.uk>
Just published at the Archive of Formal Proofs is an entry entitled
Recursion Theory I by Michael Nedzelsky. The formalization of more
recursion theory would certainly be welcome.

http://afp.sourceforge.net/

Larry Paulson

Entry name:
Recursion-Theory-I

Abstract:
This document presents the formalization of introductory material from
recursion theory --- definitions and basic properties of primitive
recursive
functions, Cantor pairing function and computably enumerable sets
(including a proof of existence of a one-complete computably
enumerable set
and a proof of the Rice's theorem).

Last updated: May 03 2024 at 12:27 UTC