4 ms·
Who are automatic theorem provers aimed at? Computer scientists with an interest in maths or mathematicians with an interest in CS? If you are a mathematician s
by HidyBush 4y ago
Who are automatic theorem provers aimed at? Computer scientists with an interest in maths or mathematicians with an interest in CS? If you are a mathematician starting off with something like Coq is a nightmare. Nobody learns OCamel in college, math majors usually learn R, Python and maybe Java or C.
Making formal proving simple and intuitive is the first step to have it heavily adopted. It should look as close as possible to writing a proof in pure first order logic.
- rscho 4y agoIMO, you overstate the issue of syntax. As a hobbyist in both programming and math, Coq's syntax has never been the reason I failed to complete a proof. But perhaps I'm just too dumb and my difficulties lie elsewhere, so that's just my 2c. I think there's room for a spectrum of theorem provers made for academic pure mathematicians, industry programmers and everything in between. Those should perhaps not have identical syntax, neither should they have the same goals. To support my point, here's an example of an exotic theorem prover: https://github.com/webyrd/mediKanren https://github.com/webyrd/mediKanren It is aimed at medical researchers, and computes proofs about the medical literature, no less! This is a very different system and audience than which you are thinking about, but it's still a theorem prover.