search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

Adding issues and milestones #2

Closed dan323 closed 1 year ago

dan323 commented 4 years ago

Hello @SKolodynski,

I am wondering if we could add a list of theories or theorems you may want in the project as issues in this repo. So that everyone is in the same page. Also, just to note that my request should be merged in the next release as IsarMathlib is not executable as it is now.

Thank you, Daniel de la Concepción Sáez

SKolodynski commented 4 years ago

I will list things that I am thinking about. Right now it is mostly around properties of uniform spaces. Or maybe one can use the list of areas Kevin Buzzard thinks are fashionable
But the number of things that have been formalized in IsarMathLib is so small that really anything you think about is fine. Of course your pull request will be merged in the next release. The issue there was that the ROOT file did not list a couple of theories, in particular the one you fixed, so no errors were flagged during release check. But of course the stuff that went into the proof document was correct. Slawomir

dan323 commented 4 years ago

I would also try to convince you to instanciate sublocales instead of simply proving group0(G,f) in topgroup, for example. It would make the proofs so much easier. Section 4 in https://isabelle.in.tum.de/doc/locales.pdf