# Re: [Hol-info] Fwd: Is there any good web inteface for formally proven mathematical theorems that anyone can contribute to without manual proof review?

Then, may I hear:  what are the values of the functions \tan (\pi/2) and
y=1/x at x = 0?


*viXra:1904.0408 <http://vixra.org/abs/1904.0408>* *submitted on 2019-04-22
What Was Division by Zero?; Division by Zero Calculus and New World

With best regards,
Sincerely yours,

Saburou Saitoh
2019.7.13.18:43

2019年7月13日(土) 16:46 Ciro Santilli <ciro.santi...@gmail.com>:

> 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
>

_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info