Re: [isabelle] "Proofs of life"



>
> Rene wrote:
> Cancer cells would be a very ambitious
> target, indeed.


I agree. Indeed, I cancelled my independent research project about
detection of cancer cells using proof assistants for lack of funding. Here
is the link to my cancelled campaign:
http://www.kicktraq.com/projects/1176467506/cancer-vs-mathematics/

My idea was as follows:

(1) A medical doctor takes a sample of cells from a part of the patient's
body that he/she suspects it is cancerous.

(2) A machine transfers the chemical structure of the ATP molecules from
the cells to a computer.

(3) A proof assistant take as input an ATP molecule and it returns TRUE if
it is generated by respiration, otherwise, it returns FALSE (in this case,
the ATP was generated by fermentation).

(4) According to Warburg's theory, the proportion of values TRUE and FALSE
will determines if the sample is cancerous or not.

I was interested in developing a library in Isabelle/HOL for step (3), but
maybe someone else will do it in the future: I have not material conditions
to adventure in an independent scientific research.

The naked mole rats are the living proof that Warburg was right: these
animals cannot develop cancer, because their cells are adapted to both the
ATP generated by respiration and the ATP generated by fermentation.
https://www.sciencedaily.com/releases/2013/07/130731093255.htm

Kind Regards,
José M.

El mié., 7 nov. 2018 a las 17:08, Rene Vestergaard (<renevestergaard at acm.org>)
escribió:

> Dear José Manuel Rodriguez Caballero,
>
> Thank you for the suggestion. Cancer cells would be a very ambitious
> target, indeed.
>
> Cheers,
> Rene
>
> On 11/8/18 5:57 AM, José Manuel Rodriguez Caballero wrote:
> > Dear Dr. Vestergaard,
> >
> >    I would like to suggest you to apply your approach to cancer cells,
> > following Warburg’s theory. There are many controversies about Warburg’s
> > point of view, but as far as I know, all the attempt of refutations were
> > counterattacked by Warburg himself and by his followers.
> >
> > Here is the main reference:
> >
> > Warburg, O. (1956). On the origin of cancer cells. Science, 123(3191),
> > 309-314.
> >
> >
> https://www.jstor.org/stable/pdf/1750066.pdf?casa_token=LA_9haDJ8xsAAAAA:EBO2uCgdY7EJh3ZhkfmX7AtoYr_M5Xfv6lip-oX6I-TBG_6FsJrH5H1JWgbG-fgUKMZqI4L2R_piQ5qnGNTuXSaEbEZz-2cpiejJxhfux_1fXw49LSmp
> >
> >
> > Sincerely yours,
> > José Manuel Rodriguez Caballero
> >
> > El mar., 6 nov. 2018 a las 20:39, Rene Vestergaard (<
> renevestergaard at acm.org>)
> > escribió:
> >
> >> "Proofs of life: molecular-biology reasoning simulates cell behaviors
> >> from first principles" is now available at
> http://arxiv.org/abs/1811.02478
> >>
> >> The work springs from computer-verified reasoning and establishes wider
> >> utility by means of a reasoning-computation correspondence, including
> >> for long-standing critical problems in biology that have defied standard
> >> approaches.
> >>
> >> Sincerely,
> >> Rene
> >>
> >> -----
> >>
> >> ESSENCE
> >> Mathematics-style correctness works for molecular biology and enables
> >> phenotype and life-cycle prediction from genotypes. Formally,
> >> reductionist science involves constructive reasoning, i.e., executable
> >> simulation.
> >>
> >> SIGNIFICANCE
> >> Axiomatic reasoning provides an alternative perspective that allows us
> >> to address long-standing open problems in biology. Our approach is
> >> supported by meta-theory and likely applies to any reductionist
> discipline.
> >>
> >> ABSTRACT
> >> Science relies on external correctness: statistical analysis and
> >> reproducibility, with ready applicability but inherent false
> >> positives/negatives. Mathematics uses internal correctness: conclusions
> >> must be established by detailed reasoning, with high confidence and deep
> >> insights but not necessarily real-world significance. Here, we formalize
> >> the molecular-biology reasoning style; establish that it constitutes an
> >> executable first-principle theory of cell behaviors that admits
> >> predictive technologies, with a range of correctness guarantees; and
> >> show that we can fully account for the standard reference: Ptashne, A
> >> Genetic Switch. Everything works for principled reasons and is presented
> >> within an open-ended meta-theoretic framework that seemingly applies to
> >> any reductionist discipline. The framework is adapted from a
> >> century-long line of work on mathematical reasoning. The key step is to
> >> not admit reasoning based on an external notion of truth but work only
> >> with what can be justified from considered assumptions. For molecular
> >> biology, the induced theory involves the concurrent running/interference
> >> of molecule-coded elementary processes of physiology change over the
> >> genome. The life cycle of the single-celled monograph organism is
> >> predicted in molecular detail as the aggregate of the possible
> >> sequentializations of the coded-for processes. The difficult question of
> >> molecular coding, i.e., the specific means of gene regulation, is
> >> addressed via a detailed modeling methodology. We establish a
> >> complementary perspective on science, complete with a proven correctness
> >> notion, and use it to make progress on long-standing and critical open
> >> problems in biology.
> >>
> >>
> >
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.