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 think a more fruitful use of proof assistants in this space is to have proven correct statistical analysis tool, where correct means that the analysis tool reports error bounds that match the model (or are overestimates, etc). All the real world interactions can't be axiomatized in any reasonable way: the correctness of the model, the incoming data, the correct usage of the tool.
How do you expect proofs will help here? On Sun, Mar 29, 2020 at 5:00 PM José Manuel Rodríguez Caballero < [email protected]> wrote: > Hello, > Disclaimer: This post is about a mental exercise, I will not apply this > theory in real-life situations. > Recently I was thinking about how to use proof assistants in order to > substitute to some extent the role of medical doctors. My motivation is > obvious: medical doctors are the main victims of COVID-19, whereas the > behavior of the pandemic is approximately exponential growth in many > countries (I know that it will change... someday). So, we need to think > about how to survive in a world without medical doctors (this mental > exercise may become the reality for some people, maybe most people on the > planet). The only solution that I see is to have a proof assistant library > about medicine and people without access to a medical doctor, but having a > computer, will use the library in order to self-medicate, but the proof > assistant will prevent them to make mistakes. Indeed, a file with a medical > proof using the proof assistant should be sufficient in order to have the > right to get medication, with the same value that a medical prescription > (this is a mental experiment, I am not suggesting to do it). > How to convince the government that a medical proof (accepted by a proof > assistant) has the same value (or even more value) than a medical > prescription? My proposal is to apply the Turing test in order to prove > that the library is statistically indistinguishable from a medical doctor. > My questions are: > > a) How to express medical information in a proof assistant? > > b) Could metamath be useful for such a task? > > Kind regards, > José M. > > -- > 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/1cbe6b08-03a8-42e7-b965-59ec38057323%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/1cbe6b08-03a8-42e7-b965-59ec38057323%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsX%2ByV%3D0czpy1wpuL8hDRfSmP-A80Qo8zfKBd7mEL%3DpZA%40mail.gmail.com.
