Email Gateway (Aug 22 2022 at 18:39): Email Gateway (Aug 22 2022 at 18:39):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to understand if it would be feasible for me to propose my own
contributions to HOL. I have read the section "Publish contributions as an
external" on the Isabelle community wiki (
https://isabelle.in.tum.de/community/Publish_contributions_as_an_external).
I am also aware of the mailing list isabelle-dev@in.tum.de. However, this
is a general question about the possibility of a contribution being
considered, given certain specific circumstances. Thus, I believe that it
may be more useful to this mailing list, rather than isabelle-dev@in.tum.de.
Otherwise, of course, please suggest to forward it to isabelle-dev@in.tum.de
.
My primary concern is that I am not affiliated with an academic group or a
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle community.
Thus, I would like to assess whether or not my contributions would be
considered on this basis. Of course, I am also aware of the existence of
the AFP. However, I believe, some of the theorems that I would like to
propose naturally extend some of the theories that are already available in
HOL and, most likely, are not suitable to be published as an independent
AFP library.
To be more specific, I would like to provide several examples of the
contributions that I would like to propose. At the moment, HOL-Algebra
contains the theory IntRing.thy that contains the lemmas "ZFact_zero:
"carrier (ZFact 0) = (⋃a. {{a}})"" and "ZFact_one: "carrier (ZFact 1) =
{UNIV}"". However, it does not seem to contain a lemma that could describe
the carrier of a more general quotient ring "ZFact (m::int)" (e.g. "0 < m
⟹ carrier (ZFact m) = {X. ∃n ∈ {0..<m}. X = {x. m dvd (x - n)}}"). Also, I
was not able to find a relatively standard textbook theorem that
characterises a cyclic group in terms of the quotient group "add_monoid
(ZFact m)" (e.g. "finite (carrier G) ⟹ order G = m ⟹ ∃a ∈ carrier G.
carrier G = {a[^]i | i::int. i ∈ UNIV} ⟹ add_monoid (ZFact m) ≅ G"). Some
of the potential contributions are not independent theorems, but minor
extensions of the existing lemmas in "HOL", e.g. lemma "ord_dvd_pow_eq_1"
in "Algebra-Multiplicative_Group" shows that "finite (carrier G)", "a ∈
carrier G" and "a [^] k = 𝟭" together imply "ord a dvd k", where "k" is of
the type "nat". However, this lemma holds even if "k" is any number of the
type "int" (the existing proof would need to be amended to take into
account the negative values of k).
Thank you
(I would prefer not to disclose my contact details publicly for the reasons
of privacy and as a measure against spam)
Email Gateway (Aug 22 2022 at 18:39):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
"mailing-list anonymous" wrote:
I would like to understand if it would be feasible for me to propose my own
contributions to HOL.
If some of your results are related to number theory, you could include
your contributions in my project of a library "number theory miscellany".
Here is my repository :
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
But, you should include in the file either your name or a pseudonym, in
order to distinguish your contributions from my contributions. Maybe you
prefer your own miscellany, e.g., "general miscellany", "topology
miscellany", etc. In my case, my main motivation to contribute, beside the
pleasure of proving some truth, is to increase my CV, because some
reviewers of important journals, e.g., American Mathematical Monthly, said
to me that my proofs are too long to be checked and that they are annoying
for the readers (someone is confusing mathematics with comic strips). I am
successfully proving the theorems from my Master Memoir in Isabelle one by
one (work-in-progress). My first version is rather non-algorithmic, but I
have the project to include an algorithmic version in order to do explicit
computations.
"mailing-list anonymous" wrote:
My primary concern is that I am not affiliated with an academic group or a
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle community.
Me neither, nevertheless, the Isabelle community, at least in my case, was
the most open research community that I have ever met. Other research
communities, like the communities of pure mathematics, are rather closed
and mathematicians in general do not read the works of outsiders (they have
not time for that), e.g., the old Gauss did not read the work of the young
Abel, because he assumed that it was wrong, the old Cauchy did not read the
work of the young Galois, etc. Proof assistants are the key for an outsider
to become an insider, because the computer guarantee that the result is
fine, even if the proof is very complex. Nevertheless, I advice you to
become part of something and to change when you will be ready: the academic
growth is step by step.
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 18:39):From: Paulo Emílio de Vilhena <pevilhena2@gmail.com>
Hello,
I’m not answering your question, but since you are working on HOL-Algebra I
would like to point out a github repository where we propose not only to
extend this library with new theories but also to revise old ones. For
instance, we already have one of the mentioned theorems you were looking
for: it is the lemma mod_ring from the theory Int_Ring (note the underline)
stated as
lemma (in int_ring) mod_ring:
assumes "a ∈ carrier R - { 𝟬 }"
shows "carrier (R Quot (PIdl a)) = (λi. PIdl a +> ⟦ i ⟧) ` {0..< ¦
int_repr a ¦}"
It’s overly complicated for now, because it’s stated for all rings
isomorphic to the ring of integers, but you can easily instantiate it for
Z. We also have a theory called Multiplicative_Group_Revised where I
started an analogous development of Multiplicative_Group but more concise
since it reuses previous developments from cycles and permutations.
Other than that, there are theories on algebraic numbers, field extensions
and division of polynomials. Our most impressive result is the existence of
the algebraic closure of a field. Here is the link for the repository in
case you want to check it out: https://github.com/DeVilhena-Paulo/GaloisCVC4
Thanks,
Paulo.
Message: 5
Email Gateway (Aug 22 2022 at 18:39):From: Tobias Nipkow <nipkow@in.tum.de>
You do not have to be affiliated with anybody to contribute to Isabelle/HOL
theories but there is no well-established process for contributing. For small
amendments you can either send them to this mailing list or contact individuals,
like the web page says that you found.
Larger contributions require more interaction with people who feel responsible
for some area. In the case of Algebra, Paulo has already indicated that there
are parellel developments that you may be able to liaise with.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 18:39):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
In what follows, I address everyone who replied to my email (not in any
particular order).
To Tobias Nipkow,
Thank you for your reply. I am glad that it is potentially possible for me
to make contributions to HOL. However, of course, given that potentially
anyone can make a contribution, it would be nice if there was a
well-established process for making contributions.
To Paulo Emílio de Vilhena,
Thank you for your response and for providing the link to the repository
GaloisCVC4. I have several questions about the repository:
I would like to confirm that, while the main purpose of the project
GaloisCVC4 is the development of Galois Theory in the context of
HOL-Algebra, you are also making changes to HOL-Algebra that are not
directly related to the main line of the development of the project
GaloisCVC4, i.e. you may consider adding to the repository any established
results from algebra or making minor amendments/extensions of the existing
theorems that do not contribute to the main line of the development.
Furthermore, I would like to understand if your intention is to
integrate GaloisCVC4 with HOL-Algebra or publish it in the context of the
AFP.
Also, I would like to understand if you intend to discontinue the work
on the project after a certain deadline or after you achieve certain
milestones.
If my understanding of the dual purpose (see clause 1) of the project
GaloisCVC4 is correct, would you, potentially, accept pull requests from
external contributors?
Also, thank you for pointing out the existence of the (Isabelle)
generalisation of the proof of the characterisation of the carrier of Z/mZ.
I only wish I knew about the existence of GaloisCVC4 earlier.
To José Manuel Rodriguez Caballero,
Thank you for your reply and for providing the link to your repository. It
is good to know about the existence of this repository because it seems
that there is no mention of it in the AFP at the moment (although I cannot
be entirely certain). The lemmas that I have mentioned in my question may
fit within the context of the repository. However, they are also very
closely related to the existing Isabelle theories within HOL-Algebra, as
confirmed by Paulo Emílio de Vilhena, who has already proven a
generalisation of one of the theorems that I mentioned in my question in
the context of an ongoing development of HOL-Algebra (unfortunately, I was
not aware of this development before asking the question). Regardless, if
possible, I would appreciate if you could reconfirm that potentially you
could accept pull requests from external contributors. Nevertheless, I have
to admit, that it is unlikely that I will produce any further proofs of
results that are related to number theory in the near future.
With regard to non-technical part of your answer, previously, I used a
pseudonym xanonec on this mailing list. I also use it on Stack Overflow.
However, it seems that mailing-list-anonymous is slightly more
'professional' in some sense. Also, I am only trying to hide my real
contact details/identity from third parties (especially spam lists/online
scam/etc). There is a good reason why there is a variety of privacy
settings available on the websites like LinkedIn and Facebook and it is
possible to control who can see your posts/profile/personal information.
However, unfortunately, mailing lists do not provide such options and,
furthermore, all posts can be found via Google. In general, I prefer the
website Stack Overflow to mailing lists. However, it seems that Isabelle
community is not very active on Stack Overflow, because some of the
questions that I tried to ask there were left without a reply/comments for
days. Nevertheless, I was able to obtain a reply to the same questions
using this mailing list within hours.
Thank you
Email Gateway (Aug 22 2022 at 18:40):From: Makarius <makarius@sketis.net>
See README_REPOSITORY. In particular:
"""
Content discipline
The following principles should be kept in mind when producing
changesets that are meant to be published at some point.
* The author of changes needs to be properly identified, using
[ui]username configuration as described above.
While Mercurial also provides means for signed changesets, we want
to keep things simple and trust that users specify their identity
correctly (and uniquely).
"""
It means you need to disclose your real name when submitting changesets.
(This is not Wikipedia where anonymous entities are allowed to do
strange things in the dark.)
Moreover it should be clear that any contribution is subject to the
existing BSD-style license scheme of the Isabelle sources: without
amendments nor exceptions.
Makarius
Email Gateway (Aug 22 2022 at 18:40):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
mailing-list anonymous:
Regardless, if
possible, I would appreciate if you could reconfirm that potentially you
could accept pull requests from external contributors.
Sure, everybody is welcome to contribute to the miscellany in number theory
(I am myself external). Also, if another person want to create another
project about miscellany, e.g., miscellany in topology, I will be glad to
contribute. I think that the best way to contribute is to make some link in
github. I have not experience about using github (maybe you have more
experience than myself in this topic). My official formation was in pure
mathematics, the computer sciences that I am doing is self-taught.
mailing-list anonymous:
It is good to know about the existence of this repository because it seems
that there is no mention of it in the AFP at the moment (although I cannot
be entirely certain)
I have the project to submit my results to AFP in the future, after proving
ALL the theorems from my Master Memoir. These theorems were new in the
literature, here is the video-abstract of my last publication (my goal is
to formalize everything until this level):
https://www.youtube.com/watch?v=Ms9lrm4wLDQ
I have not problem to include other peoples as coauthors, because this is
the spirit of miscellany. I do not say that my theory is miscellany, what I
say is that my theory is so powerful that it can be used in order to prove
miscellany results in number theory, e.g., unexpected connections between
the semi-perimeter of a Pythagorean triangle and 2-densely divisible
numbers.
mailing-list anonymous:
With regard to non-technical part of your answer, previously, I used a
pseudonym xanonec on this mailing list.
Ok, you could write in your Isabelle file "xanonec" or just your name if
you want to be recognized. If your write "mailing-list anonymous" in your
Isabelle file, people evidently will think that there was a mistake of
copy-paste. Also, the problem of calling yourself "anonymous" is that
another person can call himself/herself "anonymous" too: it is like the guy
called "Anonymous" to whom many quotations are attributed. The name is just
a mask, so being anonymous is to put your mask out.
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 18:40):From: Paulo Emílio de Vilhena <pevilhena2@gmail.com>
Hi,
1.
You are right about this. While my goal was the development of Galois
Theory, the project was actually born as an attempt from me and Martin
Baillon to reduce the amount of changes to HOL-Algebra we were both making
independently.
2.
The idea is to integrate the material which could be considerate as
fundamental to any development in algebra and publish in the context of the
AFP more specific material. We already have a big part of our material in
the library and recent releases of Isabelle will come with some of my
revised theories and sophisticated tricks such as Weak_Morphisms.thy.
3.
The project was the subject of an internship in the ALEXANDRIA team,
supervised by Larry Paulson. The internship is already over and it is not
being trivial to find time to work on the project, but I do intend to
continue. The Galois correspondence theorem is certainly a milestone, but
there is a lot of work to be done on the library itself. I think it’s
preferable to progress horizontally in a proper way than to quickly prove
profound statements in a formalism that nobody will be able to use.
4.
Contributions are welcome :) I’m quite jealous with my theories and
proofs, I must say, but if you have well-founded contributions to make, I
will probably accept. By well-founded I mean that it should have at least a
minimal explanation on why such a modification would make sense. For the
moment, there are two theories in need of revision/development that may
interest you: Int_Ring.thy and Multiplicative_Group_Revised.thy. Int_Ring,
because I think that talking about rings isomorphic to Z only complicate
things and I did that to overcome a problem which does not exist anymore,
so merging Int_Ring and IntRing is something desirable.
Multiplicative_Group_Revised should just be continued.
Lastly, I would like to thank you for your interest on the project, I hope
you will be able to find and use what you need in GaloisCVC4. If you have
any suggestions or if you find that something in our formalism was not well
thought, I’m always keen to discuss.
Paulo.
Email Gateway (Aug 22 2022 at 18:40):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to thank everyone who replied to my original query. I believe
that my question was answered in full and I would like to propose (without
being insistent) to close this topic. I would also like to make several
concluding remarks in response to the replies in Digest Vol 160, Issue 15.
However, please note that I may leave further comments on this topic
without a reply.
To Makarius,
Thank you for your comment. Of course, it was not my intention to ask
whether or not I am allowed to change or ignore any of the documented
practices for making a contribution to Isabelle/HOL. My primary concern was
whether or not my contributions would be considered if I was to propose
them while not working under the supervision of one of the existing regular
co-developers of Isabelle/HOL and while not being affiliated to a
research group that regularly works with Isabelle/HOL (at the moment,
Isabelle/HOL is merely one of my past-time hobbies). I believe that this
issue has not been documented anywhere. However, as I mentioned in my
original query, I formed an impression that all of the contributions to HOL
were made by established academics in the areas of logic/formal
verification/mathematics or students working under their supervision. Thus,
I wanted to ensure that if I was going to make a proposal, it would not be
ignored/rejected because of the aforementioned circumstances.
As a side note, based on the replies given by Paulo Emílio de Vilhena (see
below), if I decide to submit my contributions to the community, it is
likely that I will try to do so indirectly through the repository
GaloisCVC4 (also, see the next section in my reply).
To Makarius and José Manuel Rodriguez Caballero,
I have no intention to hide my identity from the regular users of this
mailing list. However, I would prefer to remain anonymous to the general
public. Of course, anyone who needs to know my name/contact details for any
good reason can inquire about them in a personal email (with the
understanding that they are not to be shared without my consent). Also, of
course, it is in my interest to associate my name with my contributions if
they are to be accepted (whether they are contributions to Isabelle/HOL or
a private repository of an academic).
To Paulo Emílio de Vilhena,
Thank you for the detailed reply.
I would like to make several comments with regard to clause 4 in your reply:
Firstly, given that you have already introduced (or seem to be working
on) a significant number of the contributions that I was going to propose,
it seems now that it is slightly less likely that I will make any attempts
to make contributions in the very near future.
I have a certain amount of experience in computer programming and I am
familiar with the feeling that one can get when an external entity with
less experience is trying to 'sabotage' your code base or your intended
direction for the development. Luckily, at least, it is nearly impossible
to introduce errors/bugs in Isabelle theorems. If I will ever make an
attempt to make a contribution, then I will also make every attempt to
ensure that it is either peripheral to the main line of the development or,
at least, it is very unlikely to have any negative impact on the main line
of the development. Of course, I would submit a pull request on GitHub and
you are welcome to reject it if you decide that it is not suitable
(obviously, if you do decide to reject it, I will appreciate any
constructive feedback).
If there was an active issue tracker for the project, I would also be glad
to look into the problems that you would like to be solved, but you believe
that they have a low priority (i.e. the problems that you would not want to
spend your time on). However, most certainly, I cannot guarantee my
commitment (as I mentioned somewhere in this reply, at the moment,
Isabelle/HOL is merely one of my past-time hobbies). Thus, please do not
start an issue tracker on my behalf :).
"I think that talking about rings isomorphic to Z only complicate
things...". I cannot imagine that anyone who is able to understand the
content of HOL-Algebra will not be able to specialise theorems in Int_Ring
to their needs. However, most certainly, it would be useful not to expect
the users to specialise the results to Z in almost every individual library
that uses Int_Ring (in all probability, Z would be a very common
application of theorems in Int_Ring).
To José Manuel Rodriguez Caballero,
Thank you for providing further information and for the confirmation that
you may be able to accept pull requests. Based on the latest reply by Paulo
Emílio de Vilhena, it seems that it is much more likely that I will be
(potentially) submitting my contributions to GaloisCVC4, because, I
believe, my (potential) contributions are more suitable for a library that
is closely associated with HOL-Algebra than a library in the area of number
theory. However, if any of my contributions will be rejected (for any
reason other than the quality of my proofs or originality) or if I will
ever formalise anything that may be more suitable for your repository, I
will let you know.
Thank you
Last updated: May 06 2024 at 12:29 UTC