I applaud and encourage anyone who is interested in entering the field of mathematical biology, and in particular the mathematically rigorous formulation and elaboration of Darwin’s ideas about evolving populations. But I am more sanguine about the prospects for using the Coq proof assistant in that endeavour.
I don’t share the common reaction of many that the term ‘Darwinism’ is just a misleading label invented by creationists. To me it’s a fair label for the adoption and study of Darwin’s main thesis – namely that the present distribution and variety of biological species can be explained as the result of a process of natural selection from the results of reproduction with random variation.
And it is certainly possible to formulate various mathematical models of the evolutionary process and prove theorems about them. Such models, like most classes of mathematical objects, can often be defined either in terms of axioms of their own or as structures within some broader axiomatic system. (For example, the important class of von Neumann algebras can be identified either concretely as subalgebras of the set of bounded operators on a Hilbert space or more abstractly by the axioms of a W*-algebra.)
However, no such model claims to capture all of the complexity of real-world biologies, so there is no single officially recognized set of such axioms for Darwinism.
The basic first step towards entering this field is probably getting a firm background in basic probability theory (not just the discrete case but also including probability measures on continuous spaces) and stochastic processes of various kinds. And a parallel step should probably be learning as much as possible of what is currently known about the actual processes of inheritance – including both the genetic coding of protein sequences and the inheritable epigenetic systems that govern the reading and expression of those genes.
This is an exciting area of study ripe for the application of new mathematical techniques (such as renormalization group theory which originated in theoretical physics). But I am almost certain that automated proof systems will not be of any use in formulating plausible conjectures, and doubt that the mathematical structures involved are particularly well suited to their capabilities for constructing proofs once such conjectures have been identified.
So if your real interest is in learning about and applying automated proof systems, then I would suggest that doing so in a different context might be more fruitful.