Re:Any claim without a URI should be treated as suspicious
by adrianN on Monday July 20, 2020 @11:40AM
(#23898885)
Now you only need to convince the scientists to write proofs in their papers in Coq or Isabelle so that you can check them.
[ Parent
| on HN ]
Re:Any claim without a URI should be treated as suspicious
by btrettel on Monday July 20, 2020 @01:02PM
(#23899751)
I basically work in mathematical physics and I'd like a system that allows me to write one thing, and output LaTeX code that can be put in a publication and also check the math.
Coq and the like seem way too "low-level". I'm sure it's possible in principle to handle proofs involving partial differential equations in Coq but it surely is not easy.