> On Sun, Mar 29, 2020 at 5:00 PM José Manuel Rodríguez Caballero < > [email protected]> wrote: ... > > Recently I was thinking about how to use proof assistants in order to > > substitute to some extent the role of medical doctors.
On Sun, 29 Mar 2020 17:42:14 -0700, Mario Carneiro <[email protected]> wrote: > I don't see how this would be workable. Medical information is not logical > deduction, and there is very little logical deduction involved. It is all > about statistics, and a proof assistant is not the best way to organize > that data. I agree. Indeed, IBM's experience with Watsom may be instructive. Watson managed to win at "Jeopardy", and that win was rightfully hailed as a stellar achievement in AI. IBM has since been working to apply Watson to medical work, and that hasn't had the same level of success. That doesn't mean it's *impossible*, but it turns out to be *much* more difficult for machines to reasonably do things like medical diagnosis in a serious way. You might use proof tools to prove that a program performs a task. But these are not the kind of tasks that we know how to mathematically model (yet). In addition, program proofs take time, and taking extra time is probably not what you want to do if your focus is COVID-19. It's perfectly reasonable to say, "I have problem X; could tool Y help?". But I don't see how to match proof tools to this problem at this time. I'd be delighted to be proven wrong :-). --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jIjpO-0004Bg-9P%40rmmprod07.runbox.
