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

Reply via email to