Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] library of proofs for Isabelle's ZF logic

Email Gateway (Aug 18 2022 at 09:36):

From: Slawomir Kolodynski <skokodyn@yahoo.com>
Some time ago I started a project on the savannah.org
server aimed at writing a library of formalized
mathematics for the Isabelle's ZF logic. It currently
features about 1200 theorems about general topology,
algebra (groups, rings and fields) and a construction
of real numbers as classes of integer almost
homomorphisms.
All proofs are written in Isar with emphasis on
readability.

Everyone who likes to write machine verifiable proofs
is invited to join the project. Please see the details
at
http://www.nongnu.org/isarmathlib/.

Slawomir Kolodynski

Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com

Last updated: Nov 21 2024 at 12:39 UTC