Discussion:
[Coq-Club] "Proofs of life"
Rene Vestergaard
2018-11-07 01:37:50 UTC
Permalink
"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.
José Manuel Rodriguez Caballero
2018-11-07 20:55:34 UTC
Permalink
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
Post by Rene Vestergaard
"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.
José Manuel Rodriguez Caballero
2018-11-08 00:05:54 UTC
Permalink
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.
Dear José Manuel Rodriguez Caballero,
Thank you for the suggestion. Cancer cells would be a very ambitious
target, indeed.
Cheers,
Rene
Post by José Manuel Rodriguez Caballero
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.
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
Post by José Manuel Rodriguez Caballero
Sincerely yours,
José Manuel Rodriguez Caballero
El mar., 6 nov. 2018 a las 20:39, Rene Vestergaard (<
Post by Rene Vestergaard
"Proofs of life: molecular-biology reasoning simulates cell behaviors
from first principles" is now available at
http://arxiv.org/abs/1811.02478
Post by José Manuel Rodriguez Caballero
Post by Rene Vestergaard
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.
Post by José Manuel Rodriguez Caballero
Post by Rene Vestergaard
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.
Rene Vestergaard
2018-11-09 07:27:21 UTC
Permalink
I should have mentioned earlier that there's an accompanying video, with
proof visualization and more:

http://ceqea.sourceforge.net/extras/instructionalPoL.mp4
Post by Rene Vestergaard
"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.
Loading...