Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Is Sergeyev's grossone theory formalized in Is...

Email Gateway (Oct 18 2022 at 07:13):

From: Marco Maggesi <marco.maggesi@unifi.it>
Hello everybody,

I remember seeing something about the computer formalization of Sergeyev's
grossone theory.
In my memory, it was a contribution in Isabelle/HOL.
Now, however, I am unable to find it again.

Does anyone on this list have information about it?

Thanks in advance,
Marco

Email Gateway (Oct 18 2022 at 09:46):

From: Manuel Eberl <manuel@pruvisto.org>
I for one have never heard of "grossones", let alone a formalisation of
them in Isabelle. Typically, such developments would end up in the
Archive of Formal Proofs (https://isa-afp.org), but there's nothing
there on this.

Of course it's possible that someone did it and just didn't publish it
in the AFP. But at least some quick googling did not turn up anything.

Manuel

Last updated: Jan 04 2025 at 20:18 UTC