isarmathlib-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Isarmathlib-devel] [FOM] Harrison Advocates ZFC


From: Slawomir Kolodynski
Subject: Re: [Isarmathlib-devel] [FOM] Harrison Advocates ZFC
Date: Mon, 6 Aug 2018 08:45:36 +0000 (UTC)

> Have you ever announced it to the Isabelle mailing list?

Yes, IsarMathLib showed up a couple of times on the Isabelle mailing list.
As for the complex numbers there is very little done, just basic definitions (construction) starting from a model of real numbers and the proof that Metamath axioms of complex numbers are satisfied, see http://isarmathlib.org/Complex_ZF.html .

Kind regards,

Slawomir


http://savannah.nongnu.org/projects/isarmathlib Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)


On Monday, August 6, 2018, 9:12:36 AM GMT+2, Askar Safin <address@hidden> wrote:


This is not my library, it is Slawomir's one. I simply found it in the internet one day. I tried to CC him.
Askar Safin

>Воскресенье,  5 августа 2018, 14:49 +03:00 от Lawrence Paulson <address@hidden>:
>
>That’s amazing! And it needs to be publicised more. Have you ever announced it to the Isabelle mailing list?
>Larry
>
>> On 5 Aug 2018, at 06:40, Askar Safin < address@hidden > wrote:
>>
>>> Isabelle/ZF is untyped, which unfortunately means it can't use Isabelle's linear arithmetic decision procedures, so arithmetic reasoning is difficult. We don't have a construction of the rational numbers, let alone the complex numbers
>> IsarMathLib (  http://www.nongnu.org/isarmathlib ) is based on Isabelle/ZF and it has real and complex numbers
>>
>> ==
>> Askar Safin
>>  http://vk.com/safinaskar

reply via email to

[Prev in Thread] Current Thread [Next in Thread]