Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "Proofs of life"


view this post on Zulip Email Gateway (Aug 22 2022 at 18:42):

From: Rene Vestergaard <renevestergaard@acm.org>
"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.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:43):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>

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@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@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.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:43):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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@acm.org>)
escribió:

view this post on Zulip Email Gateway (Aug 22 2022 at 18:43):

From: Rene Vestergaard <renevestergaard@acm.org>
I should have mentioned earlier that there's an accompanying video, with
proof visualization and more:

http://ceqea.sourceforge.net/extras/instructionalPoL.mp4


Last updated: Apr 20 2024 at 01:05 UTC