[Isarmathlib-devel] Is it worth to work on IsarMathLib?

[Victor Porton]

I did a contribution to IsarMathLib, the theory of generalization. The mission 
is accomplished.

Now I reason whether it is worth for me to continue to work with Isabelle or 
just to forget Isabelle and be busy with other things.

I'd like to formalize my theory of filters, filtrators, and what I call 
Algebraic General Topology (but I doubt whether it worth to spend time):

http://www.mathematics21.org/algebraic-general-topology.html

First, this would reliably wipe out mistakes if any.

The problem is that in IsarMathLib are missing lattices and complete lattices 
which would be a base for my theory. I reason whether it would be worth for me 
to continue with Isabelle and to code lattices, complete lattices myself, and 
afterward my theory.

Could we expect that lattices and complete lattices will arrive in IsarMathLib 
in near future even without my help?

Also look to my "Theorem 53" in my preprint article "Filters on Posets and 
Generalizations" http://www.mathematics21.org/binaries/filters.pdf (Yes, you'd 
not understand it, but that is not an issue.)

Theorem 53 For a semifiltered, star-separable, down-aligned filtrator (A; Z)
with finitely meet closed and separable core where Z is a boolean lattice and 
both
Z and A are atomistic lattices the following conditions are equivalent for any
F in A:
1. ...
2. ...
3. ...

The condition of this theorem is too long (that is there are too many 
conditions). Would formalizing it in IsarMathLib help me to receive help from 
other mathematicians who would possibly shorten my list of conditions? Does it 
make sense to work in IsarMathLib with that purpose?

So I need to decide, to continue with Isabelle or to forget about it.

-- 
Victor Porton - http://portonvictor.org