Hi there, I'm looking, for fun, for a website that anyone can publish their formal proofs to (HOL, Isabelle, Coq, etc.)
The website would then, without any human verification, git clone the proof project from GitHub, run the proof, and show a web page saying "this was proved based on such and such axioms by this person". Once this is in place, we could then start trying to do more fun things like "here is a theorem statement without proof, send email when it (or any equivalents) gets proved", etc. II have been pointed to https://devel.isa-afp.org/ , but this list appears to be "manually" curated: someone decides if proofs are good enough, controls coding style, runs the proofs manually, so it is basically "just" a library. Basically what I want is a type of Package registry (PyPI, NPM) with continuous Integration for mathematics. If you know of anything in that area, do let me know! _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
