The paper of Ho et. al. quoted in my last post refers to a paper of Perelson et. al. (Mathematical Biosciences 114, 81-125). There a detailed mathematical analysis is carried out. The main type of cells infected by HIV are the CD4+ T-cells (also known as T-helper cells). In the model in the paper of Perelson et. al. the dynamics of the populations of virions and T-cells are included. The infection of the cells by the virus is taken into account but the immune response, by which the T-cells act back on the virus, is not. The basic mathematical object of study there is a system of four ordinary differential equations. The unknowns are the densities of uninfected T-cells, latently infected T-cells (i.e. those which are not yet producing new virions), actively infected T-cells and virions. The paper starts with the common procedure in looking at dynamical systems of finding the equilibrium solutions and determining their stability by linearization. Depending on the value of a particular parameter there are either one or two stationary solutions which may be biologically relevant. They change their stability properties at the critical value of the parameter where the second stationary solution appears. At the first equilbrium the virus density is zero and when the long-time behaviour is described by convergence to this equilibrium it means clearance of the virus. At the second equilibrium point both virus and T-cells are present and when the long-time behaviour is decribed by convergence to this equilibrium it corresponds to an endemic state where the infection persists. An interesting question is: are other types of long-time behaviour possible and if so can it be proved? This kind of ODE system can be treated rather successfully by numerical methods and very often this is considered enough. A conclusion of the paper of Perelson et. al. is that for certain values of the parameters in the system no other behaviour is possible and that this includes all parameter sets which are biologically relevant. This last conclusion depends on the experimental data. They also map out a parameter regime where there is a periodic solution which acts as an attractor. This means that the system shows persistent oscillations. Most of these conclusions are based on numerical work. For a certain set of parameters the conclusions are proved rigorously using a Lyapunov function. There is also some heuristic analysis of certain phases of the dynamics using a quasi-steady state assumption. From the point of view of the role of mathematical proofs the remaining questions are: can the statements about the late-time behaviour be proved rigorously and what advantages could result from doing so?
There is a paper by Shaw et. al. which is in some ways similar to that of Ho et. al. and which appeared back to back with it in the journal (Nature, 373, 117-122). It uses slightly different mathematical models and here some simple equations are included in the text. Nowak is one of the authors and here there is a close link to his book with May quoted previously. Neither the paper nor the book pay much attention to questions of rigorous proofs of the qualitative behaviour of solutions. More recently some papers have appeared which provide an anlysis of this kind. In a paper of De Leenheer and Smith (Siam J. Appl. Math. 63, 1313-1327) the theory of monotone dynamical systems is applied. This is a method which can be used to effectively reduce the dimension of a dynamical system by one if it has a special algebraic structure. If the original system is three-dimensional, and thus potentially involves strange attractors, the reduced system is two-dimensional. Much more powerful tools such as
Poincare-Bendixson theory are available in the two-dimensional case and rule out many complications. De Leenheer and Smith use this observation to give a rigorous global qualitative analysis of some systems arising in virus dynamics, including ones involving periodic solutions. Part of the results of this paper have also been proved in a more elementary way by Korobeinikov (Bull. Math. Biol. 66, 879-883). He uses a Lyapunov function. When a Lyapunov function is known apparently intractable problems can become simple. This can work for dynamical systems of any dimension. On the other hand there is usually no mechanical procedure forfinding Lyapunov functions. That is the point where inspiration is often necessary. It is also interesting to note that the analysis here was helped by using an analogy to a certain system arising in epidemiology (the SEIR model) which had previously been analysed rigorously. The possibility of establishing analogies between mathematical models coming from very different applications is a typical strength of mathematics. In this context I would like to mention something which Rupert Klein said in a talk “Multiple scales in weather and climate” he gave at the Berlin Mathematical School on 11th January 2008. He pointed out that working in climate modelling involves using information coming from many disciplines. Often the specialists in different areas use some of the same concepts but do not know it because these concepts are known by different names in the literature ofthe different research areas. He suggested that in this context mathematicians can play an important role as translators. Mathematicianshave the tendency to extract the essential concepts from a problem they study and this can make the relations between the activities in different fields manifest.