Résultats liés à « Mathématiques »

The hidden geometry of Einstein’s equations
Joel Fine

Towards a new geometric understanding of space-time.

Einstein’s equations describe the curvature of space-time. They are essential for a full understanding of the history of our cosmos, but also for practical purposes such as the use of GPS.

Project description in PDF


Born in 1978. PhD in Differential Geometry (Imperial College London) supervised by the fields Medalist Sir Simon Donaldson, Master in Mathematics and placed 3rd in his year(Oxford). Post-doc at the University of Edinburgh. Associate Professor in Mathematics (ULB). Pr. Joël Fine is a specialist in geometry, in particular geometric analysis and the study of Einstein’s equations. He has published in leading mathematical journals such as Duke Mathematical Journal, Journal of Differential Geometry, Journals of the London Mathematical Society, Mathematische Annalen…

Distinguished international invitations include a visiting professorship at the Simons Center for Geometry and Physics (New York) and plenary speaker at the Chern Centennial conference (Mathematical Sciences Research Institute, Berkeley). He is promotor of several research projects, most notably those financed by a prestigious European Research Council Consolidator Grant and an FNRS mandat d’impulsion scientifique.

The project

1 -Einstein’s fundamental equations

Einstein’s equations describe the curvature of time and space. They are of course central to physics, but they also play a critical role in modern mathematics.
The first important question is “on which geometric spaces can we solve Einstein’s equations?” These correspond to possible shapes of the universe.

Despite fantastic advances (most notably Fields Medal winning work of Yau in 1977) we  still know of a very limited number of solutions to these fundamental equations. The second important question is “what do solutions to the equations tell us about the underlying spaces?” This was the theme of Perelman’s recent proof of the Poincaré conjecture, for which he was offered  the Fields Medal in 2006.

Perelman’s work settled many deep problems in three-dimensional geometry. The corresponding questions in dimension four,  the  dimension truly relevant to  Einstein’s theory, remain completely open.

Uncovering the hidden geometry behind Einstein’s equations will potentially open the way to a quantum theory of gravity


My goal is to explore a new, previously hidden, geometry behind Einstein’s equations. My new idea is to rewrite Einstein’s equations a “gauge theory”. In gauge theories, the force which seemingly plays the main role is not the central character. Instead there is a “potential” from which the force is derived and it is the potential that is truly fundamental. In classical physics, the potential cannot be observed directly, only the force can. But in quantum physics, one can see the potential even when there is no force at all (a  phenomenon called the Aharonov-Bohm effect).

Hyperbolic geometry plays a key role in our understanding of 3-dimensional geometry. It is also essential to the discovery by Fine-Panov of the diversity of symplectic Calabi-Yau manifolds, as predicted by string theory

In 2011, I found  a potential for Einstein’s theory. The original “obvious” object can be written in terms of a potential. The potential brings a geometry completely different from the traditional geometry of Einstein’s theory.  This new geometry takes place in a 6-dimensional space, of which 4-dimensional space-time is a shadow. This opens up two exciting possibilities: the hidden 6-dimensional geometry can be used to try and solve Einstein’s equations; it also shows how Einstein’s equations help in understanding four-dimensional spaces, similar to the use of metric geometry in three dimensions, central to Perelman’s work.

This gauge theoretic approach to Einstein’s equations was also discovered independently by Kirill Krasnov. We have since collaborated intensively on our joint theory, greatly benefitting from our complimentary backgrounds. The importance of our research has been recognized by two separate European Research Council grants, mine in mathematics, Krasnov’s in theoretical physics.



The traditional approach to Einstein’s equations is to use metric geometry. Over the past 100 years many results have been proved, but recent progress has been slow as the techniques available have been fully exploited and no new ones discovered.

Gauge theories are used to understand all microscopic phenomenon, such as this proton-proton scattering which occurred at the LHC in Geneva. This project represents one of the first uses of gauge theory to understand the macroscopic nature of gravity and space-time.

The gauge theoretic approach to Einstein’s equations reveals a new geometry, namely symplectic geometry, which we can exploit. In the last thirty years there has been an explosion in the study of symplectic spaces, thanks to the discovery of a whole host of new powerful techniques.

One theme of the project is to exploit these new methods to discover more solutions to Einstein’s equations.

Another theme is to explore this relation in reverse: the metric geometry of Einstein’s equations can be used to prove deep new results about symplectic geometry.

One example of this is the discovery by Dmitri Panov and myself of the existence of a huge number of “symplectic Calabi-Yau manifolds”. The internal consistency of string theory and mirror symmetry predicts the existence of many spaces carrying a special symplectic geometric structure.

Panov and I were the first to discover these spaces. We did so by exploiting the new link between Einstein’s equations in 4-dimensions and symplectic geometry in 6-dimensions. I fully believe that this is the tip of the iceberg, and that many  more important results in symplectic geometry can be proved this way.

Part of the Hopf fibration, a collection of circles filling out three-dimensional space. This is the simplest example of a gauge theory, corresponding to electromagnetic forces on a two-dimensional sphere

The final and most important theme is a combination of the previous two. The two different geometries in play – symplectic and metric – can be combined to create a new collection of techniques going far beyond purely metric or purely symplectic methods. I have made a first step in this direction, showing that symplectic geometry and metric geometry together give limits on the singularities which can occur in space-time (where the curvature becomes infinite, such as at a black hole). There is much more which can be done here: a new fusion of metric and symplectic ideas will vastly improve our understanding of 4 dimensional geometry and has the potential to revolutionise the study of Einstein’s equations.

4 -Some research highlights

A 3-dimensional projection of the skeleton of a 120-cell, the key building block in the work of Fine-Panov, discovering a huge number of symplectic Calabi-Yau manifolds.

Highlights in my track record include the discovery of a vast number of symplectic Calabi-Yau spaces, answering a twenty year old question, inspired by string theory, which had stumped even the Fields Medal winning mathematician Yau himself.

I was also responsible for finding the quantum analogue of the Calabi flow, a special way of deforming space so that the local average of its curvature becomes constant.

This curvature condition is a generalisation of Einstein’s equations and Calabi flow and its quantisation are at the heart of current research in this direction.


Pr. Joël Fine’ research is supported by:

5 -Differential geometry group, ULB mathematics dept

A black hole is an example of a singularity in space-time. The precise nature of singularities is governed by the symplectic geometry, revealed by the gauge theoretic approach.

I am currently the head of a group of six: four postdoctoral researchers and two doctoral students. The international reputation of my work helps me select from the very best mathematicians worldwide.

I received over fifty serious candidates for the last postdoctoral position open in my group, with applicants from universities  such as Harvard, MIT, Stanford, Cambridge, Oxford and Imperial College.

My current team has experts in both metric and symplectic geometry. I am privileged to have one of the bright young stars of Chinese mathematics working as a postdoc in my group, Chengjian Yao. At 19 years old, Yao was fast-tracked into his PhD in the US and he has continued to dazzle ever since.

Unfortunately we are the only team in Belgium working in this area. Because of this, we maintain strong links with the geometry groups in London. London is the European centre of excellence for geometry, and I know many of the people there well from my seven years at Imperial College. We have ongoing collaborations, frequent research visits, and a regular joint seminar.

6 -Requested budget over 4 years

The PhD student will investigate solutions to Einstein’s equations which are asymptotically hyperbolic. These spaces have a special geometry  at infinity. The goal is to understand how this interacts with the newly discovered symplectic geometry in six dimensions.

The postdoc will explore the link between the Gromov- Witten theory in the six-dimensional picture and gauge theory in four dimensions. Gromov-Witten theory is a special way to investigate symplectic spaces, named after the Abel prize winning mathematician Misha Gromov and the Fields Medal winning mathematician and physicist Edward Witten.

The travel budget will be used to hold frequent meetings and research seminars with collaborators and colleagues in London, including Sir Simon Donaldson (Fields medalist), André Neves (winner of the Veblen prize) and Michael Singer (editor of the Journal of the London Mathematical Society). It will also pay for regular meetings with Kirill Krasnov (based in Nottingham, UK) the co-discoveror of the new theory on which this project is based.

Click here to see the full budget

IBM Faculty Award décerné au Pr. Jean-François Raskin

 jfraskinL’IBM Faculty award 2014 a été décerné au Pr. Jean-François Raskin pour ses contributions essentielles à la recherche sur la vérification assistée par ordinateurs. Le Pr. Jean-François Raskin développe en effet de nouveaux modèles mathématiques quantitatifs et hybrides pour les systèmes informatiques embarqués. Pour en savoir plus sur son projet

Les preuves mathématiques pour assurer la correction des systèmes informatiques embarqués et d’intelligence artificielle
Jean-François Raskin

Développement de nouveaux modèles mathématiques quantitatifs et hybrides pour les systèmes informatiques embarqués, d’intelligence artificielle et l’analyse de la dynamique des systèmes biologiques.

Dernières nouvelles:

  • L’équipe du Pr. Raskin est partenaire du projet « Verifying Learning Artificial Intelligence Systems » du programme interuniversitaire Excellence of Science 2017-2021 avec des   équipes de la KULeuven et de l’Université de Namur.
  • Le Pr. Jean-François Raskin est élu par ses pairs dans le « working group 2.2 » de l’International Federation for Information Processing.
  • L’équipe du Pr. Jean-François Raskin remporte une Action de Recherche Concertée Advanced 2016-2021
  • Pr. Jean-François Raskin reçoit un mandat de Professeur Francqui pour les années 2015-2018
  • Pr. Jean-François Raskin is awarded with the 2014 IBM Faculty Award
  • Pr. Jean-François Raskin is awarded with the 2014 the silver medal of the Kurt Gödel Society for his prototype of  automatic synthetis


Né en 1972. Docteur en Sciences des Facultés Universitaires Notre-Dame de la Paix (Namur), Post-doctorat à UC Berkeley et au Max-Planck Institute de Saarbrücken. Professeur et ancien Président du Département d’Informatique de la Faculté des Sciences de l’ULB. Il a été notamment Professeur invité à l’Ecole Polytechnique Fédérale de Lausanne et à L’Ecole Normale Supérieure de Cachan.

Cliquez ici pour lire davantage à ce propos



Screen Shot 2013-12-05 at 18.06.04

Aujourd’hui, de nombreuses applications complexes et critiques, telles que l’assistance au pilotage d’un avion ou la régulation du rythme cardiaque par un pacemaker, sont mises en œuvre à l’aide de programmes informatiques.

Pour ces applications critiques, il est primordial de s’assurer que le logiciel construit est correct.

Ecrire un logiciel correct est une tâche difficile. Un logiciel peut en effet comporter plusieurs centaines de milliers de lignes de code et une seule erreur dans un programme peut avoir des conséquences désastreuses.

Malheureusement,  il est encore plus difficile de prouver (mathématiquement) qu’un logiciel ne contient aucune erreur.  Aussi, des recherches sont menées pour concevoir des algorithmes, et donc des programmes informatiques, capables de construire des preuves de correction.

Notre projet de recherche se situe précisément dans le domaine fascinant de la « vérification assistée par ordinateur » (V.A.O). Dans ce cadre, nous développons de nouveaux modèles mathématiques et l’algorithmique nécessaire à leur analyse automatique.


Screen Shot 2013-12-05 at 18.06.13Les modèles et les notions de corrections développés jusqu’à présent dans le domaine de la vérification assistée par ordinateur peuvent être qualifiés de « Booléens ». En effet, ils permettent d’établir qu’un programme est correct ou non. Ils ne permettent pas d’établir des critères de qualité plus fins.

Par exemple, un logiciel pour pacemaker doit opérer des choix en « temps réel » en fonction du comportement du cœur du patient. Si des arythmies sont détectées, le logiciel commande l’émission et l’intensité d’impulsions électriques qui auront pour effet de rétablir un rythme cardiaque plus adéquat.

La correction du logiciel qui pilote les impulsions électriques est donc primordiale. Au surplus, il faut trouver une solution qui soit la plus parcimonieuse possible. En effet, afin de garantir une qualité de vie optimale au patient, le pacemaker ne doit intervenir que si cela est nécessaire.

Pour modéliser cette notion d’optimalité, nous avons donc besoin de modèles mathématiques plus riches qui permettent de modéliser des quantités (comme la fréquence des interventions du pacemaker) et de raisonner sur ces dernières.


Screen Shot 2013-12-05 at 18.06.25Pour développer ces nouveaux outils informatiques, nous avons besoin de faire des progrès dans notre compréhension des propriétés fondamentales des nouveaux modèles mathématiques envisagés et de leurs algorithmes d’analyse.

Théorie des automates et les logiques associées

La théorie des automates finis est un des socles fondamentaux sur lesquels reposent les algorithmes de vérification de propriétés de correction des logiciels embarqués.

Depuis quelques années, des travaux de recherche visent à étendre ces théories avec des aspects quantitatifs : soit en ajoutant des variables à valeurs numériques aux automates finis pour contrôler plus finement leur exécution, soit en considérant les automates non plus comme définissant une fonction Booléenne mais une fonction dont la valeur est prise dans un domaine  infini, comme les réels ou les rationnels par exemple.

Ces modèles de calcul plus riches permettent la modélisation de systèmes informatiques plus complexes.

Pourtant, de nombreuses questions fondamentales sur ces formalismes restent ouvertes : quelle est l’expressivité des différentes classes d’automates? quelles sont les logiques équivalentes aux automates?  quelles nouvelles notions de corrections peuvent être formalisées? ces formalismes sont-ils robustes ?

Algorithmes ou semi-algorithmes pour les modèles quantitatifs.

Les problèmes de vérification que nous devons considérer sur les modèles quantitatifs sont généralement plus complexes que pour les modèles classiques, d’un point de vue conceptuel mais également d’un point de vue calculatoire.

Plusieurs problèmes importants (comme le problème d’inclusion de langages) ont déjà été montrés indécidables pour les extensions quantitatives. D’autres problèmes restent décidables mais le coût de leur résolution est très nettement accru.

Néanmoins, pour les problèmes indécidables, il convient de comprendre la frontière de décidabilité et également de proposer des solutions approchées -basées par exemple sur l’interprétation abstraite- ou encore des semi-algorithmes symboliques afin d’obtenir des solutions qui ont un intérêt dans la pratique.

Pour obtenir des résultats significatifs dans ce domaine, nous avons donc besoin de faire des avancées majeures dans notre compréhension des problèmes situés à la frontière de l’informatique théorique et des mathématiques. Ces avancées seront la base de nouveaux outils informatiques d’analyse de systèmes complexes.

Les systèmes « hybrides »

Un système informatique embarqué est typiquement un système « hybride » puisqu’il vise à contrôler un processus physique -dont l’évolution est continue- par l’intermédiaire de décisions discrètes qui auront en retour un effet sur l’évolution continue du système.

Les systèmes biologiques sont également des systèmes de nature hybride. En effet, la concentration d’une protéine évolue de façon continue dans le temps alors que l’activation ou l’inhibition d’un gène résultant dans le changement de mode de fonctionnement biochimique d’une cellule est typiquement un événement discret.

Ce dernier point est important pour comprendre l’une des applications que nous visons.

4. APPLICATIONS VISEES : systèmes embarqués  et  modélisation des systèmes biologiques


Les systèmes informatiques embarqués sont une cible privilégiée pour ces nouveaux modèles mathématiques. Les nouveaux outils de vérification que nous développerons permettront une conception plus rigoureuse de ces systèmes informatiques embarqués. Ils permettront également de certifier leur correction à l’aide de preuves mathématiques.

Il y a actuellement une demande importante pour des avancées en vérification assistée par ordinateur dans des domaines aussi importants que l’informatique pour les applications spatiales, l’aéronautique, les équipements médicaux, les microprocesseurs, la sécurité nucléaire, etc.


Recently, artificial intelligence (AI) has made substantial progresses in a series of applications domains: driverless cars, IBM’s Watson program, deep learning techniques for playing Go, are popular examples. But those recent AI’s progresses also trigger important new questions about the future: what AI systems will be able to do, what they should be allowed to do, and what the implications are for humans.

The ongoing debate has motivated the AI and computer science communities to investigate what constitutes “safe AI” and whether it is possible to develop such “safe AI” systems that can be trusted. Quoting Dr. Guruduth Banavar, Vice President of IBM Research: ”Artificial intelligence is not without its risks. But we believe the risks are manageable. And that the far greater risk would be to stifle or otherwise inhibit the development of a technology with the potential to greatly improve the quality of life around the world. […] To reap the societal benefits of AI systems, we will first need to trust it. […] Trust is built upon accountability. As such, the algorithms that underpin AI systems need to be as transparent, or at least interpretable, as possible.” In this project, we want to push this research agenda and we claim that AI systems must also be mathematically verifiable. The trust in system is particularly important for systems that are safety critical (this is the case for example for driverless cars).

Our project aims at providing theoretical foundations and algorithmic methods to support the design of safer artificial intelligence systems that use learning. Tackling this important, timely and ambitious research agenda, requires on the one hand, extending verification models, and design methodologies, and verification algorithms to cover AI systems that learn, and on the other hand, improving learning methods so that they provide guarantees that can be used in verification.

As a starting point for our research, we will build on mathematical models and algorithms that we have developed in a recent project founded by European Research Council. In the context of this project, we have generalized transition systems and automata – models of computation in the classical approach to verification – by the more flexible, and mathematically deeper, game-theoretic and stochastic frameworks.

We intend to pursue this research work in collaboration with researchers active in the area of learning and articifical intelligence. To this aim, we have recently established a collaboration with a world renowed team at KULeuven.


Notre projet inclut également un pan novateur qui vise spécifiquement la recherche en biologie.

En effet, les modèles mathématiques hybrides que nous développons sont également bien adaptés à la modélisation et l’analyse de la dynamique des systèmes biologiques.

Certes, les biologistes possèdent des outils performants pour la modélisation de leurs systèmes, mais ces outils sont basés principalement sur les équations différentielles, soit les mathématiques du continu.

Malgré une réelle demande provenant des biologistes pour des outils de modélisation hybrides, plus adaptés à la nature -même des systèmes qu’ils étudient, les avancées dans ce domaine sont encore timides : seulement une dizaine de laboratoires au monde travaillent sur cette question.

Pour progresser de manière significative dans ce domaine, nous collaborerons avec des collègues spécialisés en biologie théorique, notamment via l’engagement d’un post-doc formé à la modélisation des systèmes biologiques qui pourra nous fournir des études de cas réalistes sur lesquels nos nouveaux formalismes mathématiques pourront  être appliqués.

Notre recherche permettra donc de faire avancer la modélisation de la dynamique des systèmes biologiques en la rendant plus simple, plus efficace et en somme, plus proche de la réalité.



Screen Shot 2013-12-05 at 18.06.34Le groupe « Méthodes Formelles et Vérification Assistée par Ordinateur » a été créé en 2000 au sein du Département d’Informatique de la Faculté des Sciences de l’ULB.

Le groupe est la référence belge dans le domaine de la vérification assistée par ordinateur (V.A.O.) et de nombreux chercheurs étrangers visitent régulièrement Bruxelles pour collaborer avec le groupe du Prof. Jean-François  Raskin.

Le groupe coordonne par ailleurs le Centre Fédéré en Vérification  du FNRS qui rassemble toutes les équipes universitaires belges actives dans le domaine de la V.A.O.

Le groupe est également très actif dans le concert de la recherche européenne et a participé  (comme membre ou coordinateur)  à plusieurs projets de recherche européens d’envergure : FP7 NoE, FP7 STREP, ESF Eurocores, ESF Networks, COST Actions, etc.

Dans les prochains mois, le groupe du Pr. Raskin participera également à un nouveau projet de recherche européen, financé par l’action Future and Emerging Technologies du 7e Programme Cadre qui visera à mettre au point de nouveaux outils de développement de systèmes informatiques complexes à l’aide de la théorie des jeux.

Le groupe a une expertise reconnue dans les thématiques suivantes: systèmes hybrides et temps-réels, systèmes à espaces d’états infinis, model checking, algorithmes symboliques basés sur les antichaînes, algorithmes de synthèse basés sur la théorie des jeux.

Budget sur 4 ans


Deux chercheurs post-doctorants avec une expérience de recherche en informatique théorique travailleront sur les fondations mathématiques et algorithmiques.

Ils développeront également des outils de vérification pour les nouveaux formalismes.

Ces chercheurs collaboreront avec un biologiste ayant une expertise en modélisation des systèmes biologiques pour appliquer les théories et outils développés.


Afin de développer l’expertise en modélisation des systèmes biologiques, des échanges scientifiques de moyenne durée seront organisés chez des collègues étrangers spécialisés dans la modélisation de tels systèmes à l’aide d’automates (IST Austria, UPenn et UC Berkeley).

Par ailleurs, des ordinateurs performants seront nécessaires au développement des outils informatiques pour l’analyse de modèles mathématiques complexes. Ces équipements seront également utilisés pour l’analyse de modèles de systèmes embarqués et de systèmes biologiques.

L’analyse de ces modèles requiert des ressources de calcul importantes et dédiées.

Cliquez ici pour dérouler le tableau du budget


La fiche du projet disponible au format PDF ici.